Auch als elektronisches Dokument vorh ; Oldenburg, Univ., Diss., 2007
HochschulschriftHybrides SystemProgrammverifikationVerifikationHoare-LogikKontinuierliches SystemDiskretes System
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 große 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 große Klassen von ungültigen Gegenbeispielen für nachfolgende Iterationen ausschließt, 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.>
