research-article

Open access

Highly dependable concurrent programming using design for verification

Authors:

Aysu Betin-Can,

Tevfik BultanAuthors Info & Claims

Formal Aspects of Computing, Volume 19, Issue 2

Pages 243 - 268

https://doi.org/10.1007/s00165-006-0017-0

Published: 01 June 2007 Publication History

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.

References

References

[1]

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]

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]

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

[4]

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]

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]

Bogda JG Program analysis alleviates Java synchronization 2001 Santa Barbara University of California PhD thesis

Digital Library

[7]

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]

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]

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]

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

[11]

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]

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]

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]

Clarke EM, Grumberg O, and Peled DA Model checking 1999 Cambridge The MIT Press

Digital Library

[15]

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]

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]

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]

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]

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]

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]

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

Digital Library

[22]

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]

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]

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]

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]

Havelund K, Lowry M, and Penix J Formal analysis of a space craft controller using spin IEEE Trans Softw Eng 2001 27 8 749-765

Digital Library

[27]

Hoare CAR Communicating sequential processes Commun ACM 1978 21 8 666-677

Digital Library

[28]

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

[29]

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

[30]

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]

Lea D Concurrent programming in Java 1999 Reading Addison-Wesley

Digital Library

[32]

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

[33]

Magee J and Kramer J Concurrency: state models and Java programs 1999 England Wiley

Digital Library

[34]

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]

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]

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]

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

Digital Library

[38]

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]

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]

Visser W, Havelund K, Brat G, and Park S Model checking programs Autom Softw Eng J 2000 10 2 203-232

Digital Library

[41]

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]

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]

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

Cited By

Rahim L(2014)Analysis of design patterns in OpenNebula2014 International Conference on Computer and Information Sciences (ICCOINS)10.1109/ICCOINS.2014.6868443(1-6)Online publication date: Jun-2014
https://doi.org/10.1109/ICCOINS.2014.6868443
Rahim LWhittle J(2011)Identifying state space reduction techniques from behavioural design patternsProceedings of the Third Workshop on Behavioural Modelling10.1145/1993956.1993963(49-55)Online publication date: 6-Jun-2011
https://dl.acm.org/doi/10.1145/1993956.1993963
(2010)Modular verification of synchronization with reentrant locksProceedings of the Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign10.1109/MEMCOD.2010.5558623(59-68)Online publication date: 1-Jul-2010
https://dl.acm.org/doi/10.1109/MEMCOD.2010.5558623
Show More Cited By

Index Terms

Highly dependable concurrent programming using design for verification
1. Software and its engineering
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning

Index terms have been assigned to the content through auto-classification.

Recommendations

Eliminating synchronization faults in air traffic control software via design for verification with concurrency controllers

The increasing level of automation in critical infrastructures requires development of effective ways for finding faults in safety critical software components. Synchronization in concurrent components is especially prone to errors and, due to ...
Application of design for verification with concurrency controllers to air traffic control software
ASE '05: Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering

We present an experimental study which demonstrates that model checking techniques can be effective in finding synchronization errors in safety critical software when they are combined with a design for verification approach. We apply the concurrency ...
Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 19, Issue 2

Jun 2007

134 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© British Computer Society 2006.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 June 2007

Accepted: 01 September 2006

Revision received: 16 July 2006

Received: 20 March 2006

Published in FAC Volume 19, Issue 2

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
74
Total Downloads

Downloads (Last 12 months)57
Downloads (Last 6 weeks)14

Reflects downloads up to 17 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Rahim L(2014)Analysis of design patterns in OpenNebula2014 International Conference on Computer and Information Sciences (ICCOINS)10.1109/ICCOINS.2014.6868443(1-6)Online publication date: Jun-2014
https://doi.org/10.1109/ICCOINS.2014.6868443
Rahim LWhittle J(2011)Identifying state space reduction techniques from behavioural design patternsProceedings of the Third Workshop on Behavioural Modelling10.1145/1993956.1993963(49-55)Online publication date: 6-Jun-2011
https://dl.acm.org/doi/10.1145/1993956.1993963
(2010)Modular verification of synchronization with reentrant locksProceedings of the Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign10.1109/MEMCOD.2010.5558623(59-68)Online publication date: 1-Jul-2010
https://dl.acm.org/doi/10.1109/MEMCOD.2010.5558623
Tolubaeva MCan A(2008)Automatic Detection of Shared Objects in Multithreaded Java ProgramsProceedings of the 2008 International Conference on Computational Intelligence for Modelling Control & Automation10.1109/CIMCA.2008.225(522-526)Online publication date: 10-Dec-2008
https://dl.acm.org/doi/10.1109/CIMCA.2008.225
Betin Can ABultan TLindvall MLux BTopp S(2007)Eliminating synchronization faults in air traffic control software via design for verification with concurrency controllersAutomated Software Engineering10.1007/s10515-007-0008-214:2(129-178)Online publication date: 1-Jun-2007
https://dl.acm.org/doi/10.1007/s10515-007-0008-2

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents