Time inconsistency analysis and correction for MSC-2000 specifications

Message Sequence Charts (MSC) plays an important role in the software life cycle. It is widely used in the requirements, design, and test phases for different purposes. Therefore, it is crucial to insure the correctness of MSC specifications. For that, one has to validate these MSC specifications as early as possible in the development cycle. An important aspect of MSC-2000 specifications correctness is time consistency, including absolute and relative time constraints. The time consistency of Basic MSCs (bMSCs) and High Level MSCs (HMSCs) has been investigated in the last few years. However, a very little effort and research have been devoted for the purpose of investigation and diagnosis of causes of inconsistencies, and also strategies to correct these inconsistencies. This thesis focuses on the consistency checking of MSCs, analyzes and categorizes the causes of time inconsistencies, and provides solutions to correct time inconsistencies. For bMSCs, we classify partial order, propose solutions to identify inconsistency, and provide four correction policies for the different types of inconsistencies. For HMSCs, we decompose them into different simple paths, provide checking algorithms based on the type of the simple paths, and use different correction strategies for these inconsistent paths. Our approach helps MSC developers to insure the correctness of MSC specifications, thereby improving its quality and also that of the resulting software. A tool, called MSCTICC, implementing our algorithms has been developed and assessed in this thesis