Fluent temporal logic for discrete-time event-based models

ABSTRACT

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 state predicates whose value are determined by the occurrences of initiating and terminating events that make the fluents values become true or false, respectively.The existing fluent temporal logic is convenient for reasoning about untimed event-based models but difficult to use for timed models. The paper extends fluent temporal logic with temporal operators for modelling timed properties of discrete-time event-based models. It presents two approaches that differ on whether the properties model the system state after the occurrence of each event or at a fixed time rate. Model checking of timed properties is made possible by translating them into the existing untimed framework.

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: M. Bernardo , P. Ciancarini , L. Donatiello, Architecting Software Systems with Process Algebras, University of Bologna, 2001
• 3: 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]
• 4: 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]
• 5: Dimitra Giannakopoulou , Jeff Magee, Fluent model checking for event-based systems, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 6: Thomas A. Henzinger, It's About Time: Real-Time Logics Reviewed, Proceedings of the 9th International Conference on Concurrency Theory, p.439-454, September 08-11, 1998
• 7: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 8: 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]
• 9: Gerard J. Holzmann, The logic of bugs, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587064]
• 10: M. Joseph, Real-Time Systems: Specification, Verification and Analysis. Prentice Hall, 1996.
• 11: J. Kramer, J. Magee, M. Sloman et al, CONIC: an Integrated Approach to Distributed Computer Control Systems. IEE Proceedings, Part E 130, 1, January 1983.
• 12: Ron Koymans, Specifying Message Passing and Time-Critical Systems with Temporal Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1992
• 13: 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]
• 14: Axel van Lamsweerde, Requirements engineering in the year 00: a research perspective, Proceedings of the 22nd international conference on Software engineering, p.5-19, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337184]
• 15: E. Letier, Reasoning about Agents in Goal-Oriented Requirements Engineering. Ph. D. Thesis, University of Louvain, May 2001.
• 16: 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
• 17: Jeff Magee , Jeff Kramer, Concurrency: state models & Java programs, John Wiley & Sons, Inc., New York, NY, 2000
• 18: 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]
• 19: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 20: R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 21: 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.
• 22: S. Queins et al., The Light Control Case Study: Problem Description, Journal of Universal Computer Science, Special Issue on Requirements Engineering: the Light Control Case Study, Vol.6(7), 2000.
• 23: A. W. Roscoe, Model-checking CSP, A classical mind: essays in honour of C. A. R. Hoare, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1994

INDEX TERMS

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

General Terms:
Theory, Verification

Keywords:
discrete-time event-based models, fluent linear temporal logic, model-checking, software architecture analysis