Show simple item record

dc.contributor.authorTysowski, Piotr 18:09:08 (GMT) 18:09:08 (GMT)
dc.description.abstractMessage sequence charts (MSC’s) are a formal language for the specification of scenarios in concurrent real-time systems. The thesis addresses the synthesis of executable object-oriented design-time models from MSC specifications. The synthesis integrates with the software development process, its purpose being to automatically create working prototypes from specifications 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 specification 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 specification 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 specified 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 identified properties using the model checker Spin. A ROOM model was then synthesized from the validated MSC specification using the proposed refinement features.en
dc.publisherUniversity of Waterlooen
dc.subjectSoftware Engineeringen
dc.titleExecutable Model Synthesis and Property Validation for Message Sequence Chart Specificationsen
dc.typeMaster Thesisen
dc.pendingfalse and Computer Engineeringen and Computer Engineeringen of Waterlooen
uws-etd.degreeMaster of Applied Scienceen
uws.contributor.advisorLeue, Stefan
uws.contributor.affiliation1Faculty of Engineeringen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages