Model Checking of Message Sequence Charts

摘要: Scenario-based specifications such as message sequence charts (MSC) offer an intuitive and visual way of describing design requirements. Such focus on exchanges among communicating entities in distributed software systems. Structured MSC-graphs Hierarchical (HMSC) allow convenient expression multiple scenarios, can be viewed early model the system. In this paper, we present a comprehensive study problem verifying whether satisfies temporal requirement given by automaton, developing algorithms for different cases along with matching lower bounds. When is MSC, checking done constructing suitable automaton linearizations partial order specified coNP-complete. When MSC-graph, consider two possible semantics depending synchronous or asynchronous interpretation concatenating MSCs. For HMSCs, whose time complexity proportional to product size description cost processing MSCs at individual vertices. Under interpretation, prove undecidability problem. We, then, identify natural boundedness, give check establish Pspace-complete bounded Expspace-complete HMSCs.