Paper Info
Title
Formal Development of Object-Based Systems in a Temporal Logic Setting
Abstract
This paper presents TLO, an approach to the formal development of object- based systems in a temporal logic framework. The behavior of an object-based system is viewed as derivable from the behaviors of its constituent co mponent objects. Temporal logic is a formalism well suited for specifying behavior of c oncurrent 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 spe cification 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 (behavior), provided its environment conforms to certain assumptions. Hence, such components are most appropriately specified in an assumption/guarantee style. TLO adopts TLA as the underlying logical formalism. It encompasses a specification language for object-based designs and a corresponding method for specification and verification. The concepts are illustrated by an example inv olving both functional and fault-tolerance requirements.
Year
DOI
Venue
1999
10.1007/978-0-387-35562-7_33
FMOODS
Keywords
Field
DocType
temporal logic setting,object-based systems,formal development,specification language,fault tolerant,open system,temporal logic
Computation tree logic,Temporal logic of actions,Programming language,Interval temporal logic,Computer science,Description logic,Formal specification,Theoretical computer science,Language Of Temporal Ordering Specification,Temporal logic,Formal verification
Conference
ISBN
Citations 
PageRank 
0-7923-8429-6
0
0.34
References 
Authors
11
2
Name
Order
Citations
PageRank
E. Canver1473.43
Friedrich W. Von Henke242549.05