Highly dependable concurrent programming using design for verification


Creative Commons License

Betin-Can A., BULTAN T.

FORMAL ASPECTS OF COMPUTING, cilt.19, sa.2, ss.243-268, 2007 (SCI-Expanded) identifier identifier

  • Yayın Türü: Makale / Tam Makale
  • Cilt numarası: 19 Sayı: 2
  • Basım Tarihi: 2007
  • Doi Numarası: 10.1007/s00165-006-0017-0
  • Dergi Adı: FORMAL ASPECTS OF COMPUTING
  • Derginin Tarandığı İndeksler: Science Citation Index Expanded (SCI-EXPANDED), Scopus
  • Sayfa Sayıları: ss.243-268
  • Orta Doğu Teknik Üniversitesi Adresli: Evet

Özet

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.