Compositional specification and structured verification of hybrid systems in cTLA

Many modern chemical plants have to be modelled as complex hybrid systems consisting of various continuous and event-discrete components. Besides the modular and easy to read specification, the formal verification of required properties (e.g., safety properties) is a major problem, due to the complexity of the models. In practice, mostly informal argumentations exist which show that certain properties hold. The informal argumentation for one specific property does not deal with the complex system model as a whole but considers specific parts and aspects only. Our approach supports formal proofs which correspond to the informal argumentations even with respect to the use of subsystems only. It is based on the specification language cTLA supporting modular descriptions of hybrid systems. We outline cTLA and introduce the approach by means of a hybrid example system