Specification of hybrid systems in cTLA+

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