Der SMV (Symbolic Model Verifier) ist ein Werkzeug zur Modellprüfung (engl. Model Checking). Dieser Model Checker prüft endliche Zustandsautomaten (engl. Finite State Machines) mit der temporalen Logik CTL. == Technologie == Die Eingabesprache erlaubt es, einen Automaten synchron, asynchron, detailliert oder abstrakt zu beschreiben. In der Sprac...