Programming reflexes (Extended abstract)

摘要

Formal verification serves as the theoretical basis for the engineering task of correctness and performance (quality) assurance. State of the art model checking, automatic specification refinement and theorem proving are employed to tackle the often undecidable (as imposed by the halting problem) task of complete verification. In this paper we formalize, prove and demonstrate a new unobtrusive way to test a system during runtime. Invocation of actions and examination of reaction of the system and components of the system are examined in run time in an holistic abstract manner, namely, the current state (e.g., state snapshot) the executable (e.g., program) and the environmental current condition (e.g., operating system, hypervisor) are examined by invoking actions and examining the reactions without influencing the actual execution semantics.