Model Checking von Abstract State Machines mit [mc]square
Motivation
Abstract State Machines (ASM) sind eine formale Methode zum Entwurf und zur Analyse eines Systems auf hohem Abstraktionslevel. Ziel dieser Diplomarbeit ist die Einbettung des open-source-Simulators CoreASM in [mc]square. Dazu müssen die Zustände des Simulators serialisiert und nichtdeterministische Eigenschaften wie z. B. das Scheduling des Simulators determinisiert werden. Wichtig ist dabei die Kompatibilität auch zu zukünftigen Versionen von CoreASM zu berücksichtigen
Aufgabenstellung
Unser Model-Checking Tool [mc]square wird im Moment zur Verifikation von Assembler Quelltexten für bestimmte Mikrocontroller verwendet (z.B. ATMEL ATmega16 und Infineon XC 167). Das Verfahren, welches dabei zum Einsatz kommt, lässt sich auf Grund der Architektur des Werkzeugs auch gut auf ASMs übertragen. Inwiefern auch die Optimierungen, welche in der Verifikation der Assemblerprogramme verwendet werden, angewandt werden können, soll in dieser Diplomarbeit gezeigt werden.
Vorkenntnisse
Zur Implementierung, die im Rahmen der Arbeit erforderlich ist, sind gute Javakentnisse nötig.
Betreuer
- Dr.-Ing. Daniel Klünder