Digital instrumentation and control (I&C) systems are increasingly being used for implementing safety-critical applications such as nuclear power plant safety systems. The exhaustive verification of these systems ...
详细信息
Digital instrumentation and control (I&C) systems are increasingly being used for implementing safety-critical applications such as nuclear power plant safety systems. The exhaustive verification of these systems is challenging, and verification methods such as testing and simulation are typically insufficient. Model checking is a formal method for verifying the correctness of a system design model. The requirements of the system are formalised using temporal logic, and the behaviour of the system model is exhaustively analysed with respect to these formal specifications. The method is very effective in finding hidden design errors. Model checking is computationally very demanding, and thus one of the challenges in applying model checking is its scalability. This dissertation discusses the verification of larger systems implementing multiple functions using model checking. First of all, this dissertation presents methodology for modelling safety system designs, and describes a simple abstraction technique for models of these systems that utilises modular over-approximating abstractions. Furthermore, the dissertation presents the development of an iterative abstraction refinement algorithm for the purpose of automatically finding an abstraction level suitable for verification. This dissertation also studies hardware failures, and creates an extension of the safety system modelling methodology that enables the analysis of fault-tolerance properties in large many- redundant system assemblies. The methodology follows closely the conventions of probabilistic risk assessment (PRA), and serves as a first step for further integration between model checking and PRA. Finally, this work presents the development of a test set generation technique based on model checking that utilises the structure of function block diagram (FBD) programs. The results of this work have a high significance to safety because the developed techniques can be used to verify the correctness of safety
This paper presents a new approach to reduce finite state machines with respect to a CTL formula to alleviate state explosion problem. Reduction is achieved by removing parts useless to the formula of original machine...
详细信息
ISBN:
(纸本)9780769542485
This paper presents a new approach to reduce finite state machines with respect to a CTL formula to alleviate state explosion problem. Reduction is achieved by removing parts useless to the formula of original machines. The main contribution of this paper is to exploit relations among subformulas of the CTL formula so as to gain more reduction, as well as to extend traditional pruning method, which handles only existential formulas, to handle universal formulas. Based on this kind of reduction, verification of a large system, which usually consists of several components, can be done by evaluating properties on a reduced version of the system, which is built by composing components of the system one by one while doing reduction after each composition. Experimental results show the effectiveness of the approach. Especially when a property is written in a more detailed way, that is to describe the system part by part, the approach has a great potential.
This paper presents a new approach to reduce finite state machines with respect to a CTL formula to alleviate state explosion problem. Reduction is achieved by removing parts useless to the formula of original machine...
详细信息
This paper presents a new approach to reduce finite state machines with respect to a CTL formula to alleviate state explosion problem. Reduction is achieved by removing parts useless to the formula of original machines. The main contribution of this paper is to exploit relations among subformulas of the CTL formula so as to gain more reduction, as well as to extend traditional pruning method, which handles only existential formulas, to handle universal formulas. Based on this kind of reduction, verification of a large system, which usually consists of several components, can be done by evaluating properties on a reduced version of the system, which is built by composing components of the system one by one while doing reduction after each composition. Experimental results show the effectiveness of the approach. Especially when a property is written in a more detailed way, that is to describe the system part by part, the approach has a great potential.
We present a polytime computable state equivalence that is defined with respect to a given CTL formula. Since it does not attempt to preserve all CTL formulas, like bisimulation does, we can expect to compute coarser ...
详细信息
We present a polytime computable state equivalence that is defined with respect to a given CTL formula. Since it does not attempt to preserve all CTL formulas, like bisimulation does, we can expect to compute coarser equivalences. This equivalence can be used to reduce the complexity of model checking a system of interacting FSMs. Additionally, we show that in some cases our techniques can detect if a formula passes or fails, without forming the entire product machine. The method is exact and fully automatic, and handles full CTL.
暂无评论