Li Tan, Jesung Kim, Insup Lee, and Oleg Sokolsky. In the proceedings of IEEE Internation Conference on Information Reuse and Integration (IRI'04), Las Vegas, NV, IEEE society, 2004.
We propose an integrated framework for testing and monitoring the model-based embedded systems. The framework incorporates three separately developed techniques: 1) test generation based on hybrid system models, 2) run-time verification, and 3) modular code generation for hybrid systems. To analyze behaviors of the system, the system model is augmented with a testing automaton that represents a given test case, and with a monitoring automaton that captures formally specified properties of the system. The augmented model allows us to perform model-level validation. In the next step, we use the modular code generator to convert the testing and monitoring automata into code that can be linked with a system implementation to perform the same analysis on the implementation level. The paper presents an overview of the framework, illustrated by a case study using the Sony AIBO robot platform.