Article

Free access

State-based model checking of event-driven system requirements

Authors:

Joanne Atlee,

John GannonAuthors Info & Claims

SIGSOFT '91: Proceedings of the conference on Software for citical systems

Pages 16 - 28

https://doi.org/10.1145/125083.123047

Published: 01 September 1991 Publication History

PDF eReader

References

[1]

Alspaugh, T., S. Faulk, K. Britton, R. Parker, D. Parnas, J. Shore. "Software Requirements for the A-7E Aircraft." Naval Research Laboratory, March 1988.

Google Scholar

[2]

Bledsoe, W. and L. Hines. "Variable elimination and chaining in a resolution-based prover for inequalities." Proc. 5th Conf. Automated Deduction: Lecture Notes in Computer Science, W. Bibel and R. Kowalski, Eds., New York, Springer-Verlag, 1980, pp. 70-87.

Digital Library

Google Scholar

[3]

Browne, M. "Automatic Verification of Finite State Machines Using Temporal Logic." Ph.D. Thesis, Carnegie Mellon University, 1989.

Digital Library

Google Scholar

[4]

Browne, M., E. Clarke, and D. Dill. "Automatic Verification of Sequential Circuits Using Temporal Logic." IEEE Trans. on Computers, Vol. C-35, No. 12 (December 1986), pp. 1035-1044.

Digital Library

Google Scholar

[5]

Burch, J., E. Clarke, K. McMillan, D. Dill and J. Hwang. "Symbolic Model Checking: 1020 States and Beyond", Proc. of the 5th Ann. Sym. on Logic in Comp. Sci, June 1990.

Google Scholar

[6]

Clarke, E., E. Emerson, and A. Sistla. "Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications." ACM Trans. on Prog. Lang. and Sys., Vol. 8, No. 2, April 1986, pp. 244-263

Digital Library

Google Scholar

[7]

Degl'Innocenti90, M., G. Ferrari, G. Pacini, F. Turini. "RSF: A Formalism for Executable Requirements Specifications." Trans. on Software Engineering., Vol. 16, No. 11 (November 1990), pp. 1235-1246.

Digital Library

Google Scholar

[8]

Emerson, E. and A. Halpern. "'Sometimes' and 'Not Never' Revisited: On Branching Time Verses Linear Time Temporal Logic." Journal of the ACM, Vol. 33, No. 1 (January 1986), pp. 151-178.

Digital Library

Google Scholar

[9]

Emerson, E. and E. Clarke. "Using Branching Time emporal Logic to Synthesize Synchronization Skeletons." Science of Computer Programming 2, 1982, pp. 241-266.

Crossref

Google Scholar

[10]

Faulk, S. State Determination in Hard-Embedded Systems." Ph.D. Thesis University of North Carolina, Chapel Hill, North Carolina, June 1989.

Digital Library

Google Scholar

[11]

Gabrielian, A. and R. Iyer. "Integrating automata and temporal logic: a framework for specification of realtime systems." Proc. Unified Computation Laboratory, 1990.

Google Scholar

[12]

Gabrielian, A. "HMS Machines: A Unified Framework for Specification, Verification and Reasoning for Real- Time Systems." Proc. Office Naval Research 3rd Annual Workshop on Foundations of Real- Time Computing, 1990, pp. 341-358

Google Scholar

[13]

Ghezzi, C. D. Mandrioli, A. Morzenti. "TRIO, a logic language for executable specifications of real-time systems," J. of Systems and Software, Vol. 12, No. 2 (May 1990), pp. 107-123.

Digital Library

Google Scholar

[14]

Harel, D., H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. Shtull-Trauring, M. Trakhtenbrot. "STATEMATE: A Working Environment for the Development of Complex Reactive Systems." IEEE Trans. on Software Engineering, Vol. 16, No. 4 (April 1990), pp. 403-414.

Digital Library

Google Scholar

[15]

Harel, D. "Statecharts: A Visual Formalism for Complex Systems." Science of Computer Programming 8, 1987, pp. 231-274.

Digital Library

Google Scholar

[16]

