Parallel als Ausdruck vorh ; Oldenburg, Univ., Diss., 2007
Hochschulschrift
Hybride reaktive Systeme bestehen aus diskreten Transitionssystemen und kontinuierlichen Zustandsräumen mit wechselseitig beeinflussten Zustandswechseln. Ansätze zur Verifikation solcher Systeme skalieren zumeist schlecht in Bezug auf groe diskrete Zustandsräume, wie sie oftmals in industriellen Anwendungen vorzufinden sind, da deren Fokus sich zumeist auf die Ermittlung geeigneter kontinuierlicher Zustandsapproximationen beschränkt. Zur Verifikation solcher Systeme wird ein iteratives Abstraktionsverfeinerungsverfahren vorgestellt, welches sich wiederholende Anwendungen regelungstechnischer Gesetze ausnutzt und groe Klassen von ungültigen Gegenbeispielen für nachfolgende Iterationen ausschliet, indem eine grobe Abstraktion des Modells mit einem inkrementell konstruierten omega-Automaten parallel komponiert wird. Das Verfahren skaliert mit der Gröe des diskreten Zustandsraumes und ist bei Verwendung vollständiger Model-Checker auch für die Zertifizierung geeignet. <dt.>
Hybrid reactive systems consist of discrete transition systems and continuous state spaces, where each discrete state and each transition depends on and controls the state transformation of the latter. Most approaches to verify such systems do not scale well w.r.t. large discrete state spaces as they often occur in industrial contexts since their focus is on finding suitable continuous state approximations. To verify such models an iterative abstraction refinement approach is presented, exploiting recurring regulation laws applied to the continuous state space by ruling out comprehensive classes of spurious counterexamples for subsequent iterations. With the incremental construction of an omega-automaton and its parallel composition with a course abstraction of the model, all runs containing already detected reasons of being invalid are excluded. The technique scales with the size of the discrete state space and by applying complete model-checkers, it is suitable for certification. <engl.>
