Highly dependable concurrent programming using design for verification

Download

index.pdf

Date

2007-06-01

Author

Betin Can, Aysu

Metadata

Show full item record

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Item Usage Stats

66
views

0
downloads

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.

Subject Keywords

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

URI

https://hdl.handle.net/11511/30590

Journal

FORMAL ASPECTS OF COMPUTING

DOI

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

Collections

Graduate School of Informatics, Article

Suggestions

OpenMETU
Core

Scalable Software Model Checking Using Design for Verification TEVFİK, Bultan; Betin Can, Aysu (2005-11-13) 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. We have been investigating a design for verification approach based on the following principles: 1) use of stateful, behavioral interfaces which isolate the behavior and enable mod...
Application of design for verification with concurrency controllers to air traffic control software Betin Can, Aysu; Lindvall, Mikael; Lux, Benjamin; Topp, Stefan (2005-11-11) 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 controller design pattern to the implementation of the synchronization operations in Java programs. This pattern enables a modular verification strategy by decoupling the behaviors of the concurrency controllers from the behaviors of the threads that use them u...
Model checking of apoptosis signaling pathways in lung cancers Parlak, Mehtap Ayfer; Betin Can, Aysu; Department of Information Systems (2011) Model checking is a formal verification technique which is widely used in different areas for automated verification and analysis. In this study, we applied a Model Checking method to a biological system. Firstly we constructed a single-cell, Boolean network model for the signaling pathways of apoptosis (programmed cell death) in lung cancers by combining the intrinsic and extrinsic Apoptosis pathways, p53 signaling pathway and p53 - DAP Kinase pathway in Lung cancers. We translated this model to the NuSMV ...
Verifying Maze-Like Game Levels With Model Checker SPIN Tekik, Onur; Sürer, Elif; Betin Can, Aysu (2022-06-01) This study presents a framework that procedurally generates maze-like levels and leverages an automated verification technique called model checking to verify and produce a winning action sequence for that level. By leveraging the counterexample generation feature of the SPIN model checker, one or more solutions to the level-in-test are found, and the solutions are animated using a video game description language, PyVGDL. The framework contains four behavioral templates developed to model the logic of maze-...
Global Constraints on Feature Models KARATAS, Ahmet Serkan; OGUZTUZUN, Halit; Doğru, Ali Hikmet (2010-09-10) Feature modeling has been found very effective for modeling and managing variability in Software Product Lines. The nature of feature models invites, sometimes even requires, the use of global constraints. This paper lays the groundwork for the inclusion of global constraints in automated reasoning on feature models. We present a mapping from extended feature models to constraint logic programming over finite domains, and show that this mapping enables using global constraints on feature attributes, as well...

Citation Formats

A. Betin Can, “Highly dependable concurrent programming using design for verification,” FORMAL ASPECTS OF COMPUTING, pp. 243–268, 2007, Accessed: 00, 2020. [Online]. Available: https://hdl.handle.net/11511/30590.