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.

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Jan Olaf Blech, Ina Schaefer, Arnd Poetzsch-Heffter
URN (permanent link):urn:nbn:de:hbz:386-kluedo-15053
Serie (Series number):Interner Bericht des Fachbereich Informatik (361)
Document Type:Report
Language of publication:English
Year of Completion:2007
Year of Publication:2007
Publishing Institute:Technische Universität Kaiserslautern
Tag:Isabelle/HOL; Model Checking ; System Abstractions ; Translation Validation
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:004 Datenverarbeitung; Informatik

$Rev: 12793 $