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.

Additional Services

Author: Jan Olaf Blech, Ina Schaefer, Arnd Poetzsch-Heffter urn:nbn:de:hbz:386-kluedo-15053 Interner Bericht des Fachbereich Informatik (361) Report English 2007 2007 Technische Universität Kaiserslautern 2007/08/31 Isabelle/HOL; Model Checking ; System Abstractions ; Translation Validation Fachbereich Informatik 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011

$Rev: 13581$