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.

Volltext Dateien herunterladen

Metadaten exportieren

  • Export nach Bibtex
  • Export nach RIS

Weitere Dienste

Teilen auf Twitter Suche bei Google Scholar
Metadaten
Verfasserangaben:Jan Olaf Blech, Ina Schaefer, Arnd Poetzsch-Heffter
URN (Permalink):urn:nbn:de:hbz:386-kluedo-15053
Schriftenreihe (Bandnummer):Interner Bericht des Fachbereich Informatik (361)
Dokumentart:Bericht
Sprache der Veröffentlichung:Englisch
Jahr der Fertigstellung:2007
Jahr der Veröffentlichung:2007
Veröffentlichende Institution:Technische Universität Kaiserslautern
Datum der Publikation (Server):31.08.2007
Freies Schlagwort / Tag:Isabelle/HOL; Model Checking ; System Abstractions ; Translation Validation
Fachbereiche / Organisatorische Einheiten:Fachbereich Informatik
DDC-Sachgruppen:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Lizenz (Deutsch):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011

$Rev: 13581 $