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 - Dec 1 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

Fingerprint

simulator
Specifications
Logic programming
Testing
Computer programming languages
Simulators
test

ASJC Scopus subject areas

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

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.

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

2009. Paper presented at 19th Workshop on Logic-based methods in Programming Environments, WLPE 2009, Pasadena, CA, United States.

Research output: Contribution to conferencePaper

Guo, HF, 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, 7/14/09 - 7/14/09, .
Guo HF, Zheng W, Subramaniam M. L2C2: Logic-based LSC consistency checking. 2009. Paper presented at 19th Workshop on Logic-based methods in Programming Environments, WLPE 2009, Pasadena, CA, United States.
Guo, Hai Feng ; Zheng, Wen ; Subramaniam, Mahadevan. / L2C2 : Logic-based LSC consistency checking. Paper presented at 19th Workshop on Logic-based methods in Programming Environments, WLPE 2009, Pasadena, CA, United States.
@conference{3c456cc305494f8ba5de26d36fe3b6f2,
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.",
author = "Guo, {Hai Feng} and Wen Zheng and Mahadevan Subramaniam",
year = "2009",
month = "12",
day = "1",
language = "English (US)",
note = "19th Workshop on Logic-based methods in Programming Environments, WLPE 2009 ; Conference date: 14-07-2009 Through 14-07-2009",

}

TY - CONF

T1 - L2C2

T2 - Logic-based LSC consistency checking

AU - Guo, Hai Feng

AU - Zheng, Wen

AU - Subramaniam, Mahadevan

PY - 2009/12/1

Y1 - 2009/12/1

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.

UR - http://www.scopus.com/inward/record.url?scp=84886670463&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84886670463&partnerID=8YFLogxK

M3 - Paper

AN - SCOPUS:84886670463

ER -