ABSTRACT:
Run-time verification is a novel application of formal methods that has
two important features that makes it practically applicable.  First, it is
not subject to as much state explosion as model checking and, second, it
is applicable to analysis of system  implementations rather than their
models.  Since checking is done at run time, only the current execution is
checked for requirement violations.  At the same time, information about
violations can be fed back to the system to help it correct the  problem.
The talk will outline run-time verification within the larger context of
formal methods in general and describe the necessary components for a
run-time verification framework specification of requirements,
instrumentation of the system, detection of relevant events, checking
algorithms, and the feedback mechanism.  The approach will be illustrated
using recent case studies with the MaC (Monitoring and Checking) tool,
developed by the real-time systems group at the University of
Pennsylvania.  This is joint work with Insup Lee, Sampath Kannan, Moonjoo
Kim, Mahesh Viswanathan, Usa Sammapun.