Leveraging Formal Verification Techniques for Design-Time Animation of Reactive Control Programs

In industrial automation, end users, who usually have no or only limited programming expertise, often need to change and adapt the control program at hand. This results in high demands on end-user programming environments with respect to supporting, guiding, and supervising end users. In the project MONACO, we developed a domain-specific language and respective tools for end-user programmers. In particular, we developed a verification technique and semantic assistance tools for preventing end users from introducing semantic errors that violate specified contracts and constraints. In this paper, we present a further tool for supporting end users. The knowledge derived in the verification algorithm about states at particular code positions is leveraged in a design-time animation tool which displays the possible states of the machine. Hence, an end user can gain an intuitive understanding of the program and assess the consequences of program changes already at design time and without conducting test run.