Irman Faqrizal

Abstract:

The rapid advancement in information technology opens up promising opportunities for industrial automation systems. By minimising human intervention, the industry can significantly reduce costs and enhance the system's overall quality. Nevertheless, industrial automation systems are facing many challenges. One of them is how to verify and analyse the quantitative aspects of the system in the presence of an unpredictable environment. Formal methods have been employed recently to verify the system's correctness. However, conventional methods are often applied only at design time, neglecting the runtime execution impacted by the environment. The second major challenge in industrial automation is the need for techniques to support long-running and evolving systems. Manual modification involving human intervention defeats the purpose of automation while also being costly, time-consuming, and erroneous. An automation system must be able to evolve automatically according to requirements. The main contributions of this thesis are twofold. First, probabilistic model checking is applied to verify and analyse the quantitative aspects of the system originating from the environment. This method consists of formal modelling, monitoring, and probabilistic model computation. The results can be used to observe the impact of the environment and to suggest improvements associated with the system's quantitative features, such as productivity. The second contribution consists of two approaches for evolving automation systems. In the first approach, runtime enforcement techniques are applied to make the application adapt to the requirements. This is done by automatically synthesising and integrating new logical components called enforcers to modify the system's executions according to the requirements. The second proposal incorporates various algorithms applied to the behavioural models of the applications for generating evolution guidelines. These guidelines contain modifications to be applied to make the application satisfy the given requirements. Both solutions allow developers to avoid errors and unnecessary modifications when evolving industrial automation systems. The contributions are aimed at automation systems designed with IEC 61499, a promising industrial standard with numerous positive characteristics. Existing and new software tools are used and developed to conduct case studies and experiments validating the proposed methods.