Consistency Checking for LSC Specifications

Live sequence charts (LSCs) have been proposed as an inter-object scenario-based specification and visual programming language. In this paper, we introduce a high level computational semantics of LSCs, in the form of a PLAY-tree, to show how a running LSC affects the system behaviors in response to a set of external events. Given a nonempty regular language of external events,the consistency of an LSC specification is defined as whether there exists a corresponding PLAY-tree with all success branches; in case of inconsistency, failure traces can be obtained through failure branches of the PLAY-tree. We also present an algorithm using a memoized depth-first search strategy and an implementation framework in logic programming for consistency checking of LSCs.