首页 | 本学科首页   官方微博 | 高级检索  
     


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 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号