Model-based Runtime Verification Framework for Self-optimizing Systems |
| |
Authors: | Y. Zhao, S. Oberthü r, M. Kardos,F.J. Rammig |
| |
Affiliation: | Heinz Nixdorf Institute, University of Paderborn, Paderborn, Germany |
| |
Abstract: | This paper describes a novel on-line model checking approach offered as service of a real-time operating system (RTOS). The verification system is intended especially for self-optimizing component-based real-time systems where self-optimization is performed by dynamically exchanging components. The verification is performed at the level of (RT-UML) models. The properties to be checked are expressed by RT-OCL terms where the underlying temporal logic is restricted to either time-annotated ACTL or LTL formulae. The on-line model checking runs interleaved with the execution of the component to be checked in a pipelined manner. The technique applied is based on on-the-fly model checking. More specifically for ACTL formulae this means on-the-fly solution of the NHORNSAT problem while in the case of LTL the emptiness checking method is applied. |
| |
Keywords: | Model-based Runtime Verification On-the-fly ACTL/LTL Model Checking Self-optimizing System |
本文献已被 ScienceDirect 等数据库收录! |