Motivation
Während elektronische Schaltungen noch bis vor einigen Jahren vornehmlich in Rechenanlagen Verwendung fanden, werden sie - als zentraler Bestandteil so genannter eingebetteter Systeme - zunehmend ein Teil unserer täglichen Umgebung und finden in vielen sicherheitskritischen Bereichen Anwendung. Bei Verkehrssystemen, die Steuerungs- und Assistenzfunktion in Bahnen/Stellwerken, Flugzeugen und Automobilen übernehmen, ist die Abhängigkeit von Elektronik und zugehöriger Software bereits so groß, dass diese beispielsweise im Automobilbereich bei steigender Tendenz bis zu 40% der Kosten verursachen. Hinzu kommt, dass immer mehr sicherheitsrelevante Komponenten, wie z.B. Weichen, Triebwerke oder Bremsen, elektronisch unterstützt bzw. gesteuert werden.

Daher werden immer höhere Anforderungen an die Vertrauenswürdigkeit und Effizienz der Verfahren gestellt, die die Korrektheit von Schaltungen, Software und eingebetteten Gesamtsystemen gewährleisten sollen. In den vergangenen Jahren wurden große Fortschritte durch den Einsatz moderner Verifikationsansätze erreicht. Grundlage der Verfahren ist die formale Spezifikation und der Test bis hin zum formalen Beweis der Korrektheit. Dies wird motiviert durch die Tatsache, dass eine reine Simulation keine ausreichende Überdeckung der Funktionalität gewährleisten kann.

Weiterhin ist ein wesentlicher Aspekt bei der Konstruktion der Systeme die Systemintegration, die neben der Hardware auch die Software umfasst. Nur durch eine vereinheitlichte Sichtweise ist es möglich, diese komplexen Systeme auch in Zukunft erfolgreich entwickeln und einsetzen zu können. Diese integrierten Systeme werden häufig als eingebettete Systeme (engl: embedded systems) bezeichnet.