On the verification of safety requirements: application to industrial machine

Automated facilities now frequently call upon programmable logic controllers (PLCs) for ensuring personal safety. This obliges us to consider the safety of the software installed in these PLCs and thus the errors likely to affect them. This concern requires us to implement design methods to prevent introducing such errors and to develop confidence in the performance of these facilities.
This study investigates one of the software development options, which involves combining conventional practices (such as simulation-based testing) implemented by automation engineers with formal verification techniques based on software engineering. The latter techniques have not yet been used in the machinery field, but they enable us to ensure that a safety requirement is 100% confirmed and that the software component fulfilling this requirement is effectively free of errors that could compromise operator safety. Such techniques have their limitations and, for application in the machinery field, require monitoring of a specific development process.
We therefore propose a development process, which focuses on safety issues. This process starts by an expression of system requirements in order to yield a set of relevant safety requirements. This initial stage is important for formalising and detecting safety requirements based on global risk assessment, whilst these issues are not necessarily considered right from the start of design in the machinery safety world. Such requirements are then used to encode, and then validate, the system software. Validation could be performed either by simulation or applying formal verification techniques, depending on the maturity, skill and resources implemented by the designer.