Paper Info
Title
Increasing dependability by means of model-based acceptance test inside RTOS
Abstract
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.
Year
DOI
Venue
2005
10.1007/11752578_125
PPAM
Keywords
Field
DocType
dependability issue,actl formula,runtime verification,proposed verification approach,applied technique,component-based self-optimizing system,emptiness checking method,model-based acceptance test,ltl formula,alternative acceptance test,temporal logic,model checking
Computation tree logic,Kripke structure,Dependability,Model checking,Computer science,Runtime verification,Linear temporal logic,Temporal logic,Reactive system,Distributed computing
Conference
Volume
ISSN
ISBN
3911
0302-9743
3-540-34141-2
Citations 
PageRank 
References 
1
0.34
10
Authors
5
Name
Order
Citations
PageRank
Yuhong Zhao1235.81
Simon Oberthür2395.90
Norma Montealegre3102.89
Franz J. Rammig428540.47
Martin Kardos592.61