Capturing Assumptions while Designing a Verification Model for Embedded Systems

Research output: Book/ReportReportProfessional

16 Downloads (Pure)

Abstract

A formal proof of a system correctness typically holds under a number of assumptions. Leaving them implicit raises the chance of using the system in a context that violates some assumptions, which in return may invalidate the correctness proof. The goal of this paper is to show how combining informal and formal techniques in the process of modelling and formal verification helps capturing these assumptions. As we focus on embedded systems, the assumptions are about the control software, the system on which the software is running and the system’s environment. We present them as a list written in natural language that supplements the formally verified embedded system model. These two together are a better argument for system correctness than each of these given separately.
Original languageUndefined
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages33
Publication statusPublished - Jan 2007

Publication series

NameCTIT Technical Report Series
PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
No.2/TR-CTIT-07-03
ISSN (Print)1381-3625

Keywords

  • SCS-Services
  • EWI-9441
  • IR-66986
  • METIS-242052

Cite this

Marincic, J., Mader, A. H., & Wieringa, R. J. (2007). Capturing Assumptions while Designing a Verification Model for Embedded Systems. (CTIT Technical Report Series; No. 2/TR-CTIT-07-03). Enschede: Centre for Telematics and Information Technology (CTIT).
Marincic, J. ; Mader, Angelika H. ; Wieringa, Roelf J. / Capturing Assumptions while Designing a Verification Model for Embedded Systems. Enschede : Centre for Telematics and Information Technology (CTIT), 2007. 33 p. (CTIT Technical Report Series; 2/TR-CTIT-07-03).
@book{7b83a6cd7b49466c849ba50c9833c586,
title = "Capturing Assumptions while Designing a Verification Model for Embedded Systems",
abstract = "A formal proof of a system correctness typically holds under a number of assumptions. Leaving them implicit raises the chance of using the system in a context that violates some assumptions, which in return may invalidate the correctness proof. The goal of this paper is to show how combining informal and formal techniques in the process of modelling and formal verification helps capturing these assumptions. As we focus on embedded systems, the assumptions are about the control software, the system on which the software is running and the system’s environment. We present them as a list written in natural language that supplements the formally verified embedded system model. These two together are a better argument for system correctness than each of these given separately.",
keywords = "SCS-Services, EWI-9441, IR-66986, METIS-242052",
author = "J. Marincic and Mader, {Angelika H.} and Wieringa, {Roelf J.}",
year = "2007",
month = "1",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "2/TR-CTIT-07-03",
address = "Netherlands",

}

Marincic, J, Mader, AH & Wieringa, RJ 2007, Capturing Assumptions while Designing a Verification Model for Embedded Systems. CTIT Technical Report Series, no. 2/TR-CTIT-07-03, Centre for Telematics and Information Technology (CTIT), Enschede.

Capturing Assumptions while Designing a Verification Model for Embedded Systems. / Marincic, J.; Mader, Angelika H.; Wieringa, Roelf J.

Enschede : Centre for Telematics and Information Technology (CTIT), 2007. 33 p. (CTIT Technical Report Series; No. 2/TR-CTIT-07-03).

Research output: Book/ReportReportProfessional

TY - BOOK

T1 - Capturing Assumptions while Designing a Verification Model for Embedded Systems

AU - Marincic, J.

AU - Mader, Angelika H.

AU - Wieringa, Roelf J.

PY - 2007/1

Y1 - 2007/1

N2 - A formal proof of a system correctness typically holds under a number of assumptions. Leaving them implicit raises the chance of using the system in a context that violates some assumptions, which in return may invalidate the correctness proof. The goal of this paper is to show how combining informal and formal techniques in the process of modelling and formal verification helps capturing these assumptions. As we focus on embedded systems, the assumptions are about the control software, the system on which the software is running and the system’s environment. We present them as a list written in natural language that supplements the formally verified embedded system model. These two together are a better argument for system correctness than each of these given separately.

AB - A formal proof of a system correctness typically holds under a number of assumptions. Leaving them implicit raises the chance of using the system in a context that violates some assumptions, which in return may invalidate the correctness proof. The goal of this paper is to show how combining informal and formal techniques in the process of modelling and formal verification helps capturing these assumptions. As we focus on embedded systems, the assumptions are about the control software, the system on which the software is running and the system’s environment. We present them as a list written in natural language that supplements the formally verified embedded system model. These two together are a better argument for system correctness than each of these given separately.

KW - SCS-Services

KW - EWI-9441

KW - IR-66986

KW - METIS-242052

M3 - Report

T3 - CTIT Technical Report Series

BT - Capturing Assumptions while Designing a Verification Model for Embedded Systems

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Marincic J, Mader AH, Wieringa RJ. Capturing Assumptions while Designing a Verification Model for Embedded Systems. Enschede: Centre for Telematics and Information Technology (CTIT), 2007. 33 p. (CTIT Technical Report Series; 2/TR-CTIT-07-03).