Capturing Assumptions while Designing a Verification Model for Embedded Systems

Share/Save/Bookmark

Marincic, J. and Mader, A.H. and Wieringa, R.J. (2007) Capturing Assumptions while Designing a Verification Model for Embedded Systems. [Report]

[img]
Preview
PDF
243Kb
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.
Item Type:Report
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/66986
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 242052