This paper addresses the process of modelling embedded sys-
tems for formal verification. We propose a modelling process built on
non-monotonic refinement and a number of guidelines. The outcome of
the modelling process is a model, together with a correctness argument
that justifies our modelling decisions. After explaining the method, we
demonstrate it on a small example.
|Name||CTIT Technical Report Series|
|Publisher||Centre for Telematics and Information Technology, University of Twente|