Issue No. 05 - September/October (2004 vol. 19)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/MIS.2004.54
Robert A. Riemenschneider , SRI International
Hassen Sa?di , SRI International
Bruno Dutertre , SRI International
Model checking, a formal approach to determining whether an abstract model of a system has some desired property, is useful in assessing the dependability of extremely complex agent-based systems. Model checking requires figuring out how systems are modeled, how dependability properties are expressed, and how to automatically determine whether the model has such properties. Using this approach on complex agent-based systems is often considered infeasible, but abstraction techniques can help reduce the level of complexity. Model checking is useful not only for finding flaws in an undependable system but also for determining whether a system meets its dependability objectives. In particular, you can use model checking to focus system testing such that it provides more return for a given level of investment in testing. The application of model checking to UltraLog, a large, complex agent-based system, has demonstrated its usefulness.
agent-based systems, dependable systems, abstraction, model checking, test generation
H. Sa?di, B. Dutertre and R. A. Riemenschneider, "Using Model Checking to Assess the Dependability of Agent-Based Systems," in IEEE Intelligent Systems, vol. 19, no. , pp. 62-70, 2004.