Abstract
Model checking offers a methodology for determining whether a model satisfies a list of correctness requirements. We propose a theory of dependability auditing with model checking based on four principles: (1) The modeling process should be partitioned into computational components and behavioral components as an aid to system understanding; (2) The complex system will be abstracted to create a model; (3) A language must be available that can represent and evaluate states and processes that evolve over time; (4) Given an adequate model and temporal specifications, a model checker can verify whether or not the input model is a model of that specification: the specification will not fail in the model. We demonstrate this theoretical framework with Web Services and electronic contracting.
Recommended Citation
Anderson, Bonnie; Hansen, James; and Lowry, Paul Benjamin, "Dependability Auditing with Model Checking" (2005). AMCIS 2005 Proceedings. 276.
https://aisel.aisnet.org/amcis2005/276