Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Live and let die: LSC based verification of UML models
Damm W., Westphal B. Science of Computer Programming55 (1-3):117-159,2005.Type:Article
Date Reviewed: Oct 24 2005

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.

Reviewer:  N. S. Prywes Review #: CR131919 (0605-0492)
1) Harel, D.; Marelly, R. Come, let’s play: scenario-based programming using LCSs and the play engine. Springer-Verlag, New York, NY, 2003.
Bookmark and Share
  Editor Recommended
 
 
State Diagrams (D.2.2 ... )
 
 
Languages (D.2.1 ... )
 
 
UML (D.3.2 ... )
 
 
Requirements/ Specifications (D.2.1 )
 
Would you recommend this review?
yes
no
Other reviews under "State Diagrams": Date
Modular refinement of hierarchic reactive machines
Alur R., Grosu R. ACM Transactions on Programming Languages and Systems 26(2): 339-369, 2004. Type: Article
Jul 9 2004
Linking architectural and component system views by abstract state machines
Börger E. In Languages for system specification. Norwell, MA: Kluwer Academic Publishers, 2004. Type: Book Chapter
Feb 2 2005

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy