Please use this identifier to cite or link to this item:
|Title:||Model checking live sequence charts||Authors:||Sun, J.
|Issue Date:||2005||Citation:||Sun, J.,Dong, J.S. (2005). Model checking live sequence charts. Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS : 529-538. ScholarBank@NUS Repository.||Abstract:||Live Sequence Charts (LSCs) are a broad extension to Message Sequence Charts (MSCs) to capture complex inter-object communication rigorously. A tool support for LSCs, named PlayEngine, is developed to interactively "play-in" 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 to CSP. The practical implication is that mature tool supports for CSP can be reused to validate LSCs. In particular, FDR is used to establish the consistency of an LSC model and perform various verification. © 2005 IEEE.||Source Title:||Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS||URI:||http://scholarbank.nus.edu.sg/handle/10635/40055|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Oct 28, 2019
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.