Sciweavers

ICECCS
2005
IEEE

Model Checking Live Sequence Charts

13 years 9 months ago
Model Checking Live Sequence Charts
Live Sequence Charts (LSCs) are a broad extension to Message Sequence Charts (MSCs) to capture complex interobject communication rigorously. A tool support for LSCs, named PlayEngine, is developed to interactively “playin” and “play-out” scenarios. However, PlayEngine cannot automatically expose system design inconsistencies, e.g. conflicts between universal charts and etc. CSP is a formal language to specify sequential behaviors of a process and communication between processes, which has powerful tool supports, e.g. FDR. Semantically, system behaviors specified by LSCs correspond to CSP’s traces and failures. This close semantic correspondence makes FDR a potential model checker for LSCs. The challenge is to discover a systematic way of constructing semantic preserving CSP models from LSCs. In this work, we investigate theoretical relations between LSCs and CSP. LSCs are formalized using trace and failure semantics so as to facilitate the semantic transformation from LSCs...
Jun Sun 0001, Jin Song Dong
Added 24 Jun 2010
Updated 24 Jun 2010
Type Conference
Year 2005
Where ICECCS
Authors Jun Sun 0001, Jin Song Dong
Comments (0)