[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content

Advertisement

Springer Nature Link
Log in

Model Checking Complete Requirements Specifications Using Abstraction

  • Published:
Automated Software Engineering Aims and scope Submit manuscript

Abstract

Although model checking has proven remarkably effective in detecting errors in hardware designs, its success in the analysis of software specifications has been limited. Model checking algorithms for hardware verification commonly use Binary Decision Diagrams (BDDs) to represent predicates involving the many Boolean variables commonly found in hardware descriptions. Unfortunately, BDD representations may be less effective for analyzing software specifications, which usually contain not only Booleans but variables spanning a wide range of data types. Further, software specifications typically have huge, sometimes infinite, state spaces that cannot be model checked directly using conventional symbolic methods. One promising but largely unexplored approach to model checking software specifications is to apply mathematically sound abstraction methods. Such methods extract a reduced model from the specification, thus making model checking feasible. Currently, users of model checkers routinely analyze reduced models but often generate the models in ad hoc ways. As a result, the reduced models may be incorrect.

This paper, an expanded version of (Bharadwaj and Heitmeyer, 1997), describes how one can model check a complete requirements specification expressed in the SCR (Software Cost Reduction) tabular notation. Unlike previous approaches which applied model checking to mode transition tables with Boolean variables, we use model checking to analyze properties of a complete SCR specification with variables ranging over many data types. The paper also describes two sound and, under certain conditions, complete methods for producing abstractions from requirements specifications. These abstractions are derived from the specification and the property to be analyzed. Finally, the paper describes how SCR requirements specifications can be translated into the languages of Spin, an explicit state model checker, and SMV, a symbolic model checker, and presents the results of model checking two sample SCR specifications using our abstraction methods and the two model checkers.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

We’re sorry, something doesn't seem to be working properly.

Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  • Alspaugh, T. A., Faulk, S. R., Britton, K. H., Parker, R. A., Parnas, D. L. and Shore, J. E. 1992. Software requirements for the A-7E aircraft. Technical Report NRL-9194, Naval Research Lab., Wash., DC.

    Google Scholar 

  • Atlee, J. M. and Buckley, M. A. 1996. A logic-model semantics for SCR specifications. In Proc. Int'l Symposium on Software Testing and Analysis.

  • Atlee, J. M. and Gannon, J. 1993. State-based model checking of event-driven system requirements. IEEE Trans. Softw. Eng., 19(1):24-40.

    Google Scholar 

  • Berry, G. and Gonthier, G. 1992. The Esterel synchronous programming language: design, semantics, implementation. Science of Computer Programming, 19.

  • Bharadwaj, R. and Heitmeyer, C. 1997. Verifying SCR requirements specifications using state exploration. In Rance Cleaveland and Daniel Jackson, editors, Proc. First ACM SIGPLAN Workshop on the Automated Analysis of Software, ACM, Paris, France, pages 9-23.

    Google Scholar 

  • Bryant, R. E. 1986. Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Computers, 8(C-35):677-691.

    Google Scholar 

  • Bryant, R. E. 1992. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293-318.

    Google Scholar 

  • Chan, W., Anderson, R. J., Beame, P., Burns, S., Modugno, F., Notkin, D. and Reese, J. D. 1998. Model checking large software specifications. IEEE Trans. on Softw. Eng., 24(7).

  • Chandy, K. M. and Misra, J. 1988. Parallel Program Design — A Foundation. Reading, MA: Addison-Wesley.

    Google Scholar 

  • Clarke, E., Grumberg, O., and Long, D. 1994. Model checking and abstraction. In Proc., Principles of Programming Languages (POPL), 1994.

  • Clarke, E.M., Emerson, E. and Sistla, A. 1986. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Trans. on Prog. Lang. and Systems, 8(2):244-263.

    Google Scholar 

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

  • Courtois, P.-J. and Parnas, D.L. 1993. Documentation for safety critical software. In Proc. 15th Int'l Conf. on Softw. Eng. (ICSE '93), pages 315-323, Baltimore, MD.

  • Dams, D. and Gerth, R. 1997. Abstract interpretation of reactive systems. ACM Trans. on Prog. Lang. and Systems, pages 111-149.

  • Dijkstra, E.W. 1976. A Discipline of Programming. Prentice-Hall.

  • Dill, D.L. Drexler, A.J., Hu, A.J. and Yang, C.H. 1992. Protocol verification as a hardware design aid. In Proc. IEEE Int'l Conference on Computer Design: VLSI in Computers and Processors, pages 522-525.

  • Easterbrook, S. and Callahan, J. 1997. Formal methods for verification and validation of partial specifications: A case study. Journal of Systems and Software.

  • Faulk, S.R., Brackett, J., Ward, P. and Kirby, Jr., J. 1992. The CoRE method for real-time requirements. IEEE Software, 9(5):22-33.

    Google Scholar 

  • Faulk, S.R., Finneran, L., Kirby, Jr., J., Shah, S. and Sutton, J. 1994. Experience applying the CoRE method to the Lockheed C-130J. In Proc. 9th Annual Conf. on Computer Assurance (COMPASS '94), Gaithersburg, MD, pages 3-8.

  • Godefroid, P. 1990. Using partial orders to improve automatic verification methods. In Proceedings of the 2nd International Workshop on Computer-Aided Verification, pages 176-185.

  • Graf, S. 1994. Characterization of a sequentially consistent memory and verification of a cache memory by abstraction. In Proc. Computer Aided Verification.

  • Graf, S. and Loiseaux, C. 1993. A tool for symbolic program verification and abstraction. In Proc. Computer Aided Verification, pages 71-84.

  • Heimdahl, M.P.E. and Leveson, N. 1996. Completeness and consistency in hierarchical state-based requirements. IEEE Transactions on Software Engineering, 22(6):363-377.

    Google Scholar 

  • Heitmeyer, C., Kirby, J., Labaw, B., Archer, M. and Bharadwaj, R. 1998. Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Trans. on Softw. Eng., 24(11).

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

    Google Scholar 

  • Heitmeyer, C., Bull, A., Gasarch, C. and Labaw, B. 1995. SCR*: A toolset for specifying and analyzing requirements. In Proc. 10th Annual Conf. on Computer Assurance (COMPASS '95), pages 109-122, Gaithersburg, MD.

  • Heitmeyer, C., Kirby, J. and Labaw, B. 1997. Tools for formal specification, verification, and validation of requirements. In Proc. 12th Annual Conf. on Computer Assurance (COMPASS '97), Gaithersburg, MD.

  • Heitmeyer, C., Kirby, J. and Labaw, B. 1998. Applying the SCR requirements method to a weapons control panel: An experience report. In Proc. 2nd Workshop on Formal Methods in Software Practice (FMSP'98).

  • Heitmeyer, C., Kirby, J., Labaw, B. and Bharadwaj, R. 1998. SCR*: A toolset for specifying and analyzing software requirements. In Proc. Computer-Aided Verification, 10th Annual Conf. (CAV'98), Vancouver, Canada.

  • Heitmeyer, C.L., Jeffords, R.D. and Labaw, B.G. 1999. Tools for analyzing SCR-style requirements specifications: A formal foundation. Technical report, Naval Research Lab., Wash., DC. In preparation.

    Google Scholar 

  • Heninger, K., Parnas, D.L., Shore, J.E. and Kallander, J.W. 1978. Software requirements for the A-7E aircraft. Technical Report 3876, Naval Research Lab., Wash., DC.

    Google Scholar 

  • Hester, S.D., Parnas, D.L. and Utter, D.F. 1981. Using documentation as a software design medium. Bell System Tech. J., 60(8):1941-1977.

    Google Scholar 

  • Holzmann, G.J. 1991. Design and Validation of Computer Protocols. Prentice-Hall.

  • Holzmann, G.J. 1997. The model checker SPIN. IEEE Trans. on Softw. Eng., 23(5):279-295.

    Google Scholar 

  • Holzmann, G.J. and Peled, D. 1994. An improvement in formal verification. In Proc. FORTE94.

  • Jackson, D. 1997. Model checking and requirements. Minitutorial, Third IEEE Intern. Symposium on Requirements Engineering (RE '97).

  • Jackson, D., Jha, S., and Damon, C.A. 1994. Faster checking of software specifications using isomorphs. In Proc., Principles of Programming Languages (POPL).

  • Jeffords, R. 1997. Translating SCR properties into LTL and CTL. Technical Memorandum 5540-293A:rdj.

  • Jeffords, R. and Heitmeyer, C. 1998. Automatic generation of state invariants from requirements specifications. In Proc. Sixth ACM SIGSOFT Symp. on Foundations of Software Engineering.

  • Kaufmann, M. and Moore, J.S. 1997. An industrial-strength theorem prover based on Common Lisp. IEEE Transactions on Software Engineering, 23(4):203-213.

    Google Scholar 

  • Kirby, J. 1987. Example NRL/SCR software requirements for an automobile cruise control and monitoring system. Technical Report TR-87-07, Wang Institute of Graduate Studies.

  • Kurshan, R. 1997. Formal verification in a commercial setting. In Proc., Design Automation Conference.

  • Kurshan, R.P. 1994. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press.

  • Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A. and Bensalem, S. 1995. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:1-35.

    Google Scholar 

  • Lutz, R.R. and Shaw, H.Y. 1997. Applying the SCR* requirements toolset to DS-1 fault protection. Technical Report JPL-D15198, Jet Propulsion Laboratory, Pasadena, CA.

    Google Scholar 

  • Manna, Z. and Pnueli, A. 1991. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag.

  • McMillan, K.L. 1993. Symbolic Model Checking. Kluwer Academic Publishers.

  • Meyers, S. and White, S. 1983. Software requirements methodology and tool study for A6-E technology transfer. Technical report, Grumman Aerospace Corp., Bethpage, NY.

    Google Scholar 

  • Miller, S. 1998. Specifying the mode logic of a flight guidance system in CoRE and SCR. In Proc. 2nd Workshop on Formal Methods in Software Practice (FMSP'98).

  • Owre, S., Rushby, J., Shankar, N. and von Henke, F. 1995. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107-125.

    Google Scholar 

  • Parnas, D.L., Asmis, G.J.K. and Madey, J. 1991. Assessment of safety-critical software in nuclear power plants. Nuclear Safety, 32(2):189-198.

    Google Scholar 

  • Parnas, D.L. and Madey, J. 1995. Functional documentation for computer systems. Science of Computer Programming, 25(1):41-61.

    Google Scholar 

  • Probst, S.T. 1996. Chemical Process Safety and Operability Analysis using Symbolic Model Checking. PhD thesis, Carnegie-Mellon University, Department of Chemical Engineering, Pittsburgh, PA.

    Google Scholar 

  • Sreemani, T. and Atlee, J.M. 1996. Feasibility of model checking software requirements. In Proc. 11th Annual Conference on Computer Assurance (COMPASS '96), Gaithersburg, MD.

  • Sutton, J. 1997. Personal communication.

  • Valmari, A. 1990. A stubborn attack on state explosion. In Proceedings of the 2nd International Workshop on Computer-Aided Verification, pages 156-165.

  • Weiser, M. 1984. Program slicing. IEEE Transactions on Software Engineering, SE-10(4):352-357.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Naval Research Laboratory, Center for High Assurance Computer Systems (Code 5546), Washington, DC, 20375

    Ramesh Bharadwaj & Constance L. Heitmeyer

Authors
  1. Ramesh Bharadwaj
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Constance L. Heitmeyer
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Bharadwaj, R., Heitmeyer, C.L. Model Checking Complete Requirements Specifications Using Abstraction. Automated Software Engineering 6, 37–68 (1999). https://doi.org/10.1023/A:1008697817793

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1008697817793

Search

Navigation