Verified systems by composition from verified components

ABSTRACT

This paper presents an approach to integration of model checking into component-based development of software systems. This approach assists in development of highly reliable component-based software systems and reduces the complexity of verifying these systems by utilizing their compositional structures. Temporal properties of a software component are specified, verified, and packaged with the component. Selection of a component for reuse considers not only its functionality but also its temporal properties. When a component is composed from other components, a property of the component is verified on an abstraction of the component. The abstraction is constructed from environment assumptions of the component and verified properties of its sub-components. A general component model that enables component verification is defined. Component verification is discussed in the context of the instantiation of the general component model on an Asynchronous Interleaving Message-passing computation model. This approach has been applied to improve reliability of instances of TinyOS, a component-based run-time system for networked sensors. A case study on TinyOS is included, which illustrates the applicability of this approach, the detection of a bug, and the reduction in model checking complexity.

References

1. M. Abadi and L. Lamport. Conjoining specifications. In Proc. of ACM TOPLAS, 1995.
2. R. Alur and T. Henzinger. Reactive modules. In Proc. of IEEE LICS, 1996.
3. N. Amla, E. A. Emerson, K. S. Namjoshi, and R. Trefler. Assume-guarantee based compositional reasoning for synchronous timing diagrams. In Proc. of TACAS, volume 2031 of LNCS, 2001.
4. Shing Chi Cheung, Dimitra Giannakopoulou, and Jeff Kramer. Verification of liveness properties using compositional reachability analysis. In Proc. of ESEC/SIGSOFT FSE, 1997.
5. Shing Chi Cheung and Jeff Kramer. Enhancing compositional reachability analysis with context constraints. In Proc. of SIGSOFT FSE, 1993.
6. Shing Chi Cheung and Jeff Kramer. Compositional reachability analysis of finite-state distributed systems with user-specified constraints. In Proc. of SIGSOFT FSE, 1995.
7. Shing Chi Cheung and Jeff Kramer. Context constraints for compositional reachability analysis. ACM TOSEM 5(4), 1996.
8. Shing Chi Cheung and Jeff Kramer. Checking safety properties using compositional reachability analysis. ACM TOSEM 8(1), 1999.
9. E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. of Logic of Programs Workshop, 1981.
10. Edmund M. Clarke, Orna Grumberg, and Doron Peled. Model Checking. The MIT Press, 1999.
11. W. P. de Rover, F. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. Concurrency Verification: Introduction to Compositional and Non-compositional Proof Methods. Cambridge Univ. Press, 2001.
12. Kathi Fisler and Shriram Krishnamurthi. Modular verification of collaboration-based software designs. In Proc. of SIGSOFT FSE, 2001.
13. D. Gannakopoulou, C. Pasareanu, and H. Barringer. Assumption generation for software component verification. In Proc. of ASE, 2002.
14. S. Graf and B. Steffen. Compositional minimization of finite state systems. In Proc. of CAV, volume 531 of LNCS, 1990.
15. R. H. Hardin, Z. Har'El, and R. P. Kurshan. COSPAN. In Proc. of CAV, volume 1102 of LNCS, 1996.
16. J. Hill, R. Szewczyk, A. Woo, S. Hollar, D. Culler, and K. Pister. System architecture directions for networked sensors. In Proc. of ASPLOS-IX, 2000.
17. ITU. ITU-T Recommendation Z.100 (03/93) - Specification and Description Language (SDL). ITU, 1993.
18. Robert P. Kurshan. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, 1994.
19. K. L. McMillan. A methodology for hardware verification using compositional model checking. Cadence TR, 1999.
20. S. J. Mellor and M. J. Balcer. Executable UML: A Foundation for Model Driven Architecture. Addison Wesley, 2002.
21. A. Pnueli. In transition from global to modular reasoning about programs. In Proc. of Logics and Models of Concurrent Systems. NATO ASI Series, 1985.
22. J. P. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. of Symposium on Programming, 1982.
23. Clemens Szyperski. Component Software - Beyond Object-Oriented Programming. Addison-Wesley, 2002.
24. F. Xie and J. C. Browne. Integrated state space reduction for model checking executable object-oriented software system designs. In Proc. of FASE, 2002.
25. F. Xie, J. C. Browne, and R. P. Kurshan. Translation-based compositional reasoning for software systems. In Proc. of FME, 2003.
26. F. Xie, V. Levin, and J. C. Browne. Model checking for an executable subset of UML. In Proc. of ASE, 2001.
27. F. Xie, V. Levin, and J. C. Browne. ObjectCheck: a model checking tool for executable object-oriented software system designs. In Proc. of FASE, 2002.
28. W. Yeh and M. Young. Compositional reachability analysis using process algebra. In Proc. of Symposium on Testing, Analysis, and Verification, 1991.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Reliability

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Formal software verification

  • Software notations and tools

    • General programming languages

      • Language features

        • Modules / packages

  • Software organization and properties

    • Extra-functional properties

      • Software reliability

    • Software functional properties

      • Formal methods

        • Model checking

• Theory of computation

  • Logic

    • Verification by model checking

  • Semantics and reasoning

    • Program reasoning

      • Program verification