Guarding the guard: Using meta formal specifications to guard assertions

摘要

The promise of formal verification of system-of-systems is in harnessing the power and accuracy of modern day computers to create trust-worthy systems. The success of formal verification techniques depends, to large degree, on the existence of a sound and complete collection of formally written requirements. To date, there is no known methodology for assuring that a collection of requirements, formal or otherwise, is complete. The use of meta-assertions suggested in this paper is a step in that direction. As their name suggests, meta-assertions are (second level) assertions about (first-level) assertions. While first-level assertions are formal, executable statements about desired or undesired system behavior, second-level (meta)-assertions are formal and executable statements about desired or undesired behavior of level-one assertions. This paper examines an example of meta-assertions and discusses their use within a run-time verification environment.