Abstract | ||
---|---|---|
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. |
Year | DOI | Venue |
---|---|---|
1997 | 10.1109/APSEC.1997.640171 | APSEC |
Keywords | Field | DocType |
specification exhibit,object-z specification,partial validation,complex system,certain property,object property,modular reasoning,formal specification validation activity,modular semantics,system property,information technology,formal specification,proof,formal specifications,object oriented programming,complex systems | Complex system,Programming language,Object-oriented programming,Systems engineering,Computer science,Property (programming),Formal specification,Modular reasoning,Theoretical computer science,Modular design,Semantics,Object-Z | Conference |
ISBN | Citations | PageRank |
0-8186-8271-X | 5 | 0.76 |
References | Authors | |
5 | 1 |
Name | Order | Citations | PageRank |
---|---|---|---|
Griffiths, A. | 1 | 5 | 0.76 |