Specification of hybrid systems in cTLA+

Author

Herrmann, Peter ; Krumm, Heiko

Author_Institution

Fachbereich Inf., Dortmund Univ., Germany

fYear

1997

fDate

1-3 Apr 1997

Firstpage

212

Lastpage

216

Abstract

cTLA+ is a compositional specification and verification technique which is based on Leslie Lamport´s (1994) Temporal Logic of Actions TLA. cTLA+ supports modular process type definitions and the composition of processes to systems. Processes can model components of an implementation. Moreover they can represent modular logical constraints. Constraint-oriented structures of system specifications are of particular interest, since they can help to decompose verifications into manageable subtasks. In order to support the constraint-oriented description of hybrid systems, we developed suitable extensions of cTLA+ which cover real-time and continuous properties. We give an outline of cTLA+ and demonstrate the hybrid extensions by means of a small example. Also, the example gives a first impression of constraint-oriented specification structures of hybrid systems

Keywords

algebraic specification; formal specification; program verification; real-time systems; specification languages; temporal logic; TLA; Temporal Logic of Actions; cTLA+; compositional specification technique; constraint-oriented description; continuous properties; hybrid system specification; modular logical constraints; modular process type definitions; real-time systems; verification technique; Control systems; Formal verification; ISO; Logic design; Process control; Safety; Specification languages; State-space methods; Switches; Valves;

fLanguage

English

Publisher

ieee

Conference_Titel

Parallel and Distributed Real-Time Systems, 1997. Proceedings of the Joint Workshop on

Conference_Location

Geneva

Print_ISBN

0-8186-8096-2

Type

conf

DOI

10.1109/WPDRTS.1997.637981

Filename

637981