publication . Doctoral thesis . 2013

Three-valued abstraction and heuristic-guided refinement for verifying concurrent systems

Timm, Nils;
Open Access English
  • Published: 01 Jan 2013
  • Country: Germany
Abstract
Diese Arbeit präsentiert ein abstraktionsverfeinerungsbasiertes Verifikationsframework für nebenläufige Systeme. Zur Abstraktion verwenden wir eine Kombination aus Prädikatabstraktion und Spotlightabstraktion. Dadurch werden zwei der Hauptursachen der Zustandskomplexität bei der Verifikation nebenläufiger Systeme angegangen. Eine weitere Besonderheit des Verfahrens ist der Einsatz einer 3-wertigen abstrakten Domäne. Eigenschaften in Systemmodellen können die Werte wahr, falsch und unbekannt annehmen, wodurch sich der abstraktionsbedingte Informationsverlust modellieren lässt: Alle wahr- und falsch-Resultate die sich bei der Verifikation ergeben, lassen sich auf ...
Related Organizations
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue