Abstract
This paper reports a data abstraction algorithm that is targeted to minimize the contribution of the loop executions to the program state space. The loop abstraction is defined as the syntactic program transformation that results in the sound representation of the concrete program. The abstraction algorithm is defined and implemented in the context of the integrated software design, testing and model checking. The loop abstraction technique was applied to verification of NASA robot control software. The abstraction enabled model checking for realistic robot configurations where all other state space reduction approaches, including BDD-based verification, predicate abstraction and partial order reduction, failed.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
T. Ball, R. Majumdar, T. Millstein and S. Rajamani, Automatic Predicate Abstraction of C Programs, In Proc. of PLDI 2001, SIGPLAN Notices, Vol. 39 (2001)
B. Beizer, Software Testing Techniques, New York: Van Nostrand Reinold, (1990)
J.J. Chilenski and S.P. Miller, Applicability of modified conditional coverage to software testing, Software Engineering Journal, (1994) 193–200
E.M. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. In Proceedings POPL 92: Principles of Programming Languages, (1992) 343–354
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for the static analysis of programs by construction of approximation of fixpoints. In Proc. of POPL’77, (1977) 238–252
D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems: abstractions preserving ACTL*, ECTL*, and CTL*. In Proceedings of PROCOMET 94: Programming Concepts, Methods, and Calculi, (1994) 561–581
S. Graf and H. Saidi, Construction of abstract state graphs with PVS. In Proceedings of CAV 1997, LNCS 1254 (1997) 72–83
R. Hardin, Z. Har'EL, and R.P. Kurshan, COSPAN, In Proceedings of CAV 1996, LNCS 1102, (1996) 423–427
M.S. Hecht, Flow Analysis of Computer Programs, NY: Elsevier-N. Holland (1977)
J. Holzmann, Design and Validation of Computer Protocols, Pr. Hall, NJ (1991)
Kapoor, C., and Tesar, D.: A Reusable Operational Software Architecture for Advanced Robotics (OSCAR), The University of Texas at Austin, DOE Grant No. DE-FG01 94EW37966 (1998)
Kurshan, R., Computer-Aided Verification of Coordinating Processes-The Automata Theoretic Approach, Princeton University Press, Princeton, NJ (1994)
C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, Vol. 6(1), (1995) 11–44
K.S. Namjoshi and R P. Kurshan, Syntactic Program Transformations for Automatic Abstraction, In Proc. of CAV’00, LNCS 1855, (2000), 435–449
Y. Kesten and A. Pnueli, Control and Data Abstraction: Cornerstones of the Practical Formal Verification, Software Tools and Technology Transfer, Vol. 2(4) (2000)
SES Inc., ObjectBench Technical Reference, SES Inc. (1998)
N. Sharygina, Model Checking of Software Control Systems, Ph.D. Dissertation, The University of Texas at Austin (2002)
N. Sharygina, J.C. Browne and R. Kurshan, A Formal Object-Oriented Analysis for Software Reliability: Design for Verification, In Proc. of FASE’01, LNCS 2029, (2001), 318–332
S. Shlaer, S. Mellor, Object Lifecycles: Modeling the World in States, Pr. Hall (1992)
L. Starr, Executable UML: The Models that Are the Code, M. Integration, LLC (2001)
F. Xie, V. Levin, and J.C. Browne, Model Checking of an Executable Subset of UML, In Proceedings of ASE2001: Automated Software Engineering (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-VerlagBerlin Heidelberg
About this paper
Cite this paper
Sharygina, N., Browne, J.C. (2003). Model Checking Software via Abstraction of Loop Transitions. In: Pezzè, M. (eds) Fundamental Approaches to Software Engineering. FASE 2003. Lecture Notes in Computer Science, vol 2621. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36578-8_23
Download citation
DOI: https://doi.org/10.1007/3-540-36578-8_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00899-6
Online ISBN: 978-3-540-36578-5
eBook Packages: Springer Book Archive