TitleAn Extended Framework for the Validation and Verification of Situation-Aware Middleware Architectures
Publication TypeConference Paper
Year of Publication2003
AuthorsKim, SE., P. In, and R. Bharadwaj
Conference NameProceedings Ground System Architectures Workshop (GSAW 2003)
Conference LocationManhattan Beach, California

Model checking is a technique that has been successfully applied for the validat ion and verification of hardware specifications and communication protocols. In mission-critical syst ems of NASA and the DoD, various mobile devices generate information dynamically, and their state ch anges with time. Most often, a situation serves as a trigger for a new situation. Therefore, it is nec essary to extend existing model checking methods and tools in order to apply them for the validat ion and verification of situation-aware, mission-critical applications such as DoD command and contro l systems or the Navy s Total Ship Computing Environment. However, there are several problems to be ov ercome 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 distrib uted real-time and embedded system must necessarily be highly adaptable, secure, and reliable. Exis ting system development techniques therefore need to be extended so that future systems have the capability to meet these new system requirements.

Full Text

Kim etal2003.pdf

NRL Publication Release Number