Modelling and Synthesis of Safety-critical Software with IEC 61499

Abstract

Software forms a central part of modern industrial control systems. It is routinely used, nowadays, to control a variety of physical processes through an integration of computing elements with sensors and actuators. The falling cost of digital electronics have also led to an increasing use of multiple computing units to control large distributed systems in a networked environment. The design of such systems is complex, and requires programming methodologies that seamlessly support the specification of distributed and concurrent software. The methodologies should further be easy to understand, and should provide design artefacts that naturally support reuse. Most existing techniques for developing control software, however, are unable to support these features. Recognizing this need, the IEC 61499 standard has been proposed as a standard for developing distributed industrial control systems. This standard prescribes a component-oriented approach for developing distributed control software, based on function blocks. The graphical nature and the encapsulation offered by function blocks provide an intuitive way to describe software in a reusable manner. Executable code can further be automatically synthesized from these function blocks. This helps to simplify the task of programming, while ensuring more reliable software. The standard, however, lacks the semantic rigour necessary for the automated verification and unambiguous execution of function blocks. In particular, the model of concurrency for a network of function blocks running in a centralized or distributed fashion is not clear. Several scheduling techniques have been proposed to overcome this problem. Various run-time environments, each adhering to a particular scheduling policy, have correspondingly been developed to execute function blocks. This has resulted in incompatible behaviours, as well as complications in the formal verification of function block programs. This thesis addresses these problems by proposing a formal model for distributed IEC 61499 systems based on the globally asynchronous locally synchronous (GALS) paradigm. For a centralized implementation, function block networks are executed synchronously, while distibuted implementations are executed as a collection of synchronous islands that communicate with each other asynchronously. The semantics for synchronous execution is provably correct for any arbitrary composition of function blocks. Moreover, run-time scheduling overhead is eliminated, as all scheduling decisions can be made before a program is run. These semantics further enable formal verification of function blocks using the well-known concept of synchronous observers. The approach proposed in this thesis also allows communication in distributed systems to be specified in an abstract way, which does not yet imply any particular implementation. This abstraction can be automatically refined to obtain various implementations with different trade-offs. This has been done in a manner that is fully compatible with the IEC 61499's notion of communication function blocks. A prototype compiler has been developed to synthesize either centralized or distributed code from function block programs. The code generated by this compiler is markedly superior to that produced by existing techniques in terms of execution speed, as well as code size. These results demonstrate the viability of the ideas presented in this thesis for the development of practical industrial control software.