Development of a verification method for the FBD-style design specification using ESDT and SMV

Abstract

As PLCs are widely used in the digital I&C systems of nuclear power plants (NPPs), the safety of PLC software has become the most important consideration. Software safety is an important property for safety critical systems, especially those in aerospace, satellite and nuclear power plants, whose failure could result in danger to human life, property or environment. It is recently becoming more important due to the increase in the complexity and size of safety critical systems. This approach proposes a method to perform effective verification activities on the traceability analysis and software design evaluation in the software design phase. In order to perform the traceability analysis between a Software Requirements Specification (SRS) written in a natural language and a Software Design Specification (SDS) written in Function Block Diagram (FBD), this method uses extended-structured decision tables (ESDTs). ESDTs include information related to the traceability analysis from a text-based SRS and a FBD-based SDS, respectively. Through comparing with both ESDTs from a SRS and ESDTs from a SDS, the effective traceability analysis of both a text-based SRS and a FBD-based SDS can be achieved. For the software design evaluation, a model checking which is mainly used to verify PLC programs formally is used in this research. A FBD-style design specification is translated into input languages of the SMV by translation rules and then the FBD-style design specification can be formally analyzed using SMV.