Soliman, D: Verification and Validation of Logic Control Saf

transformation rules are formalised based on the meta-models. A prototype transformation tool is therefore developed and tested using some real safety applications. The next step is the formalisation of safety applications written in the FBD programing language and required UPPAAL systems. And of course, formalisation of detailed transformation rules is also defined. This led to developing the end version of the safety application to the timed automata SA2TA tool. This was a joint venture with the Software Engineering group (Prof. Thramboulidis) in Patras University, Greece.As a case study to test the applicability of the transformation tool, the SA2TA is then used as part of a whole methodology to upgrade a legacy system to conform to safety standards. The legacy system needed to be upgraded is an XY drawing table located in the automation laboratory in Saarland University, Germany. The suggested methodology was applied to the XY table, and the designed safety application is transformed to a UPPAAL TA system for verification purposes. Therefore, the verification process is carried out based on safety functionalities defined through the designing stage. It was found that not all safety functionalities were satisfied on the UPPAAL system, which led to some modifications in the designed safety application to meet the required safety functionalities.Some possible technical extensions to make the proposed methodology even easier to use are for example, the automatic transfer of simulation traces between PLC tools and UPPAAL in both directions. From PLC tools to UPPAAL for automatic validation and from UPPAAL to PLC tools for the visualisation of counter examples.However, one question still remains. Since there is a gap between safety engineering and software engineering; who is responsible for applying verification processes on the resulting UPPAAL system from safety applications? It is believed that more effort is required in the direction of verification to minimise this gap and facilitate obtaining safety properties in formal languages.