- search hit 1 of 1
On Translation Validation for System Abstractions
- Abstraction is intensively used in the verification of large, complex or infinite-state systems. With abstractions getting more complex it is often difficult to see whether they are valid. However, for using abstraction in model checking it has to be ensured that properties are preserved. In this paper, we use a translation validation approach to verify property preservation of system abstractions. We formulate a correctness criterion based on simulation between concrete and abstract system for a property to be verified. For each distinct run of the abstraction procedure the correctness is verified in the theorem prover Isabelle/HOL. This technique is applied in the verification of embedded adaptive systems. This paper is an extended version a previously published work.
Author: | Jan Olaf Blech, Ina Schaefer, Arnd Poetzsch-Heffter |
---|---|
URN: | urn:nbn:de:hbz:386-kluedo-15053 |
Series (Serial Number): | Interner Bericht des Fachbereich Informatik (361) |
Document Type: | Report |
Language of publication: | English |
Year of Completion: | 2007 |
Year of first Publication: | 2007 |
Publishing Institution: | Technische Universität Kaiserslautern |
Date of the Publication (Server): | 2007/08/31 |
Tag: | Isabelle/HOL; Model Checking; System Abstractions; Translation Validation |
Faculties / Organisational entities: | Kaiserslautern - Fachbereich Informatik |
DDC-Cassification: | 0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik |
Licence (German): | Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011 |