Executable Model Synthesis and Property Validation for Message Sequence Chart Specifications
MetadataShow full item record
Message sequence charts (MSC’s) are a formal language for the speciﬁcation of scenarios in concurrent real-time systems. The thesis addresses the synthesis of executable object-oriented design-time models from MSC speciﬁcations. The synthesis integrates with the software development process, its purpose being to automatically create working prototypes from speciﬁcations without error and create executable models on which properties may be validated. The usefulness of existing algorithms for the synthesis of ROOM (Real-Time Object Oriented Modeling) models from MSC’s has been evaluated from the perspective of an applications programmer ac-cording to various criteria. A number of new synthesis features have been proposed to address them, and applied to a telephony call management system for illustration. These include the speciﬁcation and construction of hierarchical structure and behavior of ROOM actors, views, multiple containment, replication, resolution of non-determinism and automatic coordination. Generalizations and algorithms have been provided. The hierarchical actor structure, replication, FSM merging, and global coordinator algorithms have been implemented in the Mesa CASE tool. A comparison is made to other speciﬁcation and modeling languages and their synthesis, such as SDL, LSC’s, and statecharts. Another application of synthesis is to generate a model with support for the automated validation of safety and liveness properties. The Mobility Management services of the GSM digital mobile telecommunications system were speciﬁed in MSC’s. A Promela model of the system was then synthesized. A number of optimizations have been proposed to reduce the complexity of the model in order to successfully perform a validation of it. Properties of the system were encoded in Linear Temporal Logic, and the Promela model was used to automatically validate a number of identiﬁed properties using the model checker Spin. A ROOM model was then synthesized from the validated MSC speciﬁcation using the proposed reﬁnement features.
Cite this version of the work
Piotr Tysowski (2000). Executable Model Synthesis and Property Validation for Message Sequence Chart Specifications. UWSpace. http://hdl.handle.net/10012/12041