Advertisement

Springer Nature is making Coronavirus research free. View research | View latest news | Sign up for updates

Highly dependable concurrent programming using design for verification

  • 54 Accesses

  • 4 Citations

Abstract

There has been significant progress in automated verification techniques based on model checking. However, scalable software model checking remains a challenging problem. We believe that this problem can be addressed using a design for verification approach based on design patterns that facilitate scalable automated verification. In this paper, we present a design for verification approach for highly dependable concurrent programming using a design pattern for concurrency controllers. A concurrency controller class consists of a set of guarded commands defining a synchronization policy, and a stateful interface describing the correct usage of the synchronization policy. We present an assume-guarantee style modular verification strategy which separates the verification of the controller behavior from the verification of the conformance to its interface. This allows us to execute the interface and behavior verification tasks separately using specialized verification techniques. We present a case study demonstrating the effectiveness of the presented approach.

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

References

  1. ACM05.

    Alur R, Cerny P, Madhusudan P, Nam W (2005) Synthesis of interface specifications for Java classes. In: Proceedings of the 32nd annual ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL), pp 98–109

  2. BBC05.

    Bultan T, Betin-Can A (2005) Scalable software model checking using design for verification. In: Proceedings of the IFIP working conference on verified software: theories, tools, experiments

  3. BCB03.

    Betin-Can A, Bultan T (2003) Interface-based specification and verification of concurrency controllers. Technical Report 2003-13, Computer Science Department, University of California, Santa Barbara

  4. BCB04.

    Betin-Can A, Bultan T (2004) Verifiable concurrent programming using concurrency controllers. In: Proceedings of the 19th IEEE international conference on automated software engineering (ASE), pp 248–257

  5. BCBL05.

    Betin-Can A, Bultan T, Lindvall M, Topp S, Lux B (2005) Application of design for verification with concurrency controllers to air traffic control software. In: Proceedings of the 20th IEEE international conference on automated software engineering (ASE), pp 14–23

  6. Bog01.

    Bogda JG (2001) Program analysis alleviates Java synchronization. PhD thesis, University of California, Santa Barbara

  7. BR01.

    Ball T, Rajamani SK (2001) Automatically validating temporal safety properties of interfaces. In: Proceedings of the SPIN workshop on model checking software. Lecture notes in computer science, vol 2057, pp 103–122

  8. BR02.

    Ball T, Rajamani SK (2002) The SLAM project: Debugging system software via static analysis. In: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL), pp 1–3

  9. BYK01.

    Bultan T, Yavuz-Kahveci T (2001) Action language verifier. In: Proceedings of the 16th IEEE international conference on automated software engineering (ASE), pp 382–386

  10. Car96.

    Cargill T (1996) Specific notification for Java thread synchronization. In: Proceedings of the 3rd conference on pattern languages of programs

  11. CBH00.

    Corbett JC, Dwyer MB, Hatcliff J, Laubach S, Pasarenau CS, Robby, Zheng H (2000) Bandera: extracting finite-state models from Java source code. In: Proceedings of the 22nd international conference on software engineering (ICSE), pp 439–448

  12. CCG03.

    Chaki S, Clarke E, Groce A, Jha S, Veith H (2003) Modular verification of software components in C. In: Proceedings of the 25th international conference on software engineering (ICSE), pp 385–395

  13. CdAH02.

    Chakrabarti A, de Alfaro L, Henzinger TA, Jurdziński M, Mang FYC (2002) Interface compatibility checking for software modules. In: Proceedings of the 14th international conference on computer aided verification (CAV). Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 428–441

  14. CGP99.

    Clarke EM, Grumberg O, Peled DA (1999) Model checking. The MIT Press, Cambridge

  15. CGS99.

    Choi JD, Gupta M, Serrano M, Sreedhar VC, Midkiff S (1999) Escape analysis for Java. In: Proceedings of the 14th ACM SIGPLAN conference on object-oriented programming, systems, languages, and applications (OOPSLA), vol 34

  16. DDH02.

    Deng X, Dwyer MB, Hatcliff J, Mizuno M (2002) Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. In: Proceedings of the 24th international conference on software engineering, pp 442–452

  17. Del00.

    Delzanno G, (2000) Automatic verification of parameterized cache coherence protocols. In: Proceedings of the 12th international conference on computer aided verification (CAV). Lecture notes in computer science, vol 1855, pp 53–68

  18. DF01.

    DeLine R, Fähndrich M (2001) Enforcing high-level protocols in low-level software. In: Proceedings of the 2001 ACM SIGPLAN conference on programming language design and implementation (PLDI), pp 59–69

  19. DF04.

    DeLine R, Fähndrich M (2004) Typestates for objects. In: Proceedings of the 18th European conference on object-oriented programming (ECOOP), pp 465–490

  20. DHJ01.

    Dwyer MB, Hatcliff J, Joehanes R, Laubach S, Pasareanu CS, Robby, Visser W, Zheng H (2001) Tool-supported program abstraction for finite-state verification. In: Proceedings of the 23rd international conference on software engineering (ICSE), pp 177–187

  21. Far98.

    Farley J (1998) Java distributed computing. O’Reilly and Associates Inc., Sebastopol

  22. FLL02.

    Flanagan C, Leino KRM, Lillibridge M, Nelson G, Saxe JB, Stata R (2002) Extended static checking for Java. In: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL), pp 234–245

  23. FQ03.

    Flanagan C, Qadeer S (2003) Thread-modular model checking. In: Proceedings of the 10th international SPIN workshop on model checking of software, pp 213–224

  24. GCJ98.

    Godefroid P, Colby C, Jagadeesan L (1998) Automatically closing open reactive programs. In: Proceedings of 1998 ACM SIGPLAN conference on programming language design and implementation (PLDI), pp 345–357

  25. HJM03.

    Henzinger TA, Jhala R, Majumdar R, Sutre G (2003) Software verification with Blast. In: Proceedings of the 10th international SPIN workshop on model checking of software. Lecture notes in computer science vol 2648. Springer, Berlin Heidelberg New York, pp 235–239

  26. HLP01.

    Havelund K, Lowry M, Penix J (2001) Formal analysis of a space craft controller using spin. IEEE Trans Softw Eng 27(8):749–765

  27. Hoa78.

    Hoare CAR (1978) Communicating sequential processes. Commun ACM 21(8):666–677

  28. Ind.

    Indus. http://indus.projects.cis.ksu.edu

  29. Jav.

    Java 5.0 concurrency utilities. http://java.sun.com/j2se/1.5.0/docs/guide/concurrency/

  30. JLP05.

    Jacobs B, Leino R, Piessens F, Schulte W (2005) Safe concurrency for aggregate objects with invariants. In: Proceedings of the 3rd IEEE international conference on software engineering and formal methods (SEFM), pp 137–147

  31. Lea99.

    Lea D (1999) Concurrent programming in Java. Addison-Wesley, Reading

  32. Meh03.

    Mehlitz PC (2003) Design for verification with dynamic assertions. Technical Report, NASA Ames

  33. MK99.

    Magee J, Kramer J (1999) Concurrency: state models and Java programs. Wiley, England

  34. MP03.

    Mehlitz PC, Penix J (2003) Design for verification using design patterns to build reliable systems. In: Proceedings of 6th workshop on component-based software engineering

  35. PDH99.

    Pasareanu CS, Dwyer MB, Huth M (1999) Assume guarantee model checking of software: a comparative case study. In: Proceedings of the workshop on theoretical and practical aspects of SPIN model checking. Lecture notes in computer science, vol 1680, pp 168–183

  36. SBK01.

    Sharygina N, Browne JC, Kurshan RP (2001) A formal object-oriented analysis for software reliability: design for verification. In: Proceedings of the 4th international conference on fundamental approaches to software engineering (FASE), pp 318–332

  37. SSR00.

    Schmidt DC, Stal M, Rohnert H, Buschmann F (2000) Pattern-oriented software architecture: Patterns for concurrent and networked objects. Wiley, England

  38. TD03.

    Tkachuk O, Dwyer MB (2003) Adapting side-effects analysis for modular program model checking. In: Proceedings of the 18th IEEE international conference on automated software engineering (ASE), pp 116–129

  39. TDP03.

    Tkachuk O, Dwyer MB, Pasareanu CS (2003) Automated environment generation for software model checking. In: Proceedings of the 11th ACM SIGSOFT symposium on foundations of software engineering held jointly with 9th European software engineering conference (ESEC/FSE), pp 188–197

  40. VHB03.

    Visser W, Havelund K, Brat G, Park S (2000) Model checking programs. Autom Softw Eng J 10(2):203–232

  41. WML02.

    Whaley J, Martin M, Lam M (2002) Automatic extraction of object-oriented component interfaces. In: Proceedings of the ACM/SIGSOFT international symposium on software testing and analysis (ISSTA), pp 218–228

  42. YKB02.

    Yavuz-Kahveci T, Bultan T (2002) Specification, verification, and synthesis of concurrency control components. In: Proceedings of the 2002 ACM/SIGSOFT international symposium on software testing and analysis (ISSTA), pp 169–179

  43. YKBB05.

    Yavuz-Kahveci T, Bartzis C, Bultan T (2005) Action language verifier, extended. In: Proceedings of the 17th international conference on computer aided verification (CAV), pp 413–417

Download references

Author information

Correspondence to Aysu Betin-Can.

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Betin-Can, A., Bultan, T. Highly dependable concurrent programming using design for verification. Form Asp Comp 19, 243–268 (2007). https://doi.org/10.1007/s00165-006-0017-0

Download citation

Keywords

  • Model checking
  • Interfaces
  • Concurrent programming
  • Synchronization
  • Design patterns