UML and Model Checking
Frank W. Schneider · 1999
UML use cases conceptually identrfy function points or major requirements that a software system must satisfy. Se-quence diagrams expand each use case to show in temporal sequence a more detailed notion of intended system behavior. The validation of sequence charts can first be examined with a model checker to determine if there are requirements violations. This process is particularly relevant in the case systems that are concurrent and reactive. We show how to apply this technique to a real-time interferometer control system using the model checker SPIN. 1 introduction This paper describes a practical application of model checking for validating sequence diagrams for the JPL Interferometer Technology Program Real-Time Control application [ 11. This application is the generic control element of a system of interferometers that are currently being designed at the Laboratory. The case study described here is the command engine framework, that provides interfaces and mechanisms to define command execution as part of a command processor called the Gizmo. The Gizmo receives commands from an external processor that require the use of scarce resources. The Unified Modeling Language [2] sequence diagrams specify the temporal order of execution. Since it is possible that commands could arrive erratically, it is possible that inadvertent out-of-sequence commands could cause a system malfunction. This could be due to elements timing out in ways that were not anticipated. Because the process of modeling