Department of Computer Sciences 1999 ACL2 Workshop March 29 - March 31, 1999

Verified Result Checking for Safety of an Automatic Test Plan Generator

We describe our approach of runtime result verification to guarantee correctness of an automatic test plan generator for relay circuit blocks used as switching devices e.g. in railway signal boxes. These devices have to be certified periodically. Test roboters are used to execute test plans (certain collections of measurements) which formerly have been invented by engineers and which are now to be generated by an expert system.

Runtime result verification guarantees the (partial) correctness of the test plan generator by checking every single resulting test plan. The checker works as a filter, either embedded or offline, sufficient to guarantee the specified post condition, which is that the test roboter will detect any malfunction in the circuit by at least one non-succeeding measure of the test plan. We are using ACL2 to prove this property. Moreover, the checker has to be implemented correctly, and it has to be executed safely, without the risk to be affected by the unverified environment.

Wolfgang Goerigk