Obtaining Formal Models through Non-Monotonic Refinement

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

    Research output: Book/ReportReportProfessional

    81 Downloads (Pure)


    When designing a model for formal verification, we want to be certain that what we proved about the model also holds for the system we modelled. This raises the question of whether our model represents the system, and what makes us confident about this. By performing so called, non-monotonic refinement in the modelling process, we make the steps and decisions explicit. This helps us to (1) increase the confidence that the model represents the system, (2) structure and organize the communication with domain experts and the problem owner, and (3) identify rational steps made while modelling. We focus on embedded control systems.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages14
    Publication statusPublished - Apr 2007

    Publication series

    NameCTIT Technical Report Series
    PublisherCentre for Telematics and Information Technology, University of Twente
    ISSN (Print)1381-3625


    • IR-67116
    • METIS-241629
    • CR-I.6.4
    • EWI-9879
    • SCS-Services
    • Model construction

    Cite this