Dimitra Giannakopoulou
Skip Abstract Section
Abstract
Model checking is an automated technique for verifying that a system satisfies a set of required properties. Such properties are typically expressed as temporal logic formulas, in which atomic propositions are predicates over state variables of the system. In event-based system descriptions, states are not characterized by state variables, but rather by the behavior that originates in these states in terms of actions. In this context, it is natural for temporal formulas to be built from atomic propositions that are predicates on the occurrence of actions. The paper identifies limitations in this approach and introduces "fluent" propositions that permit formulas to naturally express properties that combine state and action. A fluent is a property of the world that holds after it is initiated by an action and ceases to hold when terminated by another action. The paper describes an approach to model checking fluent-based linear-temporal logic properties, with its implementation and application in the LTSA tool.
- R. Allen and D. Garlan, A Formal Basis for Architectural Connection, ACM Trans. on Software Engineering and Methodology (TOSEM), Vol. 6, No. 3, pp. 213--249, 1997.]] Google Scholar
Digital Library
- B. Alpern and F. Schneider, Defining Liveness, Information Processing Letters, Vol. 21, No. 4, pp. 181--185, Oct. 1985.]]Google ScholarCross Ref
- B. Alpern and F. B. Schneider, Recognizing Safety and Liveness, Distributed Computing, Vol. 2, No. 3, pp. 117--126, 1987.]]Google ScholarDigital Library
- M. Bernardo, P. Ciancarini and L. Donatiello, Architecting Software Systems with Process Algebras, ACM Trans. on Software Engineering and Methodology (TOSEM), Vol. 11, No. 4, October 2002.]] Google ScholarDigital Library
- S. C. Cheung and J. Kramer, Checking Subsystem Safety Properties in Compositional Reachability Analysis, 18th International Conference on Software Engineering (ICSE'18), Berlin, Germany, pp. 144--154, March 1996.]] Google ScholarDigital Library
- E. M. Clarke and E. A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, Logic of Programs Workshop, Yorktown Heights NY, LNCS 131, Springer, May 1981.]] Google ScholarDigital Library
- R. Cleaveland, J. Parrow and B. Steffen, The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems, ACM Transactions on Programming Languages and Systems, Vol. 15, No. 1, pp. 36--72, 1993.]] Google ScholarDigital Library
- M. Daniele, F. Giunchiglia and M. Y. Vardi, Improved Automata Generation for Linear Temporal Logic, 11th International Conference on Computer Aided Verification (CAV 1999), Trento, Italy, LNCS 1633, July 1999.]] Google ScholarDigital Library
- R. De Nicola and F. W. Vaandrager, Three Logics for branching bisimulation, Journal of the ACM, Vol. 42, No. 2, pp. 458--487, 1995.]] Google ScholarDigital Library
- M. Dwyer, G. Avrunin and J. Corbett, Patterns in property Specifications for Finite-State Verification, 21st International Conference on Software Engineering (ICSE'99), Los Angeles, CA, pp. 411--420, 16-22 May 1999.]] Google ScholarDigital Library
- R. Gerth, D. Peled, M. Y. Vardi and P. Wolper, Simple On-the-fly Automatic Verification of Linear Temporal Logic, 15th IFIP/WG6.1 Symposium on Protocol Specification, Testing and Verification (PSTV'95), Warsaw, Poland, pp. 3--18, June 1995.]] Google ScholarDigital Library
- D. Giannakopoulou, Model Checking for Concurrent Software Architectures, PhD Thesis, Dept. of Computing. Imperial College London, 1999.]]Google Scholar
- D. Giannakopoulou and F. Lerda, From States to Transitions: Improving translation of LTL formulae to Büchi automata, 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2002), Houston, Texas, LNCS 2529, November 2002.]] Google ScholarDigital Library
- D. Giannakopoulou, J. Magee and J. Kramer, Checking Progress with Action Priority: Is it Fair?, 7th European Software Engineering Conference held jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE'99), Toulouse, France, LNCS 1687, pp. 511--527, September 1999.]] Google ScholarDigital Library
- C. A. R. Hoare, Communicating sequential processes, Prentice-Hall International, 1985.]] Google ScholarDigital Library
- G. J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, Vol. 23, No. 5, pp. 279--295, 1997.]] Google ScholarDigital Library
- J. E. Hopcroft and J. D. Ullman, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, 1979.]] Google ScholarDigital Library
- R. A. Kowalski and M. Sergot, A Logic-Based Calculus of Events, New Generation Computing, Vol. 4, No. 1, pp. 67--95, 1986.]] Google ScholarDigital Library
- L. Lamport, The Temporal Logic of Actions, ACM Transactions on Programming Languages and Systems, Vol. 16, No. 3, pp. 872--923, 1994.]] Google ScholarDigital Library
- J. Magee, N. Dulay, S. Eisenbach and J. Kramer, Specifying Distributed Software Architectures, 5th European Software Engineering Conference (ESEC'95), Sitges, Spain, LNCS 989, pp. 137--153, September 1995.]] Google ScholarDigital Library
- J. Magee and J. Kramer, Concurrency - State Models & Java Programs, John Wiley & Sons, 1999.]] Google ScholarDigital Library
- J. Magee, J. Kramer and D. Giannakopoulou, Behaviour Analysis of Software Architectures, 1st Working IFIP Conference on Software Architecture (WICSA1), San Antonio, TX, USA, 22-24 February 1999.]] Google ScholarDigital Library
- J. Magee, N. Pryce, D. Giannakopoulou and J. Kramer, Graphical Animation of Behavior Models, 22d International Conference on Software Engineering (ICSE'2000), Limerick, Ireland, June 2000.]] Google ScholarDigital Library
- Michael Leuschel, Thierry Massart and A. Currie, How to Make FDR Spin: LTL Model Checking using Refinement, International Symposium of Formal Methods Europe (FME'2001), LNCS 2021, Berlin, Germany, 2001.]] Google ScholarDigital Library
- R. Miller and M. Shanahan, The Event Calculus in Classical Logic - Alternative Axiomatisations, Linkoping Electronic Articles in Computer and Information Science, Vol. 4, No. 16, pp. 1--27, 1999.]]Google Scholar
- R. Milner, Communication and Concurrency, Prentice-Hall, 1989.]] Google ScholarDigital Library
- D. O. Paun and M. Chechik, Events in Linear-Time Properties, 4th IEEE International Symposium on Requirements Engineering (RE '99), Limerick, Ireland, June 1999.]] Google ScholarDigital Library
- D. Peled, Combining Partial Order Reductions with On-the-Fly Model Checking, 6th International Conference on Computer Aided Verification (CAV'94), Stanford, California, LNCS 818, pp. 377--390, June 1994.]] Google ScholarDigital Library
- J.-P. Queille and J. Sifakis, Specification and verification of concurrent systems in CESAR, 5th International Symposium on Programming, LNCS 137, pp. 337--350, April 1982.]] Google ScholarDigital Library
- Y. S. Ramakrishna and S. A. Smolka, Partial-Order Reduction in the Weak Modal Mu-Calculus, Eighth International Conference on Concurrency Theory (CONCUR '97), Warsaw, Poland, LNCS 1243, pp. 5--24, July 1997.]] Google ScholarDigital Library
- A. W. Roscoe, A Classical Mind: Essays in Honour of C.A.R. Hoare, pp. 353--378, Prentice-Hall, 1994.]] Google ScholarDigital Library
- E. Sandewall, Features and Fluents: The Representation of Knowledge about Dynamical Systems, Oxford University Press, 1994.]] Google ScholarDigital Library
- A. Valmari, On-the-fly Verification with Stubborn Sets, 5th International Conference on Computer-Aided Verification (CAV'93), Elounda, Greece, LNCS 697, pp. 397--408, 1993.]] Google ScholarDigital Library
- R. van Ommering, Horizontal Communication: a Style to Compose Control Software, Philips Research Laboratories, (to appear in Software Practice & Experience, Wiley 2003).]] Google ScholarDigital Library
- M. Y. Vardi and P. Wolper, An automata-theoretic approach to automatic program verification, 1st Symposium on Logic in Computer Science (LICS), Cambridge, June 1986.]]Google Scholar
Index Terms
- Fluent model checking for event-based systems
Recommendations
Fluent model checking for event-based systems
ESEC/FSE-11: Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineeringModel checking is an automated technique for verifying that a system satisfies a set of required properties. Such properties are typically expressed as temporal logic formulas, in which atomic propositions are predicates over state variables of the ...
Fluent temporal logic for discrete-time event-based models
Fluent model checking is an automated technique for verifying that an event-based operational model satisfies some state-based declarative properties. The link between the event-based and state-based formalisms is defined through "fluents" which are ...
Fluent temporal logic for discrete-time event-based models
ESEC/FSE-13: Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineeringFluent model checking is an automated technique for verifying that an event-based operational model satisfies some state-based declarative properties. The link between the event-based and state-based formalisms is defined through "fluents" which are ...
Comments