Applied formal methods - From CSP to executable hybrid specifications

Abstract

Since 1985, CSP has been applied by the author, his research team at Bremen University and verification engineers at Verified Systems International to a variety of "real-world" projects. These include the verification of high-availability database servers, of fault-tolerant computers now operable in the International Space Station, hardware-in-the-loop tests for the novel Airbus A380 aircraft controller family and conformance tests for the European Train Control System. Illustrated by examples from these projects, we highlight important aspects of the CSP language design, its semantics and tool support, and describe the impact of these features on the quality and efficiency of verification and testing. New requirements with regard to the test of hybrid control systems, the demand for executable formal specifications, as well as the ongoing discussion about the practical applicability of formal methods have led to the development of new specification formalisms. We sketch some key decisions in the formalism design and indicate how some of the fundamental properties of CSP have been adopted, while others have been deliberately discarded in these new developments. © Springer-Verlag Berlin Heidelberg 2005.