Show/Hide Menu
Hide/Show Apps
Logout
Türkçe
Türkçe
Search
Search
Login
Login
OpenMETU
OpenMETU
About
About
Open Science Policy
Open Science Policy
Communities & Collections
Communities & Collections
Help
Help
Frequently Asked Questions
Frequently Asked Questions
Guides
Guides
Thesis submission
Thesis submission
MS without thesis term project submission
MS without thesis term project submission
Publication submission with DOI
Publication submission with DOI
Publication submission
Publication submission
Supporting Information
Supporting Information
General Information
General Information
Copyright, Embargo and License
Copyright, Embargo and License
Contact us
Contact us
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
Cite This
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
IEEE
ACM
APA
CHICAGO
MLA
BibTeX
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.