Obtaining Formal Models through Non-Monotonic Refinement

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

Obtaining Formal Models through Non-Monotonic Refinement

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

Research output: Book/Report › Report › Professional

91 Downloads (Pure)

Abstract

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 language	Undefined
Place of Publication	Enschede
Publisher	Centre for Telematics and Information Technology (CTIT)
Number of pages	14
Publication status	Published - Apr 2007

Publication series

Name	CTIT Technical Report Series
Publisher	Centre for Telematics and Information Technology, University of Twente
No.	P2773/TR-CTIT-07-33
ISSN (Print)	1381-3625

Keywords

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

Access to Document

Cite this

@book{5467e65585b842a384da9cf967f67737,

title = "Obtaining Formal Models through Non-Monotonic Refinement",

abstract = "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.",

keywords = "IR-67116, METIS-241629, CR-I.6.4, EWI-9879, SCS-Services, Model construction",

author = "J. Marincic and H. Wupper and Mader, {Angelika H.} and Wieringa, {Roelf J.}",

year = "2007",

month = apr,

language = "Undefined",

series = "CTIT Technical Report Series",

publisher = "Centre for Telematics and Information Technology (CTIT)",

number = "P2773/TR-CTIT-07-33",

address = "Netherlands",

}

TY - BOOK

T1 - Obtaining Formal Models through Non-Monotonic Refinement

AU - Marincic, J.

AU - Wupper, H.

AU - Mader, Angelika H.

AU - Wieringa, Roelf J.

PY - 2007/4

Y1 - 2007/4

N2 - 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.

AB - 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.

KW - IR-67116

KW - METIS-241629

KW - CR-I.6.4

KW - EWI-9879

KW - SCS-Services

KW - Model construction

M3 - Report

T3 - CTIT Technical Report Series

BT - Obtaining Formal Models through Non-Monotonic Refinement

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -