Effiziente Quelle zur Bestimmung einer Unausführbarkeit in Timed Automata-Spuren

摘要

Ein Verfahren zum Verifizieren der Leistungsfähigkeit eines Echtzeitsystems wird als ein Timed Automaton modelliert. Ein abstraktes Modell des Systems wird gegenüber einer anfänglich linear temporären Logikspezifikation geprüft. Wenn ein Weg zu einem unerwünschten Zustand gefunden ist, wird das Gegenbeispiel als gültig oder ungültig unter Verwendung einer negativen Zykluserfassung gesetzt. Wenn ein negativer Zyklus erfasst ist, wird eine Optimierung durchgeführt, um ein minimal unausführbares Fragment in dem negativen Zyklus zu bestimmen. Die Spezifikation wird dann verfeinert, um die Verwendung des minimal unausführbaren Fragmentes zu eliminieren und das abstrakte Modell wird dann gegenüber der verfeinerten Spezifikation geprüft.