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
Open Access Guideline
Open Access Guideline
Postgraduate Thesis Guideline
Postgraduate Thesis Guideline
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
Eliminating synchronization faults in air traffic control software via design for verification with concurrency controllers
Download
index.pdf
Date
2007-06-01
Author
Betin Can, Aysu
LINDVALL, Mikael
Lux, Benjamin
Topp, Stefan
Metadata
Show full item record
This work is licensed under a
Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License
.
Item Usage Stats
143
views
0
downloads
Cite This
The increasing level of automation in critical infrastructures requires development of effective ways for finding faults in safety critical software components. Synchronization in concurrent components is especially prone to errors and, due to difficulty of exploring all thread interleavings, it is difficult to find synchronization faults. In this paper we present an experimental study demonstrating the effectiveness of model checking techniques in finding synchronization faults in safety critical software when they are combined with a design for verification approach. We based our experiments on an automated air traffic control software component called the Tactical Separation Assisted Flight Environment (TSAFE). We first reengineered TSAFE using the concurrency controller design pattern. The concurrency controller design pattern enables a modular verification strategy by decoupling the behaviors of the concurrency controllers from the behaviors of the threads that use them using interfaces specified as finite state machines. The behavior of a concurrency controller is verified with respect to arbitrary numbers of threads using the infinite state model checking techniques implemented in the Action Language Verifier (ALV). The threads which use the controller classes are checked for interface violations using the finite state model checking techniques implemented in the Java Path Finder (JPF). We present techniques for thread isolation which enables us to analyze each thread in the program separately during interface verification. We conducted two sets of experiments using these verification techniques. First, we created 40 faulty versions of TSAFE using manual fault seeding. During this exercise we also developed a classification of faults that can be found using the presented design for verification approach. Next, we generated another 100 faulty versions of TSAFE using randomly seeded faults that were created automatically based on this fault classification. We used both infinite and finite state verification techniques for finding the seeded faults. The results of our experiments demonstrate the effectiveness of the presented design for verification approach in eliminating synchronization faults.
Subject Keywords
Model checking
,
Concurrent programming
,
Synchronization
,
Design patterns
,
Interfaces
URI
https://hdl.handle.net/11511/30420
Journal
AUTOMATED SOFTWARE ENGINEERING
DOI
https://doi.org/10.1007/s10515-007-0008-2
Collections
Graduate School of Informatics, Article
Suggestions
OpenMETU
Core
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...
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...
How Does Software Visualization Contribute to Software Comprehension? A Grounded Theory Approach
Duru, Haci Ali; Çakır, Murat Perit; Isler, Veysi (2013-11-02)
Despite their ability to synthesize vast amounts of information, software visualization tools are not widely adopted in the software engineering industry. In an effort to investigate the underlying reasons, we conducted a usability study to investigate the affordances of software visualization techniques for the maintenance of complex software systems. Expert programmers were asked to carry out programming tasks with or without using a software visualization tool while their screens and eye gaze patterns we...
Development of a web-based manufacturing application system for rotational parts
Özsüer, Erhan; Anlağan, Ömer; Department of Mechanical Engineering (2003)
Developing process plans and part programs rapidly and correctly for CNC machine tools plays a vital role in manufacturing. This study is concerned with the development of a web-enabled virtual design and manufacturing application system for rotational parts. The object oriented methodology is used in the application development. Windows Distributed interNet Application (DNA) architecture which describes a framework of building software technologies in an integrated web and client-server model of computing,...
Designing cloud data warehouses using multiobjective evolutionary algorithms
Dökeroǧlu, Tansel; Sert, Seyyit Alper; Çinar, M. Serkan; Coşar, Ahmet (2014-01-01)
DataBase as a Service (DBaaS) providers need to improve their existing capabilities in data management and balance the efficient usage of virtual resources to multi-users with varying needs. However, there is still no existing method that concerns both with the optimization of the total ownership price and the performance of the queries of a Cloud data warehouse by taking into account the alternative virtual resource allocation and query execution plans. Our proposed method tunes the virtual resources of a ...
Citation Formats
IEEE
ACM
APA
CHICAGO
MLA
BibTeX
A. Betin Can, M. LINDVALL, B. Lux, and S. Topp, “Eliminating synchronization faults in air traffic control software via design for verification with concurrency controllers,”
AUTOMATED SOFTWARE ENGINEERING
, pp. 129–178, 2007, Accessed: 00, 2020. [Online]. Available: https://hdl.handle.net/11511/30420.