L2C2: Logic-based LSC consistency checking

Hai Feng Guo, Wen Zheng, Mahadevan Subramaniam

Research output: Contribution to conferencePaper

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)
StatePublished - 2009
Event19th Workshop on Logic-based methods in Programming Environments, WLPE 2009 - Pasadena, CA, United States
Duration: Jul 14 2009Jul 14 2009

Conference

Conference19th Workshop on Logic-based methods in Programming Environments, WLPE 2009
CountryUnited States
CityPasadena, CA
Period7/14/097/14/09

ASJC Scopus subject areas

  • Computer Science(all)
  • Environmental Science(all)

Fingerprint Dive into the research topics of 'L2C2: Logic-based LSC consistency checking'. Together they form a unique fingerprint.

  • Cite this

    Guo, H. F., Zheng, W., & Subramaniam, M. (2009). L2C2: Logic-based LSC consistency checking. Paper presented at 19th Workshop on Logic-based methods in Programming Environments, WLPE 2009, Pasadena, CA, United States.