Increasing dependability by means of model-based acceptance test inside RTOS

Component-based self-optimizing systems can adjust themselves over time to dynamic environments by means of exchanging components. In case that such systems are safety-critical, the dependability issue becomes paramountly significant. This paper presents a novel model-based runtime verification to increase dependability for the self-optimizing systems of this kind. The proposed verification approach plays a role of an alternative acceptance test transparently integrated in RTOS, named model-based acceptance test. The verification is performed at the level of (RT-UML) models representing the systems under consideration. The properties to be checked are expressed by RT-OCL where the underlying temporal logic is restricted to either time-annotated ACTL or LTL formulae. The applied technique is based on the on-the-fly model checking, which runs interleaved with the execution of the checked system in a pipelined manner. More specifically, for ACTL formulae this means an on-the-fly solution to the NHORNSAT problem, while in the case of LTL formulae, the emptiness checking method is applied.