The realization of the software part of a safety-related system (SRS) is a challenging task due to the necessary verification activities. To assure that safety-related systems will offer the necessary risk reduction required to achieve the desired safety integrity level, the IEC 61508 standard defines requirements for the software safety lifecycle. The standard specifies verification activities associated with all phases of the lifecycle. In this paper, an approach to automate the verification activity with focus on the software part of SRSs is presented. Based on this, the software code, which is implemented using the IEC 61131-3 programming standard and the PLCopen specification, is automatically transformed to Uppaal formal models using a software tool called SA2TA (Safety Application to Timed Automata). To further automate the verification process, test cases based on equivalence class analysis and combination of states are generated utilizing the test case generator TCG. A laboratory real world case study is used to demonstrate the applicability of the proposed approach. The main contribution of this paper is the formalization approach of the application software behaviour in TCTL (Time Computational Temporal Logic). |
