An Extended Framework for the Validation and Verification of Situation-Aware Middleware Architectures
Abstract
Model checking is a technique that has been successfully applied for the validation and verification of hardware specifications and communication protocols. In mission critical systems of NASA and the DoD, various mobile devices generate information dynamically, and their state changes with time. Most often, a situation serves as a trigger for a new situation. Therefore, it is necessary to extend existing model checking methods and tools in order to apply them for the validation and verification of situation-aware, mission-critical applications such as DoD command and control systems or the Navy's Total Ship Computing Environment. However, there are several problems to be overcome before these techniques become practical, such as overcoming the state explosion problem and adapting the V&V systems and algorithms to this application area. In this paper, we propose a new technique, founded on combining existing techniques in theorem proving and model checking to extend the application area of existing pure model checking methods. This paper also introduces state space reduction methods based on abstraction that ameliorate the state explosion problem. Future distributed real-time and embedded system must necessarily be highly adaptable, secure, and reliable. Existing system development techniques therefore need to be extended so that future systems have the capability to meet these new system requirements.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 01, 2003
- Accession Number
- ADA465139
Entities
People
- Peter In
- Ramesh Bharadwaj
- Sangeun Kim
Organizations
- Texas A&M University