Fluent model checking for event-based systems

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.

REFERENCES

• 1: Robert Allen , David Garlan, A formal basis for architectural connection, ACM Transactions on Software Engineering and Methodology (TOSEM), v.6 n.3, p.213-249, July 1997 [doi>10.1145/258077.258078]
• 2: B. Alpern and F. Schneider, Defining Liveness, Information Processing Letters, Vol. 21, No. 4, pp. 181--185, Oct. 1985.
• 3: B. Alpern and F. B. Schneider, Recognizing Safety and Liveness, Distributed Computing, Vol. 2, No. 3, pp. 117--126, 1987.
• 4: Marco Bernardo , Paolo Ciancarini , Lorenzo Donatiello, Architecting families of software systems with process algebras, ACM Transactions on Software Engineering and Methodology (TOSEM), v.11 n.4, p.386-426, October 2002 [doi>10.1145/606612.606614]
• 5: Shing C. Cheung , Jeff Kramer, Checking subsystem safety properties in compositional reachability analysis, Proceedings of the 18th international conference on Software engineering, p.144-154, March 25-29, 1996, Berlin, Germany
• 6: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 7: Rance Cleaveland , Joachim Parrow , Bernhard Steffen, The concurrency workbench: a semantics-based tool for the verification of concurrent systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.36-72, Jan. 1993 [doi>10.1145/151646.151648]
• 8: Marco Daniele , Fausto Giunchiglia , Moshe Y. Vardi, Improved Automata Generation for Linear Temporal Logic, Proceedings of the 11th International Conference on Computer Aided Verification, p.249-260, July 06-10, 1999
• 9: Rocco De Nicola , Frits Vaandrager, Three logics for branching bisimulation, Journal of the ACM (JACM), v.42 n.2, p.458-487, March 1995 [doi>10.1145/201019.201032]
• 10: Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302672]
• 11: Rob Gerth , Doron Peled , Moshe Y. Vardi , Pierre Wolper, Simple on-the-fly automatic verification of linear temporal logic, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV, p.3-18, June 01, 1995
• 12: D. Giannakopoulou, Model Checking for Concurrent Software Architectures, PhD Thesis, Dept. of Computing. Imperial College London, 1999.
• 13: Dimitra Giannakopoulou , Flavio Lerda, From States to Transitions: Improving Translation of LTL Formulae to Büchi Automata, Proceedings of the 22nd IFIP WG 6.1 International Conference Houston on Formal Techniques for Networked and Distributed Systems, p.308-326, November 11-14, 2002
• 14: Dimitra Giannakopoulou , Jeff Magee , Jeff Kramer, Checking progress with action priority: is it fair?, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.511-527, September 06-10, 1999, Toulouse, France
• 15: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 16: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 17: John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 18: R Kowalski , M Sergot, A logic-based calculus of events, New Generation Computing, v.4 n.1, p.67-95, 1986 [doi>10.1007/BF03037383]
• 19: Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994 [doi>10.1145/177492.177726]
• 20: Jeff Magee , Naranker Dulay , Susan Eisenbach , Jeff Kramer, Specifying Distributed Software Architectures, Proceedings of the 5th European Software Engineering Conference, p.137-153, September 25-28, 1995
• 21: Jeff Magee , Jeff Kramer, Concurrency: state models & Java programs, John Wiley & Sons, Inc., New York, NY, 2000
• 22: Jeff Magee , Jeff Kramer , Dimitra Giannakopoulou, Behaviour Analysis of Software Architectures, Proceedings of the TC2 First Working IFIP Conference on Software Architecture (WICSA1), p.35-50, February 22-24, 1999
• 23: Jeff Magee , Nat Pryce , Dimitra Giannakopoulou , Jeff Kramer, Graphical animation of behavior models, Proceedings of the 22nd international conference on Software engineering, p.499-508, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337368]
• 24: Michael Leuschel , Thierry Massart , Andrew Currie, How to Make FDR Spin LTL Model Checking of CSP by Refinement, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.99-118, March 12-16, 2001
• 25: 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.
• 26: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 27: Dimitrie O. Paun , Marsha Chechik, Events in Linear-Time Properties, Proceedings of the 4th IEEE International Symposium on Requirements Engineering, p.123-132, June 07-11, 1999
• 28: Doron Peled, Combining Partial Order Reductions with On-the-fly Model-Checking, Proceedings of the 6th International Conference on Computer Aided Verification, p.377-390, June 21-23, 1994
• 29: Jean-Pierre Queille , Joseph Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, p.337-351, April 06-08, 1982
• 30: Y. S. Ramakrishna , Scott A. Smolka, Partial-Order Reduction in the Weak Modal Mu-Calculus, Proceedings of the 8th International Conference on Concurrency Theory, p.5-24, July 01-04, 1997
• 31: A. W. Roscoe, A classical mind: essays in honour of C. A. R. Hoare, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1994
• 32: Erik Sandewall, Features and fluents (vol. 1): the representation of knowledge about dynamical systems, Oxford University Press, Inc., New York, NY, 1995
• 33: Antti Valmari, On-the-Fly Verification with Stubborn Sets, Proceedings of the 5th International Conference on Computer Aided Verification, p.397-408, June 28-July 01, 1993
• 34: Rob van Ommering, Horizontal communication: a style to compose control software, Software—Practice & Experience, v.33 n.12, p.1117-1150, October 2003 [doi>10.1002/spe.541]
• 35: 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.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

General Terms:
Design, Languages, Verification

Keywords:
linear temporal logic, model-checking, software architecture analysis