Applied Formal Methods - From CSP to Executable Hybrid Specifications

Author: Jan Peleska

Abstract:
Since 1985, CSP has been applied by the author, his research team and verification engineers at Verified Systems International to a variety of ``real-world'' projects. These include the verification 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.

PDF file of full paper (374KB).

PDF file of Slides presented at conference 25 Years of CSP, Institute for Computing Research, London South Bank University, UK 7 and 8 July, 2004 (181KB).