Login | Register

Validation and refinement of timed MSC specifications


Validation and refinement of timed MSC specifications

Zheng, Tong (2004) Validation and refinement of timed MSC specifications. PhD thesis, Concordia University.

[thumbnail of NQ90407.pdf]
Text (application/pdf)
NQ90407.pdf - Accepted Version


This thesis addresses the validation and the refinement of MSC (Message Sequence Charts) specifications at the requirement and the design phases in a software development process. The validation is necessary to ensure that an MSC specification does not contain semantic errors. The refinement provides a systematic approach to develop MSC specifications. The focus of this thesis is on timed MSC specifications, which may contain absolute and relative time constraints for specifying quantified timing requirements. To provide a foundation for analysis of MSC specifications, we develop a formal semantics for timed MSCs based on labeled partially ordered sets (lposets). We equip an lposet with two timing functions for expressing absolute and relative time constraints. The semantics of an MSC is represented by a set of lposets. The set can be obtained compositionally from the semantics of constructs contained in the MSC. Time constraints in an MSC specification may lead to inconsistencies. In such a case, the specification contains semantic errors. We study the time consistency of MSC specifications. We define the time consistency and develop sufficient and necessary conditions for the consistency. According to these conditions, algorithms are designed for checking the consistency. We also study the time consistency of high level MSCs and identify a subset of high level MSCs such that their consistency can be checked efficiently. We propose a refinement approach where we refine not only behaviors, but also time constraints specified in an MSC specification. Refining time constraints makes constraints on a system stronger, and assumptions on the environment weaker. We define refinement relations and develop algorithms to check the satisfaction of these relations. To reduce the complexity in the case of high level MSCs, we constrain the refinement rules. At last, as an outcome of our investigation of timed MSCs, we propose a new time construct as an extension of timed MSC in order to specify more timing requirements. Most of the algorithms presented in this thesis have been implemented and integrated to our set of tools MSC2SDL.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (PhD)
Authors:Zheng, Tong
Pagination:xiv, 150 leaves ; 29 cm.
Institution:Concordia University
Degree Name:Ph. D.
Program:Electrical and Computer Engineering
Thesis Supervisor(s):Khendek, Ferhat
Identification Number:QA 76.76 V47Z44 2004
ID Code:8000
Deposited By: Concordia University Library
Deposited On:18 Aug 2011 18:12
Last Modified:13 Jul 2020 20:03
Related URLs:
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top