Keywords
model checking, e-processes, web services, electronic contracting, dependability auditing
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.
Original Publication Citation
Anderson, B.B., Hansen, J.V., and Lowry, P.B. “Dependability Auditing with Model Checking” 11th Annual Americas Conference on Information Systems (AMCIS), Omaha, NE, August 11-14, pp. 3147-3156, 2005.
BYU ScholarsArchive Citation
Anderson, Bonnie; Hansen, James; and Lowry, Paul Benjamin, "Dependability Auditing with Model Checking" (2005). Faculty Publications. 9303.
https://scholarsarchive.byu.edu/facpub/9303
Document Type
Peer-Reviewed Article
Publication Date
2005
Publisher
11th Annual Americas Conference on Information Systems
Language
English
College
Marriott School of Business
Department
Information Systems Management
Copyright Use Information
https://lib.byu.edu/about/copyright/