Systematic testing and formal verification to validate reactive programs |
| |
Authors: | Monika Müllerburg Leszek Holenderski Olivier Maffeis Agathe Merceron Matthew Morley |
| |
Affiliation: | (1) Schloss Birlinghoven, GMD-SET, D-53757 Sankt Augustin, Germany |
| |
Abstract: | The use of systematic testing and formal verification in the validation of reactive systems implemented in synchronous languages is illustrated. Systematic testing and formal verification are two techniques for checking the consistency between a program and its specification. The approach to validation is through specification: two system views are developed in addition to the program, a behavioural specification for systematic testing and a logical specification for formal verification. Pursuing both activities, reactive programs can be validated both more efficiently (in terms of costs) and more effectively (in terms of confidence in correctness). This principle is demonstrated here using the well known lift example. |
| |
Keywords: | Validation systematic testing formal verification reactive systems synchronous programming |
本文献已被 SpringerLink 等数据库收录! |