Component-Based Development of Runtime Observers in the COMDES Framework

Wei Guan, Gang Li, Christo K. Angelov, Søren Top

Research output: Contribution to journalJournal articleResearchpeer-review

Abstract

Formal verification methods, such as exhaustive model checking, are often infeasible because of high computational complexity. Runtime observers (monitors) provide an alternative, light-weight verification method, which offers a non-exhaustive but still feasible approach to monitor system behavior 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 is facilitated by model-driven engineering. The
presented method has been experimentally validated in an industrial safety-related medical ventilator case study.
Original languageEnglish
JournalInternational Journal of Software Engineering
Volume2
ISSN1925-7899
DOIs
Publication statusPublished - 2013

Fingerprint

Model checking
Embedded systems
Computational complexity
Formal verification

Cite this

@article{f8428249e0b7422ba471bad3582aba1b,
title = "Component-Based Development of Runtime Observers in the COMDES Framework",
abstract = "Formal verification methods, such as exhaustive model checking, are often infeasible because of high computational complexity. Runtime observers (monitors) provide an alternative, light-weight verification method, which offers a non-exhaustive but still feasible approach to monitor system behavior 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 is facilitated by model-driven engineering. Thepresented method has been experimentally validated in an industrial safety-related medical ventilator case study.",
author = "Wei Guan and Gang Li and Angelov, {Christo K.} and S{\o}ren Top",
year = "2013",
doi = "10.2316/Journal.213.2013.2.213-1044",
language = "English",
volume = "2",
journal = "International Journal of Software Engineering",
issn = "1925-7899",
publisher = "ACTA Press",

}

Component-Based Development of Runtime Observers in the COMDES Framework. / Guan, Wei; Li, Gang ; Angelov, Christo K.; Top, Søren.

In: International Journal of Software Engineering, Vol. 2, 2013.

Research output: Contribution to journalJournal articleResearchpeer-review

TY - JOUR

T1 - Component-Based Development of Runtime Observers in the COMDES Framework

AU - Guan, Wei

AU - Li, Gang

AU - Angelov, Christo K.

AU - Top, Søren

PY - 2013

Y1 - 2013

N2 - Formal verification methods, such as exhaustive model checking, are often infeasible because of high computational complexity. Runtime observers (monitors) provide an alternative, light-weight verification method, which offers a non-exhaustive but still feasible approach to monitor system behavior 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 is facilitated by model-driven engineering. Thepresented method has been experimentally validated in an industrial safety-related medical ventilator case study.

AB - Formal verification methods, such as exhaustive model checking, are often infeasible because of high computational complexity. Runtime observers (monitors) provide an alternative, light-weight verification method, which offers a non-exhaustive but still feasible approach to monitor system behavior 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 is facilitated by model-driven engineering. Thepresented method has been experimentally validated in an industrial safety-related medical ventilator case study.

U2 - 10.2316/Journal.213.2013.2.213-1044

DO - 10.2316/Journal.213.2013.2.213-1044

M3 - Journal article

VL - 2

JO - International Journal of Software Engineering

JF - International Journal of Software Engineering

SN - 1925-7899

ER -