The decades old problem of formally securing safety critical systems is addressed in this paper. These are concurrent systems that interact with critical physical environments.
The authors describe verification processes that involve multiple steps. Starting with a source description of a safety critical system, it is necessary to specify its behavior, and what needs to be verified, and to build a model and exhaustively exercise it to evaluate its behavior. The language for system description is the unified model language (UML), in particular, its class and state charts. UML is used widely for system specification. The next step consists of describing the system’s requirements, based on the description in UML, using the underlying UML semantics. This is done using the graphical language of live sequence charts (LCS). Next, it is necessary to construct the resulting state transition model. This is enormous, even for a small example, and must be reduced to a finite manageable size. Finally, the model is checked to verify the requirements through execution (or simulation).
The first author, Damm, contributed to several of these steps. With the coauthor, he integrates these steps, and provides formal definitions and proofs for them. An extensive list of references is provided. A small example of an automated rail cars system (ARCS) is used to illustrate sub-steps in the process, but the example is embedded in detailed formalisms. There are also discussions and comparisons of advantages over other reported approaches and steps. The paper documents the formal definitions and proofs in the presented chain of steps for verifying safety critical systems. The paper will provide a valuable resource for researchers, though there is extensive literature available on the many other approaches to this problem, spanning the decades of research on safety critical systems.
This paper is directed to those deeply initiated in the topic. There is still a need to explain to noninitiated practitioners the concepts and techniques embedded in the steps described in the paper. Several such references are cited. To start with, I recommend the intuitive and easy-to-follow description in Harel and Marelly’s book [1]. This describes the practical use of the LCS language, with examples and system simulation.