More Web Proxy on the site http://driver.im/

Article

Free access

Action Language: a specification language for model checking reactive systems

Author:

Tevfik BultanAuthors Info & Claims

ICSE '00: Proceedings of the 22nd international conference on Software engineering

Pages 335 - 344

https://doi.org/10.1145/337180.337219

Published: 01 June 2000 Publication History

Abstract

We present a specification language called Action Language for model checking software specifications. Action Language forms an interface between transition system models that a model checker generates and high level specification languages such as Statecharts, RSML and SCR—similar to an assembly language between a microprocessor and a programming language. We show that Action Language translations of Statecharts and SCR specifications are compact and they preserve the structure of the original specification. Action Language allows specification of both synchronous and asynchronous systems. It also supports modular specifications to enable compositional model checking.

References

[1]

R. Alur and T. A. Henzinger. Reactive modules. Formal Methods in System Design, 15:7{48, July 1999.

Digital Library

[2]

J. M. Atlee and J. Gannon. State-based model checking of event-driven system requirements. IEEE Transactions on Software Engineering, 19(1):24{40, January 1993.

Digital Library

[3]

R. Bharadwaj and C. Heitmeyer. Verifying SCR requirements speci cations using state exploration. In Proceedings of First ACM SIGPLAN Workshop on Automatic Analysis of Software, January 1997.

[4]

R. Bharadwaj and C. Heitmeyer. Model checking complete requirements speci cations using abstractions. Automated Software Engineering, 6(1):37{ 68, January 1999.

Digital Library

[5]

R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677{691, 1986.

Digital Library

[6]

T. Bultan, J. Fischer, and R. Gerber. Compositional veri cation by model checking for counterexamples. In Proceedings of the 1996 ACM SIG-

Digital Library

[7]

T. Bultan, R. Gerber, and C. League. Verifying systems with integer constraints and boolean predicates: A composite approach. In Proceedings of the 1998 ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 113{123, March 1998.

Digital Library

[8]

J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. H. Hwang. Symbolic model checking: 10 20 states and beyond. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, pages 428{439, January 1990.

[9]

W. Chan, R. J. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J. D. Reese. Model checking large software specifications. IEEE Transactions on Software Engineering, 24(7):498{520, July 1998.

Digital Library

[10]

E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification ofnite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244{263, April 1986.

Digital Library

[11]

E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512{ 1542, September 1994.

Digital Library

[12]

E. M. Clarke and R. P. Kurshan. Computer aided verification. IEEE Spectrum, pages 61{67, June 1996.

Digital Library

[13]

A. Coen-Porisini, C. Ghezzi, and R. A. Kemmerer. Specification of real-time systems using ASTRAL. IEEE Transactions on Software Engineering, 23(9):572{598, September 1997.

[14]

D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems, 19(2):253{291, March 1997.

Digital Library

[15]

D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3):231{274, June 1987.

Digital Library

[16]

C. L. Heitmeyer, R. D. Jeords, and B. G. Labaw. Automated consistency checking of requirements specifications. ACM Transactions on Software Engineering and Methodology, 5(3):231{261, July 1996.

Digital Library

[17]

C. L. Heitmeyer, J. Kirby, B. Labaw, M. Archer, and R. Bharadwaj. Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Transactions on Software Engineering, 24(11):927{948, November 1998.

Digital Library

[18]

G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279{ 295, May 1997.

Digital Library

[19]

L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872{923, May 1994.

Digital Library

[20]

N. Leveson, M. Heimdahl, H. Hildreth, and J. Reese. Requirements specifications of processcontrol systems. IEEE Transactions on Software Engineering, 20(9), September 1994.

Digital Library

[21]

K. L. McMillan. Symbolic model checking. Kluwer Academic Publishers, Massachusetts, 1993.

Digital Library

[22]

A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45{60, 1981.

[23]

T. Sreemani and J. M. Atlee. Feasibility of model checking software requirements: A case study. In Proceedings of the 11th Annual Conference Computer Assurance, pages 77{88, June 1996.

[24]

M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of First IEEE Symposium on Logic Computer Science, pages 322{331, 1986.

Cited By

Brizzio MSánchez C(2023)Efficient Reactive Synthesis Using Mode DecompositionTheoretical Aspects of Computing – ICTAC 202310.1007/978-3-031-47963-2_16(256-275)Online publication date: 23-Nov-2023
https://doi.org/10.1007/978-3-031-47963-2_16
Zhang YGuo Y(2019)Runtime Monitoring of IoT Services to Guarantee PropertiesIntegrating and Streamlining Event-Driven IoT Services10.4018/978-1-5225-7622-8.ch007(223-275)Online publication date: 2019
https://doi.org/10.4018/978-1-5225-7622-8.ch007
Zhang YGuo Y(2019)Coordinating Stateful IoT Resources as Event-Driven Distributed IoT ServicesIntegrating and Streamlining Event-Driven IoT Services10.4018/978-1-5225-7622-8.ch005(140-175)Online publication date: 2019
https://doi.org/10.4018/978-1-5225-7622-8.ch005
Show More Cited By

Index Terms

Action Language: a specification language for model checking reactive systems
1. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Requirements analysis
  2. 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

A semantic model of a small typed functional language using Object-Z
APSEC '00: Proceedings of the Seventh Asia-Pacific Software Engineering Conference

The Object-Z notation is a good meta-language that can be used to specify the denotational semantics of programming languages. It has been effectively applied to some categories of languages. These include the procedural languages, the object-oriented ...
Operational specification with joint actions: serializable databases
Special issue: Specification of concurrent systems

Joint actions are introduced as a language basis for operational specification of reactive systems. Joint action systems are closed systems with no communication primitives. Their nondeterministic execution model is based on multi-party actions without ...
A Formal Framework for ASTRAL Intralevel Proof Obligations

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICSE '00: Proceedings of the 22nd international conference on Software engineering

June 2000

843 pages

ISBN:1581132069

DOI:10.1145/337180

Chairmen:
Carlo Ghezzi
Politecnico di Milano, Milau, Italy
,
Mehdi Jazayeri
Technical Univ. of Vienna, Vienna, Austria
,
Alexander L. Wolf
Univ. of Colorado, Boulder, USA

Copyright © 2000 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]

Sponsors

Irish Comp Soc: Irish Computer Society
SIGSOFT: ACM Special Interest Group on Software Engineering
IEEE-CS: Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 June 2000

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICSE00

Sponsor:

Irish Comp Soc
SIGSOFT
IEEE-CS

ICSE00: 22nd International Conference on Software Engineering

June 4 - 11, 2000

Limerick, Ireland

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
689
Total Downloads

Downloads (Last 12 months)61
Downloads (Last 6 weeks)8

Reflects downloads up to 20 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Brizzio MSánchez C(2023)Efficient Reactive Synthesis Using Mode DecompositionTheoretical Aspects of Computing – ICTAC 202310.1007/978-3-031-47963-2_16(256-275)Online publication date: 23-Nov-2023
https://doi.org/10.1007/978-3-031-47963-2_16
Zhang YGuo Y(2019)Runtime Monitoring of IoT Services to Guarantee PropertiesIntegrating and Streamlining Event-Driven IoT Services10.4018/978-1-5225-7622-8.ch007(223-275)Online publication date: 2019
https://doi.org/10.4018/978-1-5225-7622-8.ch007
Zhang YGuo Y(2019)Coordinating Stateful IoT Resources as Event-Driven Distributed IoT ServicesIntegrating and Streamlining Event-Driven IoT Services10.4018/978-1-5225-7622-8.ch005(140-175)Online publication date: 2019
https://doi.org/10.4018/978-1-5225-7622-8.ch005
Zhang YChen J(2019)Declarative Construction of Distributed Event-driven IoT Services Based on IoT Resource ModelsIEEE Transactions on Services Computing10.1109/TSC.2017.2782794(1-1)Online publication date: 2019
https://doi.org/10.1109/TSC.2017.2782794
Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
Zhang YChen JHamdan HToral-Cruz HAkleylek SMcheick HBoubiche D(2017)Modeling virtual channel to enforce runtime properties for IoT servicesProceedings of the Second International Conference on Internet of things, Data and Cloud Computing10.1145/3018896.3025150(1-17)Online publication date: 22-Mar-2017
https://dl.acm.org/doi/10.1145/3018896.3025150
Kim DHong J(2015)ESUML-EAFSoftware and Systems Modeling (SoSyM)10.1007/s10270-013-0337-514:2(795-812)Online publication date: 1-May-2015
https://dl.acm.org/doi/10.1007/s10270-013-0337-5
Rochd AZrikem MAyadi APercebois CMillan TBaron C(2014)Implementing and validating SynchSPEM: A solution for synchronizing activities and products within a software engineering process2014 International Conference on Multimedia Computing and Systems (ICMCS)10.1109/ICMCS.2014.6911272(1071-1076)Online publication date: Apr-2014
https://doi.org/10.1109/ICMCS.2014.6911272
Jebali FLang FMateescu R(2014)GRL: A Specification Language for Globally Asynchronous Locally Synchronous SystemsFormal Methods and Software Engineering10.1007/978-3-319-11737-9_15(219-234)Online publication date: 2014
https://doi.org/10.1007/978-3-319-11737-9_15
Faghih FGlinz MMurphy GPezzè M(2012)Model translations among big-step modeling languagesProceedings of the 34th International Conference on Software Engineering10.5555/2337223.2337483(1555-1558)Online publication date: 2-Jun-2012
https://dl.acm.org/doi/10.5555/2337223.2337483
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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

Media

Figures

Other

Tables

View Table of Contents