loading...
Modular reasoning in Object-Z
Clear Water Bay, HONG KONG December 02-December 05
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/APSEC.1997.640171Fourth Asia-Pacific Software Engineer ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A. Griffiths, Sch. of Inf. Technol., Queensland Univ., Qld., Australia
One of the tasks of a formal specification validation activity is to prove that systems described by the specification exhibit certain properties. For specifications describing large and complex systems, this can be difficult. Modular reasoning is an approach to this task in which one views a system as a number of smaller; simpler components, and where one attempts to carry out most of the reasoning at the component level. The paper describes a framework for conducting modular reasoning about Object-Z specifications. Using the strictly modular semantics of Object-Z as a foundation, the author formalises the notions of object property and system property. She presents results that enable object properties, which are the product of modular reasoning, to be used in the proof of system properties. The ideas are illustrated via the specification and partial validation of a small example.
Index Terms:
formal specification; Object-Z; modular reasoning; formal specification validation; complex systems; large systems; modular semantics; object property; system property; proof; partial validation
Citation:
A. Griffiths, "Modular reasoning in Object-Z," apsec, pp.140, Fourth Asia-Pacific Software Engineering and International Computer Science Conference (APSEC'97 / ICSC'97), 1997
Usage of this product signifies your acceptance of the Terms of Use.