System safety property-oriented test sequences generating method based on model checking

<p>Concurrent data structure algorithms have traditionally been designed using locks to regulate the behaviour of interacting threads, thus restricting access to parts of the shared memory to only one thread at a time. Since locks can lead to issues of performance and scalability, there has been interest in designing so-called nonblocking algorithms that do not use locks. However, designing and reasoning about concurrent systems is difficult, and is even more so for nonblocking systems, as evidenced by the number of incorrect algorithms in the literature. This thesis explores how the technique of model checking can aid the testing and verification of nonblocking data structure algorithms. Model checking is an automated verification method for finite state systems, and is able to produce counterexamples when verification fails. For verification, concurrent data structures are considered to be infinite state systems, as there is no bound on the number of interacting threads, the number of elements in the data structure, nor the number of possible distinct data values. Thus, in order to analyse concurrent data structures with model checking, we must either place finite bounds upon them, or employ an abstraction technique that will construct a finite system with the same properties. First, we discuss how nonblocking data structures can be best represented for model checking, and how to specify the properties we are interested in verifying. These properties are the safety property linearisability, and the progress properties wait-freedom, lock-freedom and obstructionfreedom. Second, we investigate using model checking for exhaustive testing, by verifying bounded (and hence finite state) instances of nonblocking data structures, parameterised by the number of threads, the number of distinct data values, and the size of storage memory (e.g. array length, or maximum number of linked list nodes). It is widely held, based on anecdotal evidence, that most bugs occur in small instances. We investigate the smallest bounds needed to falsify a number of incorrect algorithms, which supports this hypothesis. We also investigate verifying a number of correct algorithms for a range of bounds. If an algorithm can be verified for bounds significantly higher than the minimum bounds needed for falsification, then we argue it provides a high degree of confidence in the general correctness of the algorithm. However, with the available hardware we were not able to verify any of the algorithms to high enough bounds to claim such confidence. Third, we investigate using model checking to verify nonblocking data structures by employing the technique of canonical abstraction to construct finite state representations of the unbounded algorithms. Canonical abstraction represents abstract states as 3-valued logical structures, and allows the initial coarse abstraction to be refined as necessary by adding derived predicates. We introduce several novel derived predicates and show how these allow linearisability to be verified for linked list based nonblocking stack and queue algorithms. This is achieved within the standard canonical abstraction framework, in contrast to recent approaches that have added extra abstraction techniques on top to achieve the same goal. The finite state systems we construct using canonical abstraction are still relatively large, being exponential in the number of distinct abstract thread objects. We present an alternative application of canonical abstraction, which more coarsely collapses all threads in a state to be represented by a single abstract thread object. In addition, we define further novel derived predicates, and show that these allow linearisability to be verified for the same stack and queue algorithms far more efficiently.</p>

Download Full-text

Integrated modular avionics system safety analysis based on model checking

2017 Annual Reliability and Maintainability Symposium (RAMS) ◽

10.1109/ram.2017.7889773 ◽

2017 ◽

Cited By ~ 3

Author(s):

Hongli Wang ◽

Tingdi Zhao ◽

Fuchun Ren ◽

Zeyong Jiang

Keyword(s):

Model Checking ◽

Safety Analysis ◽

System Safety ◽

Integrated Modular Avionics

Download Full-text

Safety Analysis of AADL Models for Grid Cyber-Physical Systems via Model Checking of Stochastic Games

Electronics ◽

10.3390/electronics8020212 ◽

2019 ◽

Vol 8 (2) ◽

pp. 212 ◽

Cited By ~ 3

Author(s):

Xiaomin Wei ◽

Yunwei Dong ◽

Pengpeng Sun ◽

Mingrui Xiao

Keyword(s):

Model Checking ◽

Stochastic Games ◽

Safety Analysis ◽

Cyber Physical Systems ◽

System Level ◽

Probabilistic Model Checking ◽

Critical Systems ◽

System Safety ◽

Physical Systems ◽

Analysis And Design

As safety-critical systems, grid cyber-physical systems (GCPSs) are required to ensure the safety of power-related systems. However, in many cases, GCPSs may be subject to uncertain and nondeterministic environmental hazards, as well as the variable quality of devices. They can cause failures and hazards in the whole system and may jeopardize system safety. Thus, it necessitates safety analysis for system safety assurance. This paper proposes an architecture-level safety analysis approach for GCPSs applying the probabilistic model-checking of stochastic games. GCPSs are modeled using Architecture Analysis and Design Language (AADL). Random errors and failures of a GCPS and nondeterministic environment behaviors are explicitly described with AADL annexes. A GCPS AADL model including the environment can be regarded as a game. To transform AADL models to stochastic multi-player games (SMGs) models, model transformation rules are proposed and the completeness and consistency of rules are proved. Property formulae are formulated for formal verification of GCPS SMG models, so that occurrence probabilities of failed states and hazards can be obtained for system-level safety analysis. Finally, a modified IEEE 9-bus system with grid elements that are power management systems is modeled and analyzed using the proposed approach.

Download Full-text

A Summary of Recent Progress on Efficient Parametric Approximations of Viability and Discriminating Kernels

10.29007/bm16 ◽

2018 ◽

Cited By ~ 2

Author(s):

Ian M. Mitchell

Keyword(s):

Model Checking ◽

Recent Progress ◽

Polynomial Complexity ◽

Computational Algorithms ◽

Sampled Data ◽

Paper Briefly ◽

System Safety ◽

Nonparametric Approach ◽

Key Features ◽

Grid Based

Viability and discriminating kernels are powerful constructs for analyzing system safety through model checking, but until recently the only computational algorithms available were nonparametric grid-based approaches which, although accurate, scaled exponentially with the dimension of the system's state space. In contrast, several polynomial complexity reachability algorithms have been developed using various parametric set representations. In a recent series of papers, two of these parametric approaches -- based on ellipsoids and support vectors -- have been adapted to approximate viability and discriminating kernels in the discrete, continuous and sampled data models of time. This paper briefly summarizes these algorithms and compares their key features with one another and with a representative nonparametric approach.

Download Full-text

A Composite Safety Assurance Method for Developing System Architecture Using Model Checking

International Journal of Systems and Software Security and Protection ◽

10.4018/ijsssp.2021010105 ◽

2021 ◽

Vol 12 (1) ◽

pp. 78-93

Author(s):

Qiang Zhi ◽

Zhengshu Zhou ◽

Shuji Morisaki

Keyword(s):

Model Checking ◽

System Safety ◽

Critical System ◽

Safety Issues ◽

Automatic Driving ◽

Safety Assurance ◽

Safety Critical System ◽

Assurance Cases ◽

Developing System ◽

Assurance Case

Assurance case helps analyze the system dependability, but the relationships between system elements and assurance case are generally not clearly defined. In order to make system assurance more intuitive and reliable, this paper proposes an approach that clearly defines the relationships between safety issues and system elements and integrates them using ArchiMate. Also, the proposed method applies model checking to system safety assurance, and the checking results are regarded as evidence of assurance cases. This method consists of four steps: interaction visualization, processes model checking, assurance case creation, and composite safety assurance. The significance of this work is that it provides a formalized procedure for safety-critical system assurance, which could increase the confidence in system safety. It would be expected to make the safety of a system easier to explain to third parties and make the system assurance more intuitive and effective. Also, a case study on an automatic driving system is carried out to confirm the effectiveness of this approach.

Download Full-text

Generating Erroneous Human Behavior From Strategic Knowledge in Task Models and Evaluating Its Impact on System Safety With Model Checking

IEEE Transactions on Systems Man and Cybernetics Systems ◽

10.1109/tsmc.2013.2256129 ◽

2013 ◽

Vol 43 (6) ◽

pp. 1314-1327 ◽

Cited By ~ 24

Author(s):

Matthew L. Bolton ◽

Ellen J. Bass

Keyword(s):

Model Checking ◽

Human Behavior ◽

Strategic Knowledge ◽

System Safety

Download Full-text

Fuzzy Genetic Algorithm Approach for Verification of Reachability and Detection of Deadlock in Graph Transformation Systems

10.20944/preprints202010.0303.v1 ◽

2020 ◽

Author(s):

Nahid Salimi ◽

Vahid Rafe ◽

Hamed Tabrizchi ◽

Amir Mosavi

Keyword(s):

Genetic Algorithm ◽

Model Checking ◽

State Space ◽

Hybrid Approach ◽

The State ◽

Suggested Approach ◽

Safety Property ◽

Fuzzy Genetic Algorithm ◽

Fuzzy Genetic ◽

Graph Transformation Systems

model checking techniques are often used for the verification of software systems. Such techniques are accompanied with several advantages. However, state space explosion is one of the drawbacks to model checking. During recent years, several methods have been proposed based on evolutionary and meta-heuristic algorithms to solve this problem. In this paper, a hybrid approach is presented to cope with the SSE problem in model checking of systems modeled by GTS with an ample state space. Most of existence proposed methods that aim to verify systems are applied to detect deadlocks by graph transformations. The proposed approach is based on the fuzzy genetic algorithm and is designed to decline the safety property by verifying the reachability property and detecting deadlocks. In this solution, the state space of the system is searched by a fuzzy genetic algorithm to find the state in which the specified property is refuted/verified. To implement and evaluate the suggested approach, GROOVE is used as a powerful designing and model checking toolset in GTS. The experimental results indicate that the presented hybrid fuzzy method improves speed and performance by comparing other techniques

Download Full-text