Application of design for verification with concurrency controllers to air traffic control software

Date

2005-11-11

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

194
views

0
downloads

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 using interfaces specified as finite state machines. The behavior of a concurrency controller can be verified with respect to arbitrary numbers of threads using infinite state model checking techniques, and the threads which use the controller classes can be checked for interface violations using finite state model checking techniques. We present techniques for thread isolation which enables us to analyze each thread in the program separately during interface verification. We conducted an experimental study investigating the effectiveness of the presented design for verification approach on safety critical air traffic control software. In this study, we first reengineered the Tactical Separation Assisted Flight Environment (TSAFE) software using the concurrency controller design pattern. Then, using fault seeding, we created 40 faulty versions of TSAFE and used both infinite and finite state verification techniques for finding the seeded faults. The experimental study demonstrated the effectiveness of the presented modular verification approach and resulted in a classification of faults that can be found using the presented approach.

Subject Keywords

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

URI

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

DOI

https://doi.org/10.1145/1101908.1101914

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...
Evaluation of UAS Camera Operator Interfaces in a Simulated Task Environment An Optical Brain Imaging Approach Çakır, Murat Perit; Akay, Daryal; Ayaz, Hasan; İşler, Veysi (null; 2012-07-11) In this paper we focus on the effect of different interface designs on the performance and cognitive workload of sensor operators (SO) during a target detection task in a simulated environment. Functional near-infrared (fNIR) spectroscopy is used to investigate whether there is a relationship between target detection performance across three SO interfaces and brain activation data obtained from the subjects’ prefrontal cortices that are associated with relevant higher-order cognitive functions such as atten...
Investigation into adaptive structure in software-embedded products from cybernetic perspective Yurdakul, E. Ertuğrul; Şener Pedgley, Bahar; Department of Industrial Design (2007) This study investigates the concept of adaptivity in relation to the evolution of software and hence software embedded products. Whilst laying out the benefits of adaptivity in products, it discusses the potential future threats engendered by the actual change observed in the functionality principles of adaptive products. The discussion is based upon cybernetic theory which defines control technology in the 20th century anew. Accordingly, literature survey on cybernetic theory, evolution of software from co...
Eliminating synchronization faults in air traffic control software via design for verification with concurrency controllers Betin Can, Aysu; LINDVALL, Mikael; Lux, Benjamin; Topp, Stefan (2007-06-01) 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 ...
DEVELOPING A MEASUREMENT SCALE FOR EVALUATING PERCEIVED AFFECTIVE QUALITIES IN FLIGHT DECK DESIGN Güneş, Çiğdem; Töre Yargın, Gülşen; Department of Industrial Design (2021-7-13) While traditional human factors approaches have focused on efficiency, usability, and safety, emerging approaches have also focused on product experience. There is a shift from a cognitive perspective to an affective one, which concerns promoting pleasure instead of just preventing design deficiencies. There has been a growing interest in affect and pleasure in such areas as engineering design, psychology, neuroscience, human factors, and industrial design. Human Factors/Ergonomics (HF/E) approaches in avia...

Citation Formats

A. Betin Can, M. Lindvall, B. Lux, and S. Topp, “Application of design for verification with concurrency controllers to air traffic control software,” 2005, Accessed: 00, 2020. [Online]. Available: https://hdl.handle.net/11511/29902.