Loading...
Please wait, while we are loading the content...
Similar Documents
Formal Specification and Verification of Object-Based Systems in a Temporal Logic Setting (1997)
| Content Provider | CiteSeerX |
|---|---|
| Author | Canver, E. Henke, F. W. Von |
| Abstract | This paper presents an approach to specification, refinement and verification of object-based systems in a temporal logic framework. The behaviour of an objectbased system is viewed as derivable from the behaviours of its constituent component objects. Temporal logic is a formalism well suited for specifying behaviour of concurrent systems; it also provides conceptually simple notions of composition and refinement: Composition of objects is expressed as conjunction of the associated component specifications. The refinement relation between a low-level and a high-level specification requires that the former specification implies the latter. Specifically in an object-based approach, systems and their components need to be viewed as open systems: Each object guarantees some service (behaviour), provided its environment conforms to certain assumptions. Hence, such components are most appropriately specified in an assumption/guarantee style. The approach presented here adopts TLA as the und... |
| File Format | |
| Language | English |
| Publisher Date | 1997-01-01 |
| Access Restriction | Open |
| Subject Keyword | Temporal Logic Object-based System Formal Specification Former Specification Object-based Approach Environment Conforms Assumption Guarantee Style Objectbased System Simple Notion Temporal Logic Framework Refinement Relation Associated Component Specification Concurrent System Adopts Tla Open System Certain Assumption High-level Specification Constituent Component Object |
| Content Type | Text |
| Resource Type | Technical Report |