CitedEvidence
User Settings
Open AccessDissertation

Validation and refinement of timed MSC specifications

Tong Zheng-2004-01-01-Spectrum Research Repository (Concordia University)
3PDF

TL;DRAbstract

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

Chat with Paper

AI Agents for this Paper

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

Keywords

Consistency (knowledge bases)Computer scienceSemantics (computer science)Set (abstract data type)Programming languageFormal specificationProcess (computing)Formal methods

Chat

Click to start Chat