L2C2

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

L2C2: logic-based LSC consistency checking

Full text

Pdf (1.05 MB)

Source

International Conference on Principles and Practice of Declarative Programming archive
Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming table of contents

Coimbra, Portugal

SESSION: Logic programming table of contents

Pages 183-194

Year of Publication: 2009

ISBN:978-1-60558-568-0

Authors

Hai-Feng Guo	University of Nebraska at Omaha, Omaha, NE, USA
Wen Zheng	University of Nebraska at Omaha, Omaha, NE, USA
Mahadevan Subramaniam	University of Nebraska at Omaha, Omaha, NE, USA

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
ACM: Association for Computing Machinery

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 5, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1599410.1599433 What is a DOI?

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.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Harvey Abramson: Definite Clause Translation Grammars. International Symposium on Logic Programming, pp. 233--240., 1984.
	2	J. Bohn, W. Damm, J. Klose, A. Moik, and H. Wittke: Modeling and validating train system applications using statemate and live sequence charts. The 6th Biennial World Conference on Integrated Design and Process Technology, 2002.
	3	Y. Bontemps, P. Heymans: Turning high-level live sequence charts into automata. Proceedings of Scenarios and State-Machines: Models, Algorithms, and Tools, 2002.
	4	Y. Bontemps, P. Heymans, H. Kugler: Applying LSCs to the specification of an air traffic control system. Workshop on Scenarios and State Machines: Models, Algorithms and Tools, 2003.
	5	A. Bunker, G. Gopalakrishnan, and K. Slind: Live Sequence Charts Applied to Hardware Requirements Specification and Verification: A VCI Bus Interface Model. Software Tools for Technology Transfer, 7(4):341--350, 2005.
	6	E.M. Clarke, O. Grumberg, and D.A. Peled: Model Checking. The MIT Press, 2001.
	7	P. Combes, D. Harel, and H. Kugler: Modeling and Verification of a Telecommunication Application using Live Sequence Charts and the Play-Engine Tool. The 3rd Int. Symp. on Automated Technology for Verification and Analysis, 2008.
	8	Werner Damm and David Harel: LSCs: Breathing Life into Message Sequence Charts. Proc. 3rd IFIP Int. Conf. on Formal Methods for Open Object-based Distributed Systems, pp. 293--312, 1999.
	9	G. Gupta, H.-F. Guo, E. Pontelli, and A.I. Karshmer: Semantics-based Filting: Logic Programming's Killer Application. Fourth Int. Symp. on Practical Application of Declarative Languages, pp. 80--97, 2002.
	10	David Harel: From Play-In Scenarios to Code: An Achievable Dream. Proc. Fundamental Approaches to Software Engineering (FASE), pp. 22--34, 2000.
	11	David Harel and Hillel Kugler: Synthesizing State-based object systems from LSC specifications. Int. Journal of Foundations of Computer Science, 13(1): 5--51, 2002.
	12	David Harel and Rami Marelly: Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer-Verlag, 2003.
	13	D. Harel, S. Maoz, and I Segall: Some results on the expressive power and complexity of LSCs. LNCS 4800, pp. 351--366, 2008.
	14	H. Kugler, D. Harel, A. Pnueli, Y. Lu, and Y. Bontemps: Temporal logic for scenario-based specifications. In TACAS 2005, pp. 445--460.
	15	R. Kumar and E. Mercer: Improving translation of live sequence charts to temporal logic. Int. conf. on automated verification of critical systems, pp. 183--197, 2007.
	16	R. Kumar and E. Mercer: Improving live sequence chart to automata translation for verification. Electronic Communications of the EASST, 2008.
	17	J. Klose, T. Toben, B. Westphal, and H. Wittke: Check It Out: On the Efficient Formal Verification of Live Sequence Charts. 18th International Conference on Computer Aided Verification (CAV), pp. 219--233, 2006.
	18	Jun Sun and Jin Song Dong: Model checking live sequence charts. The 10th IEEE int. conf. on Engineering of complex computer systems, 2005.
	19	T. Toben and B. Westphal: On the expressive power of LSCs. The 32nd Conf. on Current Trends in Theory and Practice of Computer Science, pp. 33--43, 2006.
	20	The Object Management Group (OMG): Documentation of the Unified Modeling Language. http://www.omg.org, 2009.
	21	UML: Unified Modeling Languages Superstructure Specification, v2.0. http://www.uml.org/, OMG specification, 2005.
	22	Z.120 ITU-T Recommendation: Message Sequence Chart (MSC). ITU-T, 1996.
	23	Wen Zheng: Consistency Checking on LSC specifications. Master Thesis, University of Nebraska at Omaha, 2009.