Software engineering practices and Simulink: bridging the gap

International Journal on Software Tools for Technology Transfer - Although widely used in embedded systems design, Matlab/Simulink is not considered a state-of-the-art design environment by the...     

Repository mining for changes in Simulink and Stateflow models

Software and Systems Modeling - Model-Based Development (MBD) is widely used for embedded controls development, with MATLAB/Simulink/Stateflow being one of the most used development environments in...     

Secure and trusted partial grey-box verification

International Journal of Information Security - A crucial aspect in the development of software-intensive systems is verification. This is the process of checking whether the system has been...     

Translation of IEC 61131-3 Function Block Diagrams to PVS for Formal Verification with Real-Time Nuclear Application

The trip computers for the two reactor shutdown systems of the Ontario Power Generation (OPG) Darlington Nuclear Power Generating Station are being refurbished due to hardware obsolescence. For one of the systems, the general purpose computer originally used is being replaced by a programmable logic controller (PLC). The trip computer application software has been rewritten using function block diagrams (FBDs), a commonly used PLC programming language defined in the IEC 61131-3 standard. The replacement project’s quality assurance program requires that formal verification be performed to compare the FBDs against a formal software requirements specification written using tabular expressions (TEs). The PVS theorem proving tool is used in formal verification. Custom tools developed for OPG are used to translate TEs and FBDs into PVS code. In this paper, we present a method to rigorously translate the graphical FBD language to a mathematical model in PVS using an abstract syntax to represent the FBD constructs. We use an example from the replacement project to demonstrate the use of the model to translate a FBD module into a PVS specification. We then extend that example to demonstrate the method’s applicability to a Simulink-based design.     

Software tools for safety-critical software development

We briefly present a software methodology for safety-critical software, developed over many years to cope with industrial safety-critical applications in the Canadian nuclear industry. Following this we present discussion on software tools that have been used to support this methodology, and software tools that could be used, but have not been used for a variety of reasons. Based on our experience, we also present and motivate a list of high-level requirements for tools that would facilitate the development of safety-critical software using the presented methods, together with a small number of tools that we believe are worth developing in the future.