Validation of Embedded System Verification Models

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    3 Citations (Scopus)

    Abstract

    The result of a model-based requirements verification shows that the model of a system satisfies (or not) formalised system requirements. The verification result is correct only if the model represents the system adequately. No matter what modelling technique we use, what precedes the model construction are non-formal activities. During these activities the modeller has to learn how the system works, what the requirements are, and to decide what is relevant to model and how to do it. Due to a partly non-formal nature of modelling steps, we do not have a formal proof that the model represents the system adequately. The most we can do is to increase the confidence in the model. In this paper we explore non-formal model validation steps while designing a formal model. On the example of a Uppaal performance model we designed in a company that produces printers, we will show what validation steps were necessary to increase the stakeholders' confidence in the model. Based on this case study, we propose more general, but non-formal model validation steps, that can structure model validation. The steps we propose deal with the same design elements and issues present in other model-based verification activities, therefore can accompany them as well.
    Original languageUndefined
    Title of host publicationProceedings of Model-Driven Requirements Engineering Workshop (MoDRE)
    Place of PublicationUSA
    PublisherIEEE Computer Society
    Pages48-54
    Number of pages7
    ISBN (Print)978-1-4577-0957-9
    DOIs
    Publication statusPublished - Aug 2011

    Publication series

    Name
    PublisherIEEE Computer Society

    Keywords

    • IR-78396
    • METIS-279677
    • EWI-20743
    • SCS-Services
    • CR-D.2.1
    • CR-I.5.2
    • CR-I.6.4
    • CR-D.2.4
    • CR-D.2
    • CR-I.2.8

    Cite this

    Marincic, J., Mader, A. H., & Wieringa, R. J. (2011). Validation of Embedded System Verification Models. In Proceedings of Model-Driven Requirements Engineering Workshop (MoDRE) (pp. 48-54). USA: IEEE Computer Society. https://doi.org/10.1109/MoDRE.2011.6045366
    Marincic, J. ; Mader, Angelika H. ; Wieringa, Roelf J. / Validation of Embedded System Verification Models. Proceedings of Model-Driven Requirements Engineering Workshop (MoDRE). USA : IEEE Computer Society, 2011. pp. 48-54
    @inproceedings{59f1aa9baeeb407abdad2d80f9c65d7d,
    title = "Validation of Embedded System Verification Models",
    abstract = "The result of a model-based requirements verification shows that the model of a system satisfies (or not) formalised system requirements. The verification result is correct only if the model represents the system adequately. No matter what modelling technique we use, what precedes the model construction are non-formal activities. During these activities the modeller has to learn how the system works, what the requirements are, and to decide what is relevant to model and how to do it. Due to a partly non-formal nature of modelling steps, we do not have a formal proof that the model represents the system adequately. The most we can do is to increase the confidence in the model. In this paper we explore non-formal model validation steps while designing a formal model. On the example of a Uppaal performance model we designed in a company that produces printers, we will show what validation steps were necessary to increase the stakeholders' confidence in the model. Based on this case study, we propose more general, but non-formal model validation steps, that can structure model validation. The steps we propose deal with the same design elements and issues present in other model-based verification activities, therefore can accompany them as well.",
    keywords = "IR-78396, METIS-279677, EWI-20743, SCS-Services, CR-D.2.1, CR-I.5.2, CR-I.6.4, CR-D.2.4, CR-D.2, CR-I.2.8",
    author = "J. Marincic and Mader, {Angelika H.} and Wieringa, {Roelf J.}",
    note = "Conceptual analysis of modelling; case study; formal models; non-formal, design steps",
    year = "2011",
    month = "8",
    doi = "10.1109/MoDRE.2011.6045366",
    language = "Undefined",
    isbn = "978-1-4577-0957-9",
    publisher = "IEEE Computer Society",
    pages = "48--54",
    booktitle = "Proceedings of Model-Driven Requirements Engineering Workshop (MoDRE)",
    address = "United States",

    }

    Marincic, J, Mader, AH & Wieringa, RJ 2011, Validation of Embedded System Verification Models. in Proceedings of Model-Driven Requirements Engineering Workshop (MoDRE). IEEE Computer Society, USA, pp. 48-54. https://doi.org/10.1109/MoDRE.2011.6045366

    Validation of Embedded System Verification Models. / Marincic, J.; Mader, Angelika H.; Wieringa, Roelf J.

    Proceedings of Model-Driven Requirements Engineering Workshop (MoDRE). USA : IEEE Computer Society, 2011. p. 48-54.

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    TY - GEN

    T1 - Validation of Embedded System Verification Models

    AU - Marincic, J.

    AU - Mader, Angelika H.

    AU - Wieringa, Roelf J.

    N1 - Conceptual analysis of modelling; case study; formal models; non-formal, design steps

    PY - 2011/8

    Y1 - 2011/8

    N2 - The result of a model-based requirements verification shows that the model of a system satisfies (or not) formalised system requirements. The verification result is correct only if the model represents the system adequately. No matter what modelling technique we use, what precedes the model construction are non-formal activities. During these activities the modeller has to learn how the system works, what the requirements are, and to decide what is relevant to model and how to do it. Due to a partly non-formal nature of modelling steps, we do not have a formal proof that the model represents the system adequately. The most we can do is to increase the confidence in the model. In this paper we explore non-formal model validation steps while designing a formal model. On the example of a Uppaal performance model we designed in a company that produces printers, we will show what validation steps were necessary to increase the stakeholders' confidence in the model. Based on this case study, we propose more general, but non-formal model validation steps, that can structure model validation. The steps we propose deal with the same design elements and issues present in other model-based verification activities, therefore can accompany them as well.

    AB - The result of a model-based requirements verification shows that the model of a system satisfies (or not) formalised system requirements. The verification result is correct only if the model represents the system adequately. No matter what modelling technique we use, what precedes the model construction are non-formal activities. During these activities the modeller has to learn how the system works, what the requirements are, and to decide what is relevant to model and how to do it. Due to a partly non-formal nature of modelling steps, we do not have a formal proof that the model represents the system adequately. The most we can do is to increase the confidence in the model. In this paper we explore non-formal model validation steps while designing a formal model. On the example of a Uppaal performance model we designed in a company that produces printers, we will show what validation steps were necessary to increase the stakeholders' confidence in the model. Based on this case study, we propose more general, but non-formal model validation steps, that can structure model validation. The steps we propose deal with the same design elements and issues present in other model-based verification activities, therefore can accompany them as well.

    KW - IR-78396

    KW - METIS-279677

    KW - EWI-20743

    KW - SCS-Services

    KW - CR-D.2.1

    KW - CR-I.5.2

    KW - CR-I.6.4

    KW - CR-D.2.4

    KW - CR-D.2

    KW - CR-I.2.8

    U2 - 10.1109/MoDRE.2011.6045366

    DO - 10.1109/MoDRE.2011.6045366

    M3 - Conference contribution

    SN - 978-1-4577-0957-9

    SP - 48

    EP - 54

    BT - Proceedings of Model-Driven Requirements Engineering Workshop (MoDRE)

    PB - IEEE Computer Society

    CY - USA

    ER -

    Marincic J, Mader AH, Wieringa RJ. Validation of Embedded System Verification Models. In Proceedings of Model-Driven Requirements Engineering Workshop (MoDRE). USA: IEEE Computer Society. 2011. p. 48-54 https://doi.org/10.1109/MoDRE.2011.6045366