Dependability Auditing with Model Checking

摘要

Model checking offers a methodology for determining whether a model satisfies a list of correctness requirements. Wernpropose a theory of dependability auditing with model checking based on four principles: (1) The modeling process should bernpartitioned into computational components and behavioral components as an aid to system understanding; (2) The complexrnsystem will be abstracted to create a model; (3) A language must be available that can represent and evaluate states andrnprocesses that evolve over time; (4) Given an adequate model and temporal specifications, a model checker can verifyrnwhether or not the input model is a model of that specification: the specification will not fail in the model. We demonstraternthis theoretical framework with Web Services and electronic contracting.