AMC - Tool support for automating Model Checking Lifecycle

Abstract

In model checking, the most time consuming stage is oftentimes not writing the formal model (of the system to be analyzed) itself but validating the model: ensuring the correct system has been modeled, before ensuring that the system is correct. This is due to the fact that ancillary tool support for formal verification has been chronically inadequate, especially in processing and understanding the output from large and complex models. We present an integrated tool framework, called AMC and implemented in Java, to aid the model checking process in all its stages. AMC consists of a parameterized automated model generator, a translator from unstructured model checking output to a general XML trace format, an execution trace visualizer, an interactive model simulator, and an automated results analyzer that produces PDF reports from the model checking runs. As a case study, we use a clock synchronization algorithm recently developed at NASA and the evmdd-smc model checker developed at NIA.