Scalable Software Model Checking Using Design for Verification

Date

2005-11-13

Author

TEVFİK, Bultan
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

92
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. 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 modular verification, 2) an assume-guarantee style verification strategy which separates verification of the behavior from the verification of the conformance to the interface specifications, 3) a general model checking technique for interface verification, and 4) domain specific and specialized verification techniques for behavior verification. So far we have applied this approach to verification of synchronization operations in concurrent programs and to verification of interactions among multiple peers in composite web services. The case studies we conducted indicate that scalable software verification is achievable in these application domains using our design for verification approach

Subject Keywords

Computer science, software engineering, Computer science, theory and methods

URI

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

Collections

Graduate School of Informatics, Conference / Seminar

Suggestions

OpenMETU
Core

Highly dependable concurrent programming using design for verification Betin Can, Aysu (2007-06-01) 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 controll...
Continuous process improvement in software organizations utilizing maturity models Uskarcı, Algan; Demirörs, Onur; Department of Information Systems (2017) During the last two decades, staged process maturity models have been successfully used by software organizations for process improvement. However, the subject of how effective these models are in terms of organization-wide continuous process improvement has not been extensively studied. This study aims to fill this gap by performing a multiple case study to answer questions such as “Are software process improvement activities continuous?”, “Is there an organization wide commitment to process improvement ac...
Analysis of extended feature models with constraint programming Karataş, Ahmet Serkan; Oğuztüzün, Mehmet Halit S.; Department of Computer Engineering (2010) In this dissertation we lay the groundwork of automated analysis of extended feature models with constraint programming. Among different proposals, feature modeling has proven to be very effective for modeling and managing variability in Software Product Lines. However, industrial experiences showed that feature models often grow too large with hundreds of features and complex cross-tree relationships, which necessitates automated analysis support. To address this issue we present a mapping from extended fe...
SIMULATION CONCEPTS FOR INFORMATION-SYSTEM MOURANT, RR; Tarı, Zehra Sibel (Elsevier BV, 1993-09-01) Recent Improvements in document image systems and their low-cost implementation on networks of microcomputers is leading to the reengineering of many information systems. We describe how document image systems can be applied to information systems. In order to compare the performance of a conventional information system with one implemented with document imaging processing capability we conducted a discrete event simulation. We modeled the conventional information system for processing graduate student ...
Domain adaptation on graphs by learning graph topologies: theoretical analysis and an algorithm Vural, Elif (The Scientific and Technological Research Council of Turkey, 2019-01-01) Traditional machine learning algorithms assume that the training and test data have the same distribution, while this assumption does not necessarily hold in real applications. Domain adaptation methods take into account the deviations in data distribution. In this work, we study the problem of domain adaptation on graphs. We consider a source graph and a target graph constructed with samples drawn from data manifolds. We study the problem of estimating the unknown class labels on the target graph using the...

Citation Formats

B. TEVFİK and A. Betin Can, “Scalable Software Model Checking Using Design for Verification,” 2005, Accessed: 00, 2020. [Online]. Available: https://hdl.handle.net/11511/56061.