Validation of Embedded System Verification Models

J. Marincic, Angelika H. Mader, Roelf J. Wieringa

    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