Dominik Hurnaus, Herbert Prähofer,
"Programming Assistance Based on Contracts and Modular Verification in the Automation Domain"
: SAC '10 Proceedings of the 2010 ACM Symposium on Applied Computing, ACM Digital Library, Seite(n) 2544-2551, 3-2010, ISBN: 978-1-60558-639-7
Programming Assistance Based on Contracts and Modular Verification in the Automation Domain
Sprache des Titels:
SAC '10 Proceedings of the 2010 ACM Symposium on Applied Computing
In industrial automation, control software often has to get changed and adapted by domain experts and end users who have no or only limited software development expertise. This results in high demands on programming environments with respect to supporting, guiding, and supervising the programming tasks. In this paper we present an approach based on model checking and artificial intelligence techniques to guide domain experts in building control software which is guaranteed to obey specified contracts and constraints. The work is based on Monaco which is a domain-specific language for programming automation solutions. As Monaco employs a hierarchical component approach, the verification is done hierarchically where an upper component is verified against the contracts of its subcomponents. The verification approach is leveraged in different programming support systems which give immediate feedback about valid and invalid programs in an integrated development environment.