Herbert Prähofer, Dominik Hurnaus,
"Leveraging Formal Verification Techniques for Design-Time Animation of Reactive Control Programs"
: Proc. of the Seventh IASTED International Conference on Human-Computer Interaction (HCI 2012), ACTA Press, 2012
Leveraging Formal Verification Techniques for Design-Time Animation of Reactive Control Programs
Sprache des Titels:
Proc. of the Seventh IASTED International Conference on Human-Computer Interaction (HCI 2012)
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.