Model checking PSL safety properties

Abstract

Model checking is a modern, efficient approach to gaining confidence of the correctness of complex systems. It outperforms conventional testing methods especially in cases where a high degree of confidence in the correctness of the system is required, or when the test runs of the system are difficult to reproduce accurately. In model checking the system is verified against a specification that is expressed in a formal specification language. The main challenges are that the process requires quite a lot of training, experience, and computing power. Recent developments in the field of model checking address all of these issues.

Safety properties are a subset of formal specifications that are simpler to verify than formal specifications in the general case. Additionally, safety properties can be used to improve conventional testing methods by observing the behaviour of the system at runtime and reporting the detected violations of the safety properties, which are more expressive than the properties used with conventional testing. In model checking, recognising and separately verifying safety properties can give faster verification times than just processing all properties without a specialised algorithm for safety properties.

One of the problems related to model checking is creating specifications that are meaningful to both humans and to model checking tools. One specification language that focuses on this problem is the IEEE 1850 standard Property Specification Language (PSL). It is not as widely supported by academic model checking tools as linear temporal logic (LTL) or computation tree logic (CTL), but it has many features that make writing specifications easier for engineers.

This work describes a method for verifying PSL safety properties by converting them to transducers, a variant of symbolic finite automata. The semantics in the most current proposal for the revised PSL standard is reviewed, and additional operators are introduced for formula rewriting. The main contributions of this work are the PSL translation and its proof of correctness with respect to the presented semantics, and a prototype implementation of an algorithm for model checking PSL safety properties. The implementation is built on top of the NuSMV model checker, a modern, open-source tool that previously had little support for PSL. Experiment results are presented to show the feasibility of the implemented approach.