research-article

State-Based Model Checking of Event-Driven System Requirements

Authors:

J. GannonAuthors Info & Claims

IEEE Transactions on Software Engineering, Volume 19, Issue 1

Pages 24 - 40

https://doi.org/10.1109/32.210305

Published: 01 January 1993 Publication History

Abstract

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 software requirements for the A-7 military aircraft). Model checking of temporal logics has been established as a sound technique for verifying properties of hardware systems. An automated technique for formalizing the semiformal SCR requirements and for transforming the resultant formal specification onto a finite structure that a model checker can analyze has been developed. This technique was effective in uncovering violations of system invariants in both an automobile cruise control system and a water-level monitoring system.

References

[1]

{1} T. Alspaugh, S. Faulk, K. Britton, R. Parker, D. Parnas, and J. Shore, "Software requirements for the A-7E Aircraft," Naval Research Lab., Tech. Rep., March 1988.

[2]

{2} J. Atlee, "Automated analysis of software requirements," Ph.D. dissertation, Dept. of Computer Science, University of Maryland, College Park, MD, 1992.

Digital Library

[3]

{3} J. Atlee and J. Gannon, "State-based model checking of event-driven system requirements," in Proc. ACM SIGSOFT'91 Conf. Software for Critical Systems, 1991, pp. 16-28.

Digital Library

[4]

{4} W. Bledsoe and L. Hines, "Variable elimination and chaining in a resolution-based prover for inequalities," in Proc. 5th Conf. Automated Deduction: Lecture Notes in Computer Science, 1980, pp. 70-87.

Digital Library

[5]

{5} M. Browne, "Automatic verification of finite state machines using temporal logic," Ph.D. dissertation, Dept. of Computer Science, Carnegie Mellon University, Pittsburgh, PA, 1989.

Digital Library

[6]

{6} M. Browne, E. Clarke, and D. Dill, "Automatic verification of sequential circuits using temporal logic," IEEE Trans. Comput., vol. C-35, no. 12, pp. 1035-1044, Dec. 1986.

Digital Library

[7]

{7} J. Burch, E. Clarke, K. McMillan, D. Dill, and J. Hwang, "Symbolic model checking: 10<sup>20</sup> states and beyond," in Proc. 5th Annu. Symp. Logic in Computer Science, June 1990, pp. 428-439.

[8]

{8} E. Clarke, E. Emerson, and A. Sistla, "Automatic verification of finite state concurrent systems using temporal logic specifications," ACM Trans. Programming Languages and Syst., vol. 8, no. 2, pp. 244-263, Apr. 1986.

Digital Library

[9]

{9} E. Clarke, D. Long, and K. McMillan, "A language for compositional specification and verification of finite state hardware controllers," Proc. IEEE, vol. 79, no. 9, pp. 1283-1292, Sept. 1991.

[10]

{10} M. Degl'Innocenti, G. Ferrari, G. Pacini, and F. Turini, "RSF: A formalism for executable requirements specifications," IEEE Trans. Software Eng., vol. 16, no. 11, pp. 1235-1246, Nov. 1990.

Digital Library

[11]

{11} E. Emerson and E. Clarke, "Using branching time temporal logic to synthesize synchronization skeletons," Sci. Comput. Programming, vol. 2, pp. 241-266, 1982.

[12]

{12} S. Faulk, "State determination in hard-embedded systems," Ph.D. dissertation, Dept. of Computer Science, University of North Carolina, Chapel Hill, 1989.

Digital Library

[13]

{13} A. Gabrielian and M. Franklin, "Multilevel specification of real-time systems," Commun. ACM, vol. 34, no. 5, pp. 51-50, May 1991.

Digital Library

[14]

{14} A. Gabrielian and R. Iyer, "Integrating automata and temporal logic: A framework for specification of real-time systems and software," in Proc. Unified Computation Laboratory, 1990.

[15]

{15} C. Ghezzi, D. Mandrioli, and A. Morzenti, "TRIO, a logic language for executable specifications of real-time systems," J. Syst. and Software, vol. 12, no. 2, pp. 107-123, May 1990.

Digital Library

[16]

{16} D. Harel, "Statecharts: A visual formalism for complex systems," Science of Comput. Programming, vol. 8, pp. 231-274, 1987.

Digital Library

[17]

{17} D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. Shtull-Trauring, and M. Trakhtenbrot, "STATEMATE: A working environment for the development of complex reactive systems," IEEE Trans. Software Eng., vol. 16, no. 4, pp. 403-414, April 1990.

Digital Library

[18]

{18} C. Heitmeyer and B. Labaw, "Consistency checks for SCR-style requirements specifications," in preparation.

[19]

{19} K. Heninger, "Specifying software requirements for complex systems: New techniques and their applications," IEEE Trans. Software Eng., vol. SE-6, no. 1, pp. 2-12, Jan. 1980.

Digital Library

[20]

{20} F. Jahanian and A. Mok, "Safety analysis of timing properties in real-time systems," IEEE Trans. Software Eng., vol. SE-12, no. 9, pp. 890-904, Sept. 1986.

Digital Library

[21]

{21} J. Kirby, "Example NRL/SCR software requirements for an automobile cruise control and monitoring system," Wang Institute of Graduate Studies, Tech. Rep. TR-87-07, July 1987.

[22]

{22} Z. Manna and A. Pnueli, "Tools and rules for the practicing verifier," Dept. of Computer Science, Stanford University, Palo Alto, CA, Tech. Rep. STAN-CS-90-1321, 1990.

Digital Library

[23]

{23} J. Ostroff, Temporal Logic for Real-Time Systems. Research Studies Press, Ltd., 1989.

Digital Library

[24]

