Automated Result Verification with AWK

The goal of result-verificationis toprove that one execution run of a program satisjes its speciJcation. Compared with iniplenzentation-verification,result-verification has a larger scopefor applications inpractice, gives more opportunitiesfor automation and, based on the execution record not the implementation, isparticularly suitablefor complex systems. This paper proposes a technicalframework to apply this technique in practice. Weshow how to writeformal result-based specifications, how to generate LI verifier program to check a given speciJcation and to carry out resultverification according to the generated program. The execution result is written as a text jle, the verifier is written in AWK (special-purpose languagefor text processing) and verijcation is done automatically by the AWK interpreter; given the verifier and the execution result as inputs.

• Type: Conference
• Year: 2000
• Where: ICECCS
• Authors: Balkhis Abu Bakar, Tomasz Janowski
• Keywords: Execution Run, Hardware, ICECCS 2000, LI Verifier Program, Verifier