L2C2

Logic-based LSC consistency checking

Hai Feng Guo, Wen Zheng, Mahadevan Subramaniam

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Citations (Scopus)

Abstract

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.

Original languageEnglish (US)
Title of host publicationPPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming
Pages183-194
Number of pages12
DOIs
StatePublished - Nov 30 2009
Event11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP'09 - Coimbra, Portugal
Duration: Sep 7 2009Sep 9 2009

Publication series

NamePPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming

Conference

Conference11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP'09
CountryPortugal
CityCoimbra
Period9/7/099/9/09

Fingerprint

Specifications
Logic programming
Testing
Computer programming languages
Simulators

Keywords

  • Live sequence chart (LSC)
  • Logic programming
  • Memoization
  • PLAY-tree
  • Scenario-based programming

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Software

Cite this

Guo, H. F., Zheng, W., & Subramaniam, M. (2009). L2C2: Logic-based LSC consistency checking. In PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (pp. 183-194). (PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming). https://doi.org/10.1145/1599410.1599433

L2C2 : Logic-based LSC consistency checking. / Guo, Hai Feng; Zheng, Wen; Subramaniam, Mahadevan.

PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming. 2009. p. 183-194 (PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Guo, HF, Zheng, W & Subramaniam, M 2009, L2C2: Logic-based LSC consistency checking. in PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming. PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, pp. 183-194, 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP'09, Coimbra, Portugal, 9/7/09. https://doi.org/10.1145/1599410.1599433
Guo HF, Zheng W, Subramaniam M. L2C2: Logic-based LSC consistency checking. In PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming. 2009. p. 183-194. (PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming). https://doi.org/10.1145/1599410.1599433
Guo, Hai Feng ; Zheng, Wen ; Subramaniam, Mahadevan. / L2C2 : Logic-based LSC consistency checking. PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming. 2009. pp. 183-194 (PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming).
@inproceedings{942e54b911d14646be95de9f9a752f9e,
title = "L2C2: Logic-based LSC consistency checking",
abstract = "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.",
keywords = "Live sequence chart (LSC), Logic programming, Memoization, PLAY-tree, Scenario-based programming",
author = "Guo, {Hai Feng} and Wen Zheng and Mahadevan Subramaniam",
year = "2009",
month = "11",
day = "30",
doi = "10.1145/1599410.1599433",
language = "English (US)",
isbn = "9781605585680",
series = "PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming",
pages = "183--194",
booktitle = "PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming",

}

TY - GEN

T1 - L2C2

T2 - Logic-based LSC consistency checking

AU - Guo, Hai Feng

AU - Zheng, Wen

AU - Subramaniam, Mahadevan

PY - 2009/11/30

Y1 - 2009/11/30

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

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

ER -