{24} D. Parnas, D. Smith, and T. Pearce, "Making formal software documentation more practical: A progress report," Dept. of Computing and Information Science, Queen's University, Kingston, Ontario, Canada, Tech. Rep. TR-88-236, 1988.

[25]

{25} A. Pnueli, "The temporal logic of programs," in Proc. 18th Annu. Symp. the Foundation of Computer Science, 1977, pp. 46-57.

Digital Library

[26]

{26} S. Smith and S. Gerhart, "STATEMATE and cruise control: A case<sup>2</sup> study," in Proc. COMPAC'88, 12th Int. IEEE Computer Software and Application Conf., 1988, pp. 49-56.

[27]

{27} J. van Schouwen, "The A-7 requirements model: Reexamination for real-time systems and an application to monitoring systems," Dept. of Computing and Information Science, Queens's University, Kingston, Ontario, Canada, Tech. Rep. TR-90-276, May 1990.

[28]

{28} J. van Schouwen, private communication, 1991.

[29]

{29} D. Weiss, private communication, 1992.

Cited By

Wu GLiu XYing STetsuo T(2023)Automated analysis of the SCR-style requirements specificationsJournal of Computer Science and Technology10.1007/BF0294874314:4(401-407)Online publication date: 22-Mar-2023
https://dl.acm.org/doi/10.1007/BF02948743
Tamburri DBersani MMirandola RPea G(2018)DevOps Service Observability By-Design: Experimenting with Model-View-ControllerService-Oriented and Cloud Computing10.1007/978-3-319-99819-0_4(49-64)Online publication date: 12-Sep-2018
https://dl.acm.org/doi/10.1007/978-3-319-99819-0_4
Aceituna DDo HSrinivasan SJalote PBriand LHoek A(2014)A systematic approach to transforming system requirements into model checking specificationsCompanion Proceedings of the 36th International Conference on Software Engineering10.1145/2591062.2591183(165-174)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2591062.2591183
Show More Cited By

State-Based Model Checking of Event-Driven System Requirements
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning

Recommendations

A logic-model semantics for SCR software requirements
ISSTA '96: Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis

This paper presents a simple logic-model semantics for Software Cost Reduction (SCR) software requirements. Such a semantics enables model-checking of native SCR requirements and obviates the need to transform the requirements for analysis. The paper ...
Model checking and modular verification

We describe a framework for compositional verification of finite-state processes. The framework is based on two ideas: a subset of the logic CTL for which satisfaction is preserved under composition, and a preorder on structures which captures the ...
Three-valued logic in bounded model checking
MEMOCODE '05: Proceedings of the 2nd ACM/IEEE International Conference on Formal Methods and Models for Co-Design

In principle, bounded model checking (BMC) leads to semi-decision procedures that can be used to verify liveness properties and to falsify safety properties. If the procedures fail, there is usually no information about the validity of the considered ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image IEEE Transactions on Software Engineering

IEEE Transactions on Software Engineering Volume 19, Issue 1

January 1993

84 pages

ISSN:0098-5589

Issue’s Table of Contents

Copyright © Copyright © 1993 IEEE. All Rights Reserved.

Publisher

IEEE Press

Publication History

Published: 01 January 1993

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

71
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 28 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wu GLiu XYing STetsuo T(2023)Automated analysis of the SCR-style requirements specificationsJournal of Computer Science and Technology10.1007/BF0294874314:4(401-407)Online publication date: 22-Mar-2023
https://dl.acm.org/doi/10.1007/BF02948743
Tamburri DBersani MMirandola RPea G(2018)DevOps Service Observability By-Design: Experimenting with Model-View-ControllerService-Oriented and Cloud Computing10.1007/978-3-319-99819-0_4(49-64)Online publication date: 12-Sep-2018
https://dl.acm.org/doi/10.1007/978-3-319-99819-0_4
Aceituna DDo HSrinivasan SJalote PBriand LHoek A(2014)A systematic approach to transforming system requirements into model checking specificationsCompanion Proceedings of the 36th International Conference on Software Engineering10.1145/2591062.2591183(165-174)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2591062.2591183
Carvalho GFalcão DBarros FSampaio AMota AMotta LBlackburn M(2014)NAT2TEST SCRScience of Computer Programming10.1016/j.scico.2014.06.00795:P3(275-297)Online publication date: 1-Dec-2014
https://dl.acm.org/doi/10.1016/j.scico.2014.06.007
Carvalho GFalcão DBarros FSampaio AMota AMotta LBlackburn MShin SMaldonado J(2013)Test case generation from natural language requirements based on SCR specificationsProceedings of the 28th Annual ACM Symposium on Applied Computing10.1145/2480362.2480591(1217-1222)Online publication date: 18-Mar-2013
https://dl.acm.org/doi/10.1145/2480362.2480591
Yoong LRoop PSalcic Z(2013)Implementing constrained cyber-physical systems with IEC 61499ACM Transactions on Embedded Computing Systems10.1145/2362336.236234511:4(1-22)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.1145/2362336.2362345
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
Degiovanni RPonzio PAguirre NFrias M(2011)Abstraction based automated test generation from formal tabular requirements specificationsProceedings of the 5th international conference on Tests and proofs10.5555/2025936.2025944(84-101)Online publication date: 30-Jun-2011
https://dl.acm.org/doi/10.5555/2025936.2025944
Ammann POffutt JXu W(2008)Coverage criteria for state based specificationsFormal methods and testing10.5555/1806209.1806213(118-156)Online publication date: 1-Jan-2008
https://dl.acm.org/doi/10.5555/1806209.1806213
du Bousquet LDelaunay M(2008)Towards Mutation Analysis for Lustre ProgramsElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2008.05.009203:4(35-48)Online publication date: 1-Jun-2008
https://dl.acm.org/doi/10.1016/j.entcs.2008.05.009
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents