A Taxonomy of Modelling Decisions for Embedded Systems Verification

Angelika H. Mader, Hanno Wupper, Mieke Boon, J. Marincic

Research output: Book/ReportReportProfessional

17 Downloads (Pure)

Abstract

During model construction a number of decisions has to be taken. Often, decisions remain implicit, which has consequences for the correct interpretation of the model, and provides a source of miscommunication between different stakeholders and domain experts. We present a taxonomy of decisions guiding the modelling process and helping to distinguish, document and order the choices and assumptions involved. We focus on modelling of embedded systems, the purpose of the models we construct is formal verification. As a consequence we model both, control software and the controlled environment. Moreover, we aim at models in a formal representation, suitable for, e.g., model checking. The explicitness of modelling decisions allows to assess the quality of models and to clarify how meaningful verification results are. The taxonomy is a result of conceptual analysis and not bound to certain languages, methods, and tools. It can be used as complement for existing modelling methods.
Original languageEnglish
Place of PublicationEnschede
PublisherDistributed and Embedded Security (DIES)
Number of pages14
Publication statusPublished - 24 May 2008

Publication series

NameCTIT Technical Report Series
No.08-37
ISSN (Print)1381-3625

Fingerprint

Taxonomies
Embedded systems
Model checking

Keywords

  • EWI-12763
  • IR-64770
  • METIS-256116

Cite this

Mader, A. H., Wupper, H., Boon, M., & Marincic, J. (2008). A Taxonomy of Modelling Decisions for Embedded Systems Verification. (CTIT Technical Report Series; No. 08-37). Enschede: Distributed and Embedded Security (DIES).
Mader, Angelika H. ; Wupper, Hanno ; Boon, Mieke ; Marincic, J. / A Taxonomy of Modelling Decisions for Embedded Systems Verification. Enschede : Distributed and Embedded Security (DIES), 2008. 14 p. (CTIT Technical Report Series; 08-37).
@book{d66dfc008c3647f4936a2a88e0801847,
title = "A Taxonomy of Modelling Decisions for Embedded Systems Verification",
abstract = "During model construction a number of decisions has to be taken. Often, decisions remain implicit, which has consequences for the correct interpretation of the model, and provides a source of miscommunication between different stakeholders and domain experts. We present a taxonomy of decisions guiding the modelling process and helping to distinguish, document and order the choices and assumptions involved. We focus on modelling of embedded systems, the purpose of the models we construct is formal verification. As a consequence we model both, control software and the controlled environment. Moreover, we aim at models in a formal representation, suitable for, e.g., model checking. The explicitness of modelling decisions allows to assess the quality of models and to clarify how meaningful verification results are. The taxonomy is a result of conceptual analysis and not bound to certain languages, methods, and tools. It can be used as complement for existing modelling methods.",
keywords = "EWI-12763, IR-64770, METIS-256116",
author = "Mader, {Angelika H.} and Hanno Wupper and Mieke Boon and J. Marincic",
note = "submitted",
year = "2008",
month = "5",
day = "24",
language = "English",
series = "CTIT Technical Report Series",
publisher = "Distributed and Embedded Security (DIES)",
number = "08-37",

}

Mader, AH, Wupper, H, Boon, M & Marincic, J 2008, A Taxonomy of Modelling Decisions for Embedded Systems Verification. CTIT Technical Report Series, no. 08-37, Distributed and Embedded Security (DIES), Enschede.

A Taxonomy of Modelling Decisions for Embedded Systems Verification. / Mader, Angelika H.; Wupper, Hanno; Boon, Mieke; Marincic, J.

Enschede : Distributed and Embedded Security (DIES), 2008. 14 p. (CTIT Technical Report Series; No. 08-37).

Research output: Book/ReportReportProfessional

TY - BOOK

T1 - A Taxonomy of Modelling Decisions for Embedded Systems Verification

AU - Mader, Angelika H.

AU - Wupper, Hanno

AU - Boon, Mieke

AU - Marincic, J.

N1 - submitted

PY - 2008/5/24

Y1 - 2008/5/24

N2 - During model construction a number of decisions has to be taken. Often, decisions remain implicit, which has consequences for the correct interpretation of the model, and provides a source of miscommunication between different stakeholders and domain experts. We present a taxonomy of decisions guiding the modelling process and helping to distinguish, document and order the choices and assumptions involved. We focus on modelling of embedded systems, the purpose of the models we construct is formal verification. As a consequence we model both, control software and the controlled environment. Moreover, we aim at models in a formal representation, suitable for, e.g., model checking. The explicitness of modelling decisions allows to assess the quality of models and to clarify how meaningful verification results are. The taxonomy is a result of conceptual analysis and not bound to certain languages, methods, and tools. It can be used as complement for existing modelling methods.

AB - During model construction a number of decisions has to be taken. Often, decisions remain implicit, which has consequences for the correct interpretation of the model, and provides a source of miscommunication between different stakeholders and domain experts. We present a taxonomy of decisions guiding the modelling process and helping to distinguish, document and order the choices and assumptions involved. We focus on modelling of embedded systems, the purpose of the models we construct is formal verification. As a consequence we model both, control software and the controlled environment. Moreover, we aim at models in a formal representation, suitable for, e.g., model checking. The explicitness of modelling decisions allows to assess the quality of models and to clarify how meaningful verification results are. The taxonomy is a result of conceptual analysis and not bound to certain languages, methods, and tools. It can be used as complement for existing modelling methods.

KW - EWI-12763

KW - IR-64770

KW - METIS-256116

M3 - Report

T3 - CTIT Technical Report Series

BT - A Taxonomy of Modelling Decisions for Embedded Systems Verification

PB - Distributed and Embedded Security (DIES)

CY - Enschede

ER -

Mader AH, Wupper H, Boon M, Marincic J. A Taxonomy of Modelling Decisions for Embedded Systems Verification. Enschede: Distributed and Embedded Security (DIES), 2008. 14 p. (CTIT Technical Report Series; 08-37).