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.
|Name||CTIT Technical Report Series|
|Publisher||Centre for Telematics and Information Technology, University of Twente|
- Model construction