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

161
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 ...
Fully-Automatic Target Detection and Tracking for Real-Time, Airborne Imaging Applications Alkanat, Tunc; Tunali, Emre; Oz, Sinan (2015-03-14) In this study, an efficient, robust algorithm for automatic target detection and tracking is introduced. Procedure starts with a detection phase. Proposed method uses two alternatives for the detection phase, namely maximally stable extremal regions detector and Canny edge detector. After detection, regions of interest are evaluated and eliminated according to their compactness and effective saliency. The detection process is repeated for a predetermined number of pyramid levels where each level processes a...
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-...

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.