Safe and Verifiable Design of Concurrent Programs

The design of concurrent programs has a reputation for being difficult, and thus potentially dangerous in safety-critical real-time and embedded systems. The recent appearance of Java, with its simple thread model, and new CASE tools that can verify and check the design of concurrent applications, now significantly reduce design and testing time and eliminate those problems which commonly plague concurrent systems. Our approach uses recently developed Java class libraries based on Hoare's Communicating Sequential Processes (CSP); the use of CSP greatly simplifies the design of concurrent systems and, in many cases, a parallel approach often significantly simplifies systems originally approached sequentially. New CSP CASE tools permit designs to be verified against formal specifications and checked for deadlock and livelock. Below we introduce CSP and its implementation in Java and develop a small concurrent application. The formal CSP description of the application is provided, as well as that of an equivalent sequential version. FDR is used to verify the correctness of both implementations, their equivalence, and their freedom from deadlock and livelock.