Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Formal Approaches to Software Testing

FATES 2004: Formal Approaches to Software Testing pp 155–169Cite as

An Automata-Theoretic Approach for Model-Checking Systems with Unspecified Components

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 3395))

Abstract

This paper introduces a new approach for the verification of systems with unspecified components. In our approach, some model-checking problems concerning a component-based system are first reduced to the emptiness problem of an oracle finite automaton, which is then solved by testing the unspecified components on-the-fly with test-cases generated automatically from the oracle finite automaton. The generated test-cases are of bounded length, and with a properly chosen bound, a complete and sound solution is immediate. Particularly, the whole verification process can be carried out in an automatic way. In the paper, a symbolic algorithm is given for generating test-cases and performing the testings, and an example is drawn from an TinyOS application to illustrate our approach.

The research was supported in part by NSF Grant CCF-0430531.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: Modularity in model checking. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  2. Ammann, P., Black, P.E., Ding, W.: Model checkers in software testing. NIST-IR 6777, National Institute of Standards and Technology (2002)

    Google Scholar 

  3. Ammann, P., Black, P.E., Majurski, W.: Using model checking to generate tests from specifications. In: ICFEM 1998, p. 46 (1998)

    Google Scholar 

  4. UC Berkeley: Tinyos 1.1.0 (September 2003), http://webs.cs.berkeley.edu/tos/download.html

  5. Black, P.E., Okun, V., Yesha, Y.: Mutation operators for specifications. In: ASE 2000, p. 81 (2000)

    Google Scholar 

  6. Brown, A.W., Wallnau, K.C.: The current state of CBSE. IEEE Software 15(5), 37–46 (1998)

    Article  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  8. Callahan, J., Schneider, F., Easterbrook, S.: Automated software testing using model checking. In: Proceedings 1996 SPIN Workshop (1996)

    Google Scholar 

  9. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  10. Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, pp. 997–1072. Elsevier, Amsterdam (1990)

    Google Scholar 

  11. Engels, A., Feijs, L.M.G., Mauw, S.: Test generation for intelligent networks using model checking. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 384–398. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  12. Fisler, K., Krishnamurthi, S.: Modular verification of collaboration-based software designs. In: ESEC/FSE 2001, pp. 152–163. ACM Press, New York (2001)

    Google Scholar 

  13. Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC 1999 and ESEC-FSE 1999. LNCS, vol. 1687, pp. 146–163. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  14. Giannakopoulou, D., Pasareanu, C., Barringer, H.: Assumption generation for software component verification. In: ASE 2002, p. 3. IEEE Computer Society Press, Los Alamitos (2002)

    Google Scholar 

  15. Gorton, I., Liu, A.: Software component quality assessment in practice: successes and practical impediments. In: ICSE 2002, pp. 555–558. ACM Press, New York (2002)

    Google Scholar 

  16. Groce, A., Peled, D., Yannakakis, M.: Amc: An adaptive model checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 521–525. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  17. Henzinger, T.A., Qadeer, S., Rajamani, S.K.: You assume, we guarantee: Methodology and case studies. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 440–451. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  18. Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D.E., Pister, K.S.J.: System architecture directions for networked sensors. In: Architectural Support for Programming Languages and Operating Systems, pp. 93–104 (2000)

    Google Scholar 

  19. Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997); Special Issue: Formal Methods in Software Practice

    Article  Google Scholar 

  20. Kozaczynski, W., Booch, G.: Component-based software engineering. IEEE Software 15(5), 34–36 (1998)

    Article  Google Scholar 

  21. Lamport, L.: Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems (TOPLAS) 5(2), 190–222 (1983)

    Article  MATH  Google Scholar 

  22. Li, H., Krishnamurthi, S., Fisler, K.: Verifying cross-cutting features as open systems. ACM SIGSOFT Software Engineering Notes 27(6), 89–98 (2002)

    Article  Google Scholar 

  23. Lynch, N., Tuttle, M.: Hierarchical correctness proofs for distributed algorithms. In: Proc. 6th ACM Symp. on Principles of Distributed Computing, pp. 137–151 (1987)

    Google Scholar 

  24. Orso, A., Harrold, M.J., Rosenblum, D.: Component metadata for software engineering tasks. In: Emmerich, W., Tai, S. (eds.) EDO 2000. LNCS, vol. 1999, pp. 129–144. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  25. Peled, D.: Algorithmic testing methods. In: CAV 2003. LNCS, vol. 2725. Springer, Heidelberg (2003)

    Google Scholar 

  26. Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. In: Wu, J., Chanson, S.T., Gao, Q. (eds.) FORTE/PSTV 1999, pp. 225–240. Kluwer, Dordrecht (1999)

    Google Scholar 

  27. Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems, sub-series F: Computer and System Science (1985)

    Google Scholar 

  28. Somenzi, F.: Cudd: Cu decision diagram package release (1998)

    Google Scholar 

  29. Stafford, J., Wolf, A.: Annotating components to support component-based static analyses of software systems. In: Grace Hopper Celebration of Women in Computing, Hyannis, Massachusetts (September 2000)

    Google Scholar 

  30. Szyperski, C.: Component technology: what, where, and how? In: ICSE 2003, pp. 684–693. IEEE Computer Society Press, Los Alamitos (2003)

    Google Scholar 

  31. Trakhtenbrot, B.A., Barzdin, Y.M.: Finite automata; behavior and synthesis. North-Holland Pub. Co., Amsterdam (1973)

    MATH  Google Scholar 

  32. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS 1986, pp. 332–344. IEEE Computer Society Press, Los Alamitos (1986)

    Google Scholar 

  33. Voas, J.: Developing a usage-based software certification process. IEEE Computer 33(8), 32–37 (2000)

    Article  Google Scholar 

  34. Whaley, J., Martin, M.C., Lam, M.S.: Automatic extraction of object-oriented component interfaces. In: ISSTA 2002 (July 2002)

    Google Scholar 

  35. Xie, G., Li, C., Dang, Z.: Testability of oracle automata. In: Domaratzki, M., Okhotin, A., Salomaa, K., Yu, S. (eds.) CIAA 2004. LNCS, vol. 3317, pp. 331–332. Springer, Heidelberg (2004) (to appear)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Electrical Engineering and Computer Science, Washington State University, Pullman, WA, 99164, USA

    Gaoyan Xie & Zhe Dang

Authors
  1. Gaoyan Xie
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zhe Dang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Goettingen, Germany

    Jens Grabowski

  2. Department of Computer Science, Aalborg University, Fredrik Bajersvej 7E, DK-9220, Aalborg, Denmark

    Brian Nielsen

Rights and permissions

Reprints and permissions

Copyright information

© 2005 IFIP International Federation for Information Processing

About this paper

Cite this paper

Xie, G., Dang, Z. (2005). An Automata-Theoretic Approach for Model-Checking Systems with Unspecified Components. In: Grabowski, J., Nielsen, B. (eds) Formal Approaches to Software Testing. FATES 2004. Lecture Notes in Computer Science, vol 3395. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31848-4_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-31848-4_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-25109-5

  • Online ISBN: 978-3-540-31848-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation