Technical Report on Cycle Calculus and Framework
for Hybrid and Safety Critical System Specification
with three Case Studies
Formal Systems Research Group
Department of Computer Science
University of York
email: [email protected]
In this report a formal framework for the development of hybrid and safety critical systems is introduced. The framework consists of a Cycle calculus, a computational model of reactive systems, and a procedure to develop the top level specification of a safety critical system. The Cycle Calculus incorporates both discrete and continuous time modes, integrates state-base and event-base formalisms in a unifying framework, and combines conventional continuous functions, includes differential and integral functions, with digital logic components. The Cycle Calculus has a wide application in various forms of dependability analysis for hybrid systems, especially in temporal analysis and safety analysis. Three application examples, an automatic door system, a lift system and a safe pump system are given in full. This report serves as a technical reference manual.