TY - GEN
T1 - L2C2
T2 - 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP'09
AU - Guo, Hai Feng
AU - Zheng, Wen
AU - Subramaniam, Mahadevan
PY - 2009
Y1 - 2009
N2 - Live sequence charts (LSCs) have been proposed as an inter-object scenario-based specification and visual programming language for reactive systems. In this paper, we introduce a logic-based framework to check the consistency of an LSC specification. An LSC simulator has been implemented in logic programming, utilizing a memoized depth-first search strategy, to show how a reactive system in LSCs would response to a set of external event sequences. A formal notation is defined to specify external event sequences, extending the regular expression with a parallel operator and a testing control. The parallel operator allows interleaved parallel external events to be tested in LSCs simultaneously; while the testing control provides users to a new approach to specify and test certain temporal properties (e.g., CTL formula) in a form of LSC. Our framework further provides either a state transition graph or a failure trace to justify the consistency checking results.
AB - Live sequence charts (LSCs) have been proposed as an inter-object scenario-based specification and visual programming language for reactive systems. In this paper, we introduce a logic-based framework to check the consistency of an LSC specification. An LSC simulator has been implemented in logic programming, utilizing a memoized depth-first search strategy, to show how a reactive system in LSCs would response to a set of external event sequences. A formal notation is defined to specify external event sequences, extending the regular expression with a parallel operator and a testing control. The parallel operator allows interleaved parallel external events to be tested in LSCs simultaneously; while the testing control provides users to a new approach to specify and test certain temporal properties (e.g., CTL formula) in a form of LSC. Our framework further provides either a state transition graph or a failure trace to justify the consistency checking results.
KW - Live sequence chart (LSC)
KW - Logic programming
KW - Memoization
KW - PLAY-tree
KW - Scenario-based programming
UR - http://www.scopus.com/inward/record.url?scp=70450242752&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70450242752&partnerID=8YFLogxK
U2 - 10.1145/1599410.1599433
DO - 10.1145/1599410.1599433
M3 - Conference contribution
AN - SCOPUS:70450242752
SN - 9781605585680
T3 - PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming
SP - 183
EP - 194
BT - PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming
Y2 - 7 September 2009 through 9 September 2009
ER -