Abstract

Computer-aided verification of embedded systems hinges on the availability of good verification models of the systems at hand. Such models must be much simpler than full design models or specifications to be of practical value, because of the unavoidable combinatorial complexities in the verification of any non-trivial system. Good verification models, therefore, are lean and mean, and cannot be obtained easily or generated automatically. Current research, however, seems to take the construction of verification models more or less for granted, although their development typically requires a coordinated integration of the experience, intuition and creativity of verification and domain experts. We argue that there is a great need for systematic methods for the construction of verification models to move on, and leave the current stage that can be characterised as that of model hacking. The ad-hoc construction of verification models obscures the relationship between models and the systems that they represent, and undermines the reliability and relevance of the verification results that are obtained. We propose some ingredients for a solution to this problem.
LanguageUndefined
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
StatePublished - Jan 2004

Publication series

NameTR-CTIT
PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
No.04-03

Keywords

  • METIS-220393
  • EWI-795
  • IR-48688

Cite this

Brinksma, H., & Mader, A. H. (2004). On Verification Modelling of Embedded Systems. (TR-CTIT; No. 04-03). Enschede: Centre for Telematics and Information Technology (CTIT).
Brinksma, Hendrik ; Mader, Angelika H./ On Verification Modelling of Embedded Systems. Enschede : Centre for Telematics and Information Technology (CTIT), 2004. (TR-CTIT; 04-03).
@book{18e405baf3ed49a19ae58d228635b21c,
title = "On Verification Modelling of Embedded Systems",
abstract = "Computer-aided verification of embedded systems hinges on the availability of good verification models of the systems at hand. Such models must be much simpler than full design models or specifications to be of practical value, because of the unavoidable combinatorial complexities in the verification of any non-trivial system. Good verification models, therefore, are lean and mean, and cannot be obtained easily or generated automatically. Current research, however, seems to take the construction of verification models more or less for granted, although their development typically requires a coordinated integration of the experience, intuition and creativity of verification and domain experts. We argue that there is a great need for systematic methods for the construction of verification models to move on, and leave the current stage that can be characterised as that of model hacking. The ad-hoc construction of verification models obscures the relationship between models and the systems that they represent, and undermines the reliability and relevance of the verification results that are obtained. We propose some ingredients for a solution to this problem.",
keywords = "METIS-220393, EWI-795, IR-48688",
author = "Hendrik Brinksma and Mader, {Angelika H.}",
note = "Imported from DIES",
year = "2004",
month = "1",
language = "Undefined",
series = "TR-CTIT",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "04-03",
address = "Netherlands",

}

Brinksma, H & Mader, AH 2004, On Verification Modelling of Embedded Systems. TR-CTIT, no. 04-03, Centre for Telematics and Information Technology (CTIT), Enschede.

On Verification Modelling of Embedded Systems. / Brinksma, Hendrik; Mader, Angelika H.

Enschede : Centre for Telematics and Information Technology (CTIT), 2004. (TR-CTIT; No. 04-03).

Research output: Book/ReportReport

TY - BOOK

T1 - On Verification Modelling of Embedded Systems

AU - Brinksma,Hendrik

AU - Mader,Angelika H.

N1 - Imported from DIES

PY - 2004/1

Y1 - 2004/1

N2 - Computer-aided verification of embedded systems hinges on the availability of good verification models of the systems at hand. Such models must be much simpler than full design models or specifications to be of practical value, because of the unavoidable combinatorial complexities in the verification of any non-trivial system. Good verification models, therefore, are lean and mean, and cannot be obtained easily or generated automatically. Current research, however, seems to take the construction of verification models more or less for granted, although their development typically requires a coordinated integration of the experience, intuition and creativity of verification and domain experts. We argue that there is a great need for systematic methods for the construction of verification models to move on, and leave the current stage that can be characterised as that of model hacking. The ad-hoc construction of verification models obscures the relationship between models and the systems that they represent, and undermines the reliability and relevance of the verification results that are obtained. We propose some ingredients for a solution to this problem.

AB - Computer-aided verification of embedded systems hinges on the availability of good verification models of the systems at hand. Such models must be much simpler than full design models or specifications to be of practical value, because of the unavoidable combinatorial complexities in the verification of any non-trivial system. Good verification models, therefore, are lean and mean, and cannot be obtained easily or generated automatically. Current research, however, seems to take the construction of verification models more or less for granted, although their development typically requires a coordinated integration of the experience, intuition and creativity of verification and domain experts. We argue that there is a great need for systematic methods for the construction of verification models to move on, and leave the current stage that can be characterised as that of model hacking. The ad-hoc construction of verification models obscures the relationship between models and the systems that they represent, and undermines the reliability and relevance of the verification results that are obtained. We propose some ingredients for a solution to this problem.

KW - METIS-220393

KW - EWI-795

KW - IR-48688

M3 - Report

T3 - TR-CTIT

BT - On Verification Modelling of Embedded Systems

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Brinksma H, Mader AH. On Verification Modelling of Embedded Systems. Enschede: Centre for Telematics and Information Technology (CTIT), 2004. (TR-CTIT; 04-03).