Heninger, K. "Specifying Software Requirements for Complex Systems: New Techniques and Their Applications." IEEE Trans. on Software Engineering, Vol. SE-6, No. 1 (January 1980), pp. 2-12.

Digital Library

Google Scholar

[17]

Heitmeyer, C. and B. Labaw. "Consistency Checks for SCR-Style Requirements Specifications." (in preparation)

Google Scholar

[18]

Jahanian F. and A. Mok. "Safety Analysis of Timing Properties in Real-Time Systems." IEEE Trans. on Software Engineering, Vol. SE-12, No. 9 (September 1986), pp. 890-904.

Digital Library

Google Scholar

[19]

Kirby, J. "Example NRL/SCR Software Requirements for an Automobile Cruise Control and Monitoring System." Tech. Rep. TR-87-07, Wang Institute of Graduate Studies, July 1987.

Google Scholar

[20]

Manna, Z. and Pnueli, A. "Tools and Rules for the Practicing Verifier." Tech. Rep STAN-CS-90-1321, Stanford University, Stanford CA, July 1990.

Digital Library

Google Scholar

[21]

Parnas, D. and J. Madey. "Functional Documentation for Computer Systems Engineering." Tech. Rep. TR-90-287, Queen's University, Kingston, Ontario, September 1990.

Google Scholar

[22]

Ostroff, J. and W. Wonham. "Modeling, Specifying,and Verifying Real-time Embedded Computer Systems." Proc. IEEE Real- Time Systems Sym., 1987, pp. 124-132.

Google Scholar

[23]

Pnueli, A. "The Temporal Logic of Programs." Proc. of 18th Annual Sym. on the Foundation of Comp. Sci., 1977, pp. 46-57.

Google Scholar

[24]

Sistla, A., and E. Clarke. "The Complexity of Propositional Linear TemporaJ Logics." Journal of ACM, Vol. 32, No. 3 (July 1985), pp. 733-749.

Digital Library

Google Scholar

[25]

Smith, S. and S. Gerhart. "STATEMATE and Cruise Control: A Case2 Study." Proc. COMPAC '88, 12th Int. IEEE Computer Software and Application Conference., 1988, pp.49-56

Crossref

Google Scholar

[26]

van Schouwen, J. "The A-7 Requirements Model: Reexamination for Real-Time Systems and an Application to Monitoring Systems." Tech. Rep. 90-276, Queen's University, Kingston, Ontario, May 1990.

Google Scholar

[27]

van Schouwen, J. Private communications.

Google Scholar

Cited By

View all

Lin YRadoi CDig DCheung SOrso AStorey M(2014)Retrofitting concurrency for Android applications through refactoringProceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering10.1145/2635868.2635903(341-352)Online publication date: 11-Nov-2014
https://dl.acm.org/doi/10.1145/2635868.2635903
(2014)BibliographyService Orchestration As Organization10.1016/B978-0-12-800938-3.00026-6(257-272)Online publication date: 2014
https://doi.org/10.1016/B978-0-12-800938-3.00026-6
Breaux T(2010)A method to acquire compliance monitors from regulations2010 Third International Workshop on Requirements Engineering and Law10.1109/RELAW.2010.5625358(17-26)Online publication date: Sep-2010
https://doi.org/10.1109/RELAW.2010.5625358
Show More Cited By

Recommendations

State-Based Model Checking of Event-Driven System Requirements

It is demonstrated how model checking can be used to verify safety properties for event-driven systems. SCR tabular requirements describe required system behavior in a format that is intuitive, easy to read, and scalable to large systems (e.g. the ...
Analyzing tabular requirements specifications using infinite state model checking
MEMOCODE '06: Proceedings of the Fourth ACM/IEEE International Conference on Formal Methods and Models for Co-Design

This paper investigates the application of infinite state model checking to the formal analysis of requirements specifications in the SCR (software cost reduction) tabular notation using action language verifier (ALV). After reviewing the SCR method and ...
A Specification-Based Approach to Model Checking Event-Driven Systems
SoICT '19: Proceedings of the 10th International Symposium on Information and Communication Technology

An event-driven system with multiple external events is difficult to verify manually. Model checking is an appropriate approach for exhaustively and automatically verifying this kind of systems. In fact, adopting the specification language used by a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

SIGSOFT '91: Proceedings of the conference on Software for citical systems

September 1991

161 pages

ISBN:0897914554

DOI:10.1145/125083

Chairman:
Mark Moriconi
SRI International, USA

ACM SIGSOFT Software Engineering Notes Volume 16, Issue 5
Dec. 1991
161 pages
ISSN:0163-5948
DOI:10.1145/123041
Editor:
Mark Moriconi
Issue’s Table of Contents

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 1991

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

SIGSOFT 91

Sponsor:

SIGSOFT

SIGSOFT 91: Software for Critical Systems

December 4 - 6, 1991

Louisiana, New Orleans, USA

Acceptance Rates

Overall Acceptance Rate 17 of 128 submissions, 13%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

22
Total Citations
View Citations
724
Total Downloads

Downloads (Last 12 months)95
Downloads (Last 6 weeks)16

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Lin YRadoi CDig DCheung SOrso AStorey M(2014)Retrofitting concurrency for Android applications through refactoringProceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering10.1145/2635868.2635903(341-352)Online publication date: 11-Nov-2014
https://dl.acm.org/doi/10.1145/2635868.2635903
(2014)BibliographyService Orchestration As Organization10.1016/B978-0-12-800938-3.00026-6(257-272)Online publication date: 2014
https://doi.org/10.1016/B978-0-12-800938-3.00026-6
Breaux T(2010)A method to acquire compliance monitors from regulations2010 Third International Workshop on Requirements Engineering and Law10.1109/RELAW.2010.5625358(17-26)Online publication date: Sep-2010
https://doi.org/10.1109/RELAW.2010.5625358
Khwaja AUrban J(2010)A property based specification formalism classificationJournal of Systems and Software10.1016/j.jss.2010.07.03183:11(2344-2362)Online publication date: 1-Nov-2010
https://dl.acm.org/doi/10.1016/j.jss.2010.07.031
Owre SRushby JShankar N(2005)Integration in PVS: Tables, types, and model checkingTools and Algorithms for the Construction and Analysis of Systems10.1007/BFb0035400(366-383)Online publication date: 26-Jun-2005
https://doi.org/10.1007/BFb0035400
Yunja Choi Heimdahl M(2002)Model checking RSML/sup -e/ requirements7th IEEE International Symposium on High Assurance Systems Engineering, 2002. Proceedings.10.1109/HASE.2002.1173111(109-118)Online publication date: 2002
https://doi.org/10.1109/HASE.2002.1173111
Choi YRayadurgam SHeimdahl M(2001)Automatic abstraction for model checking software systems with interrelated numeric constraintsACM SIGSOFT Software Engineering Notes10.1145/503271.50323226:5(164-174)Online publication date: 1-Sep-2001
https://dl.acm.org/doi/10.1145/503271.503232
Choi YRayadurgam SHeimdahl MTjoa AGruhn V(2001)Automatic abstraction for model checking software systems with interrelated numeric constraintsProceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering10.1145/503209.503232(164-174)Online publication date: 10-Sep-2001
https://dl.acm.org/doi/10.1145/503209.503232
Cheng BFrance R(1999)A discussion about integrated techniquesProceedings. 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques10.1109/WIFT.1998.766299(65-72)Online publication date: 1999
https://doi.org/10.1109/WIFT.1998.766299
Cheng B(1999)Multiple dimensions of integrating development technologyProceedings Computer Security, Dependability, and Assurance: From Needs to Solutions (Cat. No.98EX358)10.1109/CSDA.1998.798356(39-48)Online publication date: 1999
https://doi.org/10.1109/CSDA.1998.798356
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

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

Cited By

Index Terms

Recommendations

State-Based Model Checking of Event-Driven System Requirements

Analyzing tabular requirements specifications using infinite state model checking

A Specification-Based Approach to Model Checking Event-Driven Systems