LeeTL: LTL with quantifications over model objects
Pages 41 - 49
Abstract
Dynamic creating of objects and processes as one of the widely used techniques for developing models does not support by the majority of model checking tools. In addition, although there exist few model checking tools which support dynamic creation of model elements, e.g. Spin, they do not provide a property language for presenting the behavioral specifications of dynamically created elements. In this paper, we address this shortage and provide proper support for the model checking of object-based models which contain dynamic object creation. To this aim, we propose LeeTL, a new temporal logic that supports quantifications over model objects. Using LeeTL, it is also possible to traverse objects to access the variables of the objects for defining property formulas. We propose an algorithm for transforming LeeTL formulas to Büchi automata to be able to use the existing model checking tools which support Büchi automata.
References
[1]
Joe Armstrong. 1997.
[2]
The development of Erlang. SIGPLAN Not. 32 (August 1997), 196–203. Issue 8.
[3]
Christel Baier and Joost-Pieter Katoen. 2008.
[4]
Principles of Model Checking. MIT Press. I–XVII, 1–975 pages.
[5]
James C Corbett, Matthew B Dwyer, John Hatcliff, and others. 2002. Expressing checkable properties of dynamic systems: the Bandera Specification Language. International Journal on Software Tools for Technology Transfer 4, 1 (2002), 34–56.
[6]
Claudio Demartini, Radu Iosif, and Riccardo Sisto. 1999.
[7]
dSPIN: A Dynamic Extension of SPIN. In Theoretical and Practical Aspects of SPIN Model Checking, 5th and 6th International SPIN Workshops, Trento, Italy, July 5, 1999, Toulouse, France, September 21 and 24 1999, Proceedings (Lecture Notes in Computer Science), Dennis Dams, Rob Gerth, Stefan Leue, and Mieke Massink (Eds.), Vol. 1680.
[8]
Springer, 261–276.
[9]
Dino Distefano, Joost-Pieter Katoen, and Arend Rensink. 2005. Who is pointing when to whom? In FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science. Springer Berlin Heidelberg, 250–262.
[10]
Rob Gerth, Doron Peled, Moshe Y Vardi, and Pierre Wolper. 1995. Simple onthe-fly automatic verification of linear temporal logic. In Proceedings of the Fifteenth IFIP WG6. 1 International Symposium on Protocol Specification, Testing and Verification. IFIP. LeeTL: LTL with Quantifications over Model Objects SPIN’17, July 2017, Santa Barbara, CA, USA
[11]
Dimitra Giannakopoulou and Flavio Lerda. 2002.
[12]
From states to transitions: Improving translation of LTL formulae to B üchi automata. In Formal Techniques for Networked and Distributed SytemsfiFORTE 2002. Springer, 308–326.
[13]
Klaus Havelund and Grigore Rosu. 2004. An Overview of the Runtime Verification Tool Java PathExplorer. Formal Methods in System Design 24, 2 (2004), 189–215.
[14]
Klaus Havelund and Grigore Rosu. 2004. An Overview of the Runtime Verification Tool Java PathExplorer. Formal Methods in System Design 24, 2 (2004), 189–215.
[15]
Gerard J. Holzmann. 1997. The Model Checker SPIN. IEEE Trans. Software Eng. 23, 5 (1997), 279–295.
[16]
Radu Iosif and Riccardo Sisto. 2003. Temporal logic properties of Java objects. Journal of Systems and Software 68, 3 (2003), 243–251.
[17]
Mohammad Mahdi Jaghoori, Marjan Sirjani, Mohammad Reza Mousavi, Ehsan Khamespanah, and Ali Movaghar. 2010. Symmetry and Partial Order Reduction Techniques in Model Checking Rebeca. Acta Inf. 47, 1 (2010), 33–66.
[18]
Hamideh Sabouri and Marjan Sirjani. 2008. Slicing-Based Reductions for Rebeca. In Proceedings of FACS 2008. ENTCS.
[19]
Marjan Sirjani. 2007. Rebeca: Theory, applications, and tools. In Formal Methods for Components and Objects. Springer, 102–126.
[20]
Marjan Sirjani, Frank S. de Boer, and Ali Movaghar-Rahimabadi. 2005. Modular Verification of a Component-Based Actor Language. J. UCS 11, 10 (2005), 1695– 1717.
[21]
Marjan Sirjani and Mohammad Mahdi Jaghoori. 2011. Ten Years of Analyzing Actors: Rebeca Experience. In Formal Modeling: Actors, Open Systems, Biological Systems. 20–56.
[22]
Fu Song and Zhilin Wu. 2016. On temporal logics with data variable quantifications: Decidability and complexity. Inf. Comput. 251 (2016), 104–139.
Index Terms
- LeeTL: LTL with quantifications over model objects
Recommendations
Regular model checking for LTL(MSO)
Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of ...
Rebeca: theory, applications, and tools
FMCO'06: Proceedings of the 5th international conference on Formal methods for components and objectsRebeca is an actor-based language with a formal foundation for modeling concurrent and distributed systems which is designed in an effort to bridge the gap between formal verification approaches and real applications. Rebeca is supported by a tool-set ...
LTL satisfiability checking
We report here on an experimental investigation of LTL satisfiability checking via a reduction to model checking. By using large LTL formulas, we offer challenging model-checking benchmarks to both explicit and symbolic model checkers. For symbolic ...
Comments
Information & Contributors
Information
Published In
July 2017
199 pages
Copyright © 2017 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 13 July 2017
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
Conference
ISSTA '17
Sponsor:
ISSTA '17: International Symposium on Software Testing and Analysis
July 13 - 14, 2017
CA, Santa Barbara, USA
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 54Total Downloads
- Downloads (Last 12 months)1
- Downloads (Last 6 weeks)1
Reflects downloads up to 09 Mar 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in