Towards the safe-IOCOS relation -- On testing and correction of errors in an implementation to ensure safety

Sammanfattning: The technological advancement that has occurred at a blistering pace in the past decades has enabled manufacturing companies to conceive innovative products. However, to meet growing demands of consumers, manufacturing companies are expected to maintain a steady production rate without compromising product quality. To meet these requirements, the industrial sector is increasingly using robots and other automated machinery. Automated machines are predominantly controlled via programmable logic controllers (PLCs) to carry out the nominal tasks. For safety critical tasks, though, special devices in conjunction with safety PLCs are used to prevent material damage and accidents leading to human injuries. Before physical commissioning of a manufacturing system, the nominal PLC code is tested to uncover faults. This can be done either by running tests on the physical system or using a simulation model via virtual commissioning . However, the safety code is usually tested during the factory acceptance test  phase on the actual physical system. The faults found in the safety code are corrected manually, which is time consuming and error prone. The formal methods community has developed testing relations and approaches that can be used to automatically test and amend faults in the implementation. The work presented in this thesis is based on such a testing relation and formal approach. The safe input-output conformance simulation relation (safe-IOCOS) is a testing relation that requires equality for traces composed of safety behaviors. However, in practical settings, many safety behaviors in a production system are implemented for each nominal operation. And these behaviors get tested multiple times during testing, which increases the testing time unnecessarily. To counter this problem, an approach to minimize testing time is proposed. Furthermore, an approach to automatically amend a faulty implementation to ensure safety properties with respect to a safety specification is presented. This approach uses the procedure of synthesis , from the framework of supervisory control theory, based on the infimial controllable superlanguage , which not only removes the faults from the implementation but also guarantees to make it safe-IOCOS.