Deadlock and Livelock Analysis for the ISS - Experiences with Using Formal Methods in an Industrial Application

Photograph of Bettina Buth

Bettina Buth


From 1995 till 1998 the Bremen Institute of Safe Systems (BISS) and Verified Systems International collaborated with Daimler-Chrysler Aerospace RI (now EADS Space Transportation) for the verification of critical aspects of the central computer of the Russian Module of the International Space Station (ISS). The FTC is a fault-tolerant computer system for controlling experiments as well as docking manouvers. The project objective was to define and perform a verification suite for the software layers implementing the avionics interface (AVI, MIL-STD 1553 bus) as well as the fault management layer (FML). The software consisted of about 11,000 lines of OCCAM code, which exhibits a high degree of concurrency. The verification objectives were to investigate problems predominantly related to the concurrency and the internal communication behaviour of the components. The use of OCCAM had introduced a new level of complexity not easily handled by conventional testing approaches.

These comprise freedom of deadlock, freedom of livelock, correct implementation of voting algorithms, correct implementation of the Byzantine Agreement Protocol, performance properties depending on clock rates, Hardware-In-The-Loop tests for the overall system.

The talk will focus on those aspects which were handled by using CSP and model checking as the basic approach. The general idea for the analysis of communication properties of OCCAM programs as proposed here is to exploit the fact that OCCAM channel communication can easily be modelled in CSP. The basic idea for both deadlock and livelock analysis performed in this project is to use FDR2 for model checking. After manually abstracting the OCCAM programs to CSP processes the systems still is too large for a direct approach using FDR2. Thus it is necessary to decompose the task and use other techniques for combining the results to obtain an overall result for the full system. Some of these techniques are tool supported, others currently are only performed unassisted.

In 2002, it became necessary to re-verify properties of these software modules after they were adapted for the reuse within the Automatic Transport Vehicle ATV developed by EADS Space Transportation. For this purpose the models were adapted and the required checks performed. A side e ect of this analysis is an evaluation which of the software changes a ect the abstract models and in which way.

The talk will discuss both the original work and the experiences of the re-verification.
Tuesday 14th June 2005, 14:00
Esso Lecture Theatre
Department of Computer Science