System modelling for safety and fault analysis using the software tool NP-Circuit

NP-Circuit is a generic modelling tool which enables the logical functionality of complete systems to be modelled, and from this a formal verification of the system behaviour against its overall specification is derived. Unlike simulation, which derives outputs from a set of inputs, NP-Circuit permits input conditions to be derived which satisfy specified output criteria. In this context it enables potential conflicts to be extracted and all their sources to be identified, a task which can only be undertaken clumsily and inexactly using a simulation tool. This together with a guaranteed mathematical solution to the model makes the tool well suited to analysing and verifying the safety requirements of systems and also enables fault tree and failure mode analysis to be undertaken. Central to the package is a theorem prover, the algorithm of which makes solutions insensitive to circuit complexity and so fast solution times to complex system models can be achieved. This paper demonstrates that by using a graphical approach, formal methods can be introduced into the design process alongside other methods, and need not be thought of as esoteric and requiring specialist formal methods knowledge