Wei Guan, Gang Li, and Søren Top
Domain-specific frameworks, model-based analysis, runtime verification, multicore
Formal verification methods, such as exhaustive model checking, are often infeasible because of high computational complexity. Runtime observers provide an alternative, light-weight verification method, which offers a non-exhaustive but still feasible approach to monitor system behaviour against formally specified properties. This paper presents a component-based design method for runtime observers in the context of COMDES framework (a component-based framework for distributed embedded system and its supporting tools). Therefore, runtime verification can be facilitated by model-driven engineering. The presented method has been experimentally validated in an industrial safety-related medical ventilator case study.
Important Links:
Go Back
