State-machine Construction for LSC Specification
Eunyoung Lee · 한국정보기술학회논문지 · 2010
Live sequence chart (LSC) specification is an extension of message sequence charts for inter-object interaction specification. Live sequence charts have strengths over traditional message sequence charts: message abstraction, a richer set of constructs such as loops or forbidden messages, and explicit modes to distinguish whether a chart must always or at least once be satisfied. Scenario-based languages are usually used for specifying and/or verifying requirements against an already-implemented system. However, a scenario-based language with rich semantics like the LSC specification can also be used to specify a system to be implemented. In this paper, I propose an algorithm synthesizing a global finite state machine from requirements, after refining the formal semantics of LSC specification. The proposed algorithm can understand and properly handle LSC's expressive constructs, such as pre-charts, object properties and conditions, producing an implementation of the LSC specifications described by those constructs.