An Extended Framework for the Validation and Verification of Situation-Aware Middleware Architectures
TEXAS A AND M UNIV COLLEGE STATION DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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 Navys 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 VV 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.
- Information Science
- Computer Programming and Software
- Computer Systems Management and Standards