A Formal Object-Oriented Analysis for Software Reliability: Design for Verification

  • Natasha Sharygina
  • James C. Browne
  • Robert P. Kurshan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2029)


This paper presents the OOA design step in a methodology which integrates automata-based model checking into a commercially supported OO software development process.We define and illustrate a set of design rules for OOA models with executable semantics, which lead to automata models with tractable state spaces. The design rules yield OOA models with functionally structured designs similar to those of hardware systems. These structures support modelchecking through techniques known to be feasible for hardware. The formal OOA methodology, including the design rules, was applied to the design of NASA robot control software. Serious logical design errors that had eluded prior testing, were discovered in the course of model-checking.


Model Check Joint Angle Design Rule State Transition Diagram Redundant Robot 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Booch, G., Object-Oriented Analysis and Design with Applications, Benjamin/Cummings, Redwood City, CA (1994)Google Scholar
  2. 2.
    Bounimova, E., Levin, V., Basbugoglu, O., and Inan, K., AVerification Engine for SDL Spec. Of Comm. Protocols, In Proc. of the 1st Symp. on Computer Networks, Istanbul, Turkey, (1996) 16–25Google Scholar
  3. 3.
    Bosnacki, D., Damm, D., Holenderski, L.,and Sidorova, N., Model checking SDL with Spin, In Proc. of TACAS2000, Berlin, Germany, (2000) 363–377Google Scholar
  4. 4.
    Clarke, E.M., and Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic,Workshop on Logic of Programs,Yorktown Heights,NY. LNCS, Vol. 131, (1981) 52–71Google Scholar
  5. 5.
    Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Pasareanu, C., Bandera: Extracting finite-state models for Java source code, In Proc. of 22nd ICSE (2000)Google Scholar
  6. 6.
    Chan, W., Anderson, R., Beame, P., Burns, S., Modugno, F., Notkin, D., Reese, J., Model Checking Large Software Specifications, In Proc. of IEEE Transaction on Software Engineering (1998) 498–519Google Scholar
  7. 7.
    Gnesi, S., Lenzini, G., Abbaneo, C., Latella, D., Amendola, A., Marmo, P.,AnAutomatic SPIN Validation of a Safety Critical Railway Control System, In Proc. of Int. Conf. on Dependable Systems and Networks, (2000) 119–124Google Scholar
  8. 8.
    Gunter, E., and Peled D., Path Exploration Tool, In Proc. of TACAS 1999, Amsterdam, The Netherlands (1999) 405–419Google Scholar
  9. 9.
    Hardin R., Har’El, Z., and Kurshan, R.P., COSPAN, In Proc., CAV’96, LNCS, Vol. 1102, (1996) 423–427Google Scholar
  10. 10.
    Havelund, K., and Pressburger, T., Model Checking Java Programs Using Java PathFinder, In Proc. 4’th SPIN workshop (1998)Google Scholar
  11. 11.
    Holzmann, G., and Smith, M., Feaver: Automating software feature verification, Bell Labs Technical Journal, Vol. 5, 2, (2000) 72–87CrossRefGoogle Scholar
  12. 12.
    Holzmann, G., The Model Checker SPIN, IEEE Trans. on Software Engineering, Vol. 5(23), (1997) 279–295CrossRefGoogle Scholar
  13. 13.
    Kapoor, C., and Tesar, D.: A Reusable Operational Software Architecture for Advanced Robotics (OSCAR), The University of Texas at Austin, Report to DOE, Grant No. DE-FG01 94EW37966 and NASA Grant No. NAG 9–809 (1998)Google Scholar
  14. 14.
    Kurshan, R., Computer-Aided Verification of Coordinating Processes-The Automata-Theoretic Approach, Princeton University Press, Princeton, NJ (1994)Google Scholar
  15. 15.
    Lano, K., Formal Object-Oriented Development, Springer (1997)Google Scholar
  16. 16.
    Lind-Nielsen, J, Andersen H., R., etc., Verification of large State/Event Systems using Compositionality and Depenedency Analysis, In Proc. of TACAS’98, Portugal (1998) 201–216Google Scholar
  17. 17.
    Liskov, B., Data Abstraction and Hierarchy, In Proc. of OOPSLA conference (1987)Google Scholar
  18. 18.
    McMillan, K. Symbolic Model Checking, Kluwer (1993)Google Scholar
  19. 19.
    Moors, T., Protocol Organs: Modularity should reflect function, not timing, In Proc. OPENARCH98, (1998) 91–100Google Scholar
  20. 20.
    Object Management Group (OMG), Action Semantic for the UML, OMG (2000)Google Scholar
  21. 21.
    Rumbaugh, J., Jacobson, I. and Booch, G., The Unified Modeling Language Reference Manual, Object Technology Series, Addison-Wesley (1999)Google Scholar
  22. 22.
    Sharygina, N., and Browne, J., Automated Rob. Decision Support Software Reverse Engineering, Tech. Rep., The Univ. of Texas at Austin, Robotics Research Croup (1999)Google Scholar
  23. 23.
    Sharygina, N., and Peled, D., A Combined Testing and Verification Approach for Software Reliability, In Proc. of FME2001 (to appear), Berlin (2001)Google Scholar
  24. 24.
    SES Inc., CodeGenesis User Reference Manual, SES Inc. (1998)Google Scholar
  25. 25.
    SES inc., ObjectBench Technical Reference, SES Inc. (1998)Google Scholar
  26. 26.
    Shlaer, S., and Mellor, S., Object Lifecycles: Modeling theWorld in States, Prentice-Hall, NJ (1992)Google Scholar
  27. 27.
    Xie, F., Levin, V., Browne, J., Integrating model checking into object-oriented software development process, Techn.Rep., University of Texas at Austin, Comp. Science Dept. (2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Natasha Sharygina
    • 1
  • James C. Browne
    • 2
  • Robert P. Kurshan
    • 1
  1. 1.Bell LaboratoriesMurray HillUSA
  2. 2.Computer Science DepartmentThe University of Texas at AustinAustinUSA

Personalised recommendations