Technical Report on Cycle Calculus and Framework

for Hybrid and Safety Critical System Specification

with three Case Studies

Heping He

Formal Systems Research Group
Department of Computer Science
University of York
UK
email: [email protected]

ABSTRACT

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.