Verifikation von eingebetteten Systemen

点击翻译按钮获取中文摘要

Eingebettete Systeme müssen in der Lage sein, jederzeit auf Aktionen ihrer Umgebung mit entsprechenden Reaktionen zu antworten. Daher spricht man von reaktiven Systemen, wobei angenommen wird, daß solche Systeme oft unter harten Echtzeitanforderungen arbeiten müssen. Aus diesem Grund werden diese Systeme in der Regel durch parallele Prozesse implementiert, die oft zusätzlich noch durch speziell entworfene Hardware beschleunigt werden. Derzeit existieren weder einheitliche Beschreibungssprachen noch Verifikationsverfahren, mit denen der Entwurf derartiger Systeme hinreichend effizient unterstützt werden kann. In dem hier beantragten Forschungsvorhaben wurde daher in der vorangegangenen Förderperiode zunächst eine synchrone Sprache PURR zur Modellierung reaktiver Systeme definiert, zu der in der nun folgenden Förderperiode geeignete Verifikationsmethoden entwickelt werden sollen. Die zu entwickelnden Methoden sollen in Fallstudien im Rahmen von Kooperationen mit anderen Projekten validiert werden.