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.

Download full text files

Export metadata

Additional Services

Search Google Scholar
Author:Jan Olaf Blech, Ina Schaefer, Arnd Poetzsch-Heffter
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