Highly dependable concurrent programming using design for verification |
| |
Authors: | Aysu Betin-Can Tevfik Bultan |
| |
Affiliation: | (1) Informatics Institute, Middle East Technical University, 06531 Ankara, Turkey;(2) Computer Science Department, University of California, Santa Barbara, CA 93106, USA |
| |
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. |
| |
Keywords: | Model checking Interfaces Concurrent programming Synchronization Design patterns |
本文献已被 SpringerLink 等数据库收录! |
|