article

Fluent model checking for event-based systems

Authors:

Dimitra Giannakopoulou,

Jeff MageeAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 28, Issue 5

Pages 257 - 266

https://doi.org/10.1145/949952.940106

Published: 01 September 2003 Publication History

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]

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.]]

Digital Library

[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.]]

Digital Library

[4]

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.]]

Digital Library

[5]

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.]]

Digital Library

[6]

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.]]

Digital Library

[7]

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.]]

Digital Library

[8]

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.]]

Digital Library

[9]

R. De Nicola and F. W. Vaandrager, Three Logics for branching bisimulation, Journal of the ACM, Vol. 42, No. 2, pp. 458--487, 1995.]]

Digital Library

[10]

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.]]

Digital Library

[11]

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.]]

Digital Library

[12]

D. Giannakopoulou, Model Checking for Concurrent Software Architectures, PhD Thesis, Dept. of Computing. Imperial College London, 1999.]]

[13]

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.]]

Digital Library

[14]

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.]]

Digital Library

[15]

C. A. R. Hoare, Communicating sequential processes, Prentice-Hall International, 1985.]]

Digital Library

[16]

G. J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, Vol. 23, No. 5, pp. 279--295, 1997.]]

Digital Library

[17]

J. E. Hopcroft and J. D. Ullman, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, 1979.]]

Digital Library

[18]

R. A. Kowalski and M. Sergot, A Logic-Based Calculus of Events, New Generation Computing, Vol. 4, No. 1, pp. 67--95, 1986.]]

Digital Library

[19]

L. Lamport, The Temporal Logic of Actions, ACM Transactions on Programming Languages and Systems, Vol. 16, No. 3, pp. 872--923, 1994.]]

Digital Library

[20]

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.]]

Digital Library

[21]

J. Magee and J. Kramer, Concurrency - State Models & Java Programs, John Wiley & Sons, 1999.]]

Digital Library

[22]

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.]]

Digital Library

[23]

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.]]

Digital Library

[24]

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.]]

Digital Library

[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, 1989.]]

Digital Library

[27]

D. O. Paun and M. Chechik, Events in Linear-Time Properties, 4th IEEE International Symposium on Requirements Engineering (RE '99), Limerick, Ireland, June 1999.]]

Digital Library

[28]

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.]]

Digital Library

[29]

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.]]

Digital Library

[30]

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.]]

Digital Library

[31]

A. W. Roscoe, A Classical Mind: Essays in Honour of C.A.R. Hoare, pp. 353--378, Prentice-Hall, 1994.]]

Digital Library

[32]

E. Sandewall, Features and Fluents: The Representation of Knowledge about Dynamical Systems, Oxford University Press, 1994.]]

Digital Library

[33]

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.]]

Digital Library

[34]

R. van Ommering, Horizontal Communication: a Style to Compose Control Software, Philips Research Laboratories, (to appear in Software Practice & Experience, Wiley 2003).]]

Digital Library

[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.]]

Cited By

Arioka YYamauchi TTei K(2023)Pre-controller Synthesis for Runtime Controller Synthesis2023 IEEE 13th International Conference on Control System, Computing and Engineering (ICCSCE)10.1109/ICCSCE58721.2023.10237143(161-166)Online publication date: 25-Aug-2023
https://doi.org/10.1109/ICCSCE58721.2023.10237143
Li JTei K(2022)Done is better than perfect: Iterative Adaptation via Multi-grained Requirement Relaxation2022 IEEE 30th International Requirements Engineering Conference (RE)10.1109/RE54965.2022.00043(288-294)Online publication date: Aug-2022
https://doi.org/10.1109/RE54965.2022.00043
Abd Alrahman YAzzopardi SPiterman N(2022)Model Checking Reconfigurable Interacting SystemsLeveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning10.1007/978-3-031-19759-8_23(373-389)Online publication date: 17-Oct-2022
https://doi.org/10.1007/978-3-031-19759-8_23
Show More Cited By

Index Terms

Fluent model checking for event-based systems
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking

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 engineering

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 ...
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 engineering

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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 28, Issue 5

September 2003

382 pages

ISSN:0163-5948

DOI:10.1145/949952

Issue’s Table of Contents

ESEC/FSE-11: Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering
September 2003
394 pages
ISBN:1581137435
DOI:10.1145/940071
General Chair:
Jukka Paakki
University of Helsinki, Finland
,
Program Chair:
Paola Inverardi
University of L'Aquila, Italy

Copyright © 2003 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 ACM 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 September 2003

Published in SIGSOFT Volume 28, Issue 5

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

134
Total Citations
View Citations
1,366
Total Downloads

Downloads (Last 12 months)21
Downloads (Last 6 weeks)2

Reflects downloads up to 22 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Arioka YYamauchi TTei K(2023)Pre-controller Synthesis for Runtime Controller Synthesis2023 IEEE 13th International Conference on Control System, Computing and Engineering (ICCSCE)10.1109/ICCSCE58721.2023.10237143(161-166)Online publication date: 25-Aug-2023
https://doi.org/10.1109/ICCSCE58721.2023.10237143
Li JTei K(2022)Done is better than perfect: Iterative Adaptation via Multi-grained Requirement Relaxation2022 IEEE 30th International Requirements Engineering Conference (RE)10.1109/RE54965.2022.00043(288-294)Online publication date: Aug-2022
https://doi.org/10.1109/RE54965.2022.00043
Abd Alrahman YAzzopardi SPiterman N(2022)Model Checking Reconfigurable Interacting SystemsLeveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning10.1007/978-3-031-19759-8_23(373-389)Online publication date: 17-Oct-2022
https://doi.org/10.1007/978-3-031-19759-8_23
Asteasuain FCaldeira L(2022)A Sound and Correct Formalism to Specify, Verify and Synthesize Behavior in BIG DATA SystemsComputer Science – CACIC 202110.1007/978-3-031-05903-2_8(109-123)Online publication date: 20-May-2022
https://doi.org/10.1007/978-3-031-05903-2_8
Yamauchi THirano TLi JKawasaki TChen YTsuge AOkoshi TNakazawa JYoshioka NPalaiokrassas GLitke ATei K(2021)A Development Method for Safe Node-RED Systems using Discrete Controller Synthesis2021 IEEE International Conferences on Internet of Things (iThings) and IEEE Green Computing & Communications (GreenCom) and IEEE Cyber, Physical & Social Computing (CPSCom) and IEEE Smart Data (SmartData) and IEEE Congress on Cybermatics (Cybermatics)10.1109/iThings-GreenCom-CPSCom-SmartData-Cybermatics53846.2021.00033(130-137)Online publication date: Dec-2021
https://doi.org/10.1109/iThings-GreenCom-CPSCom-SmartData-Cybermatics53846.2021.00033
Seow K(2021)Supervisory Control of Fair Discrete-Event Systems: A Canonical Temporal Logic FoundationIEEE Transactions on Automatic Control10.1109/TAC.2020.303715666:11(5269-5282)Online publication date: Nov-2021
https://doi.org/10.1109/TAC.2020.3037156
Maoz SRingert J(2021)Spectra: a specification language for reactive systemsSoftware and Systems Modeling10.1007/s10270-021-00868-zOnline publication date: 14-Apr-2021
https://doi.org/10.1007/s10270-021-00868-z
Kumazawa TTakimoto MKambayashi Y(2020)A Survey on the Applications of Swarm Intelligence to Software VerificationHandbook of Research on Fireworks Algorithms and Swarm Intelligence10.4018/978-1-7998-1659-1.ch017(376-398)Online publication date: 2020
https://doi.org/10.4018/978-1-7998-1659-1.ch017
Fujikura TKurachi R(2020)A Simultaneous Attack Scenario Generation Method Using the Parallel Behavior Model2020 IEEE 91st Vehicular Technology Conference (VTC2020-Spring)10.1109/VTC2020-Spring48590.2020.9129076(1-7)Online publication date: May-2020
https://doi.org/10.1109/VTC2020-Spring48590.2020.9129076
Li JAizawa KTei KHoniden S(2020)Efficient Difference Analysis Algorithm for Runtime Requirement Degradation under System Functional Fault2020 IEEE 18th International Conference on Embedded and Ubiquitous Computing (EUC)10.1109/EUC50751.2020.00012(33-40)Online publication date: Dec-2020
https://doi.org/10.1109/EUC50751.2020.00012
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents