Als einfaches Beispiel sei hier eine Ampelsteuerung spezifiziert, also ein System, das im Wesentlichen lediglich ein Steuerwerk darstellt, das einen Kontrollfluss realisiert. Es beschreibt die Steuerung einer Hauptstraßen/Nebenstraßen-Ampel mit zusätzlicher Fußgänger-Ampel für die Hauptstraße und soll die in der Abbildung dargestellten Eigenschaften aufweisen.
Neben diesen globalen Eigenschaften werden der detaillierte Aufbau der Ampelsteuerung und die Funktionalität mit verschiedenen formalen Methoden beschrieben.