Ich bin Informatikstudent an der RWTH-Aachen und schreibe gerade meine Diplomarbeit am Lehrstuhl Informatik 11.
In meiner Diplomarbeit habe ich unseren Model-Checker [mc]square für SPSen erweitert. Das SPS Modell ist eine "konventionelle SPS" mit einer Konfiguration, einer Ressource und einem zyklischen Task, der ein Programm steuert. Da [mc]square für Mikrocontroller auf Assemblercode arbeitet, haben wir wegen der Ähnlichkeit die Sprache Anweisungsliste gewählt.
Ich habe mir für die Verwendung von [mc]square folgendes ausgedacht:
1) der Programmierer schreibt sein Programm in CoDeSys und prüft auf syntaktische Korrektheit
2) dann exportiert er sein Programm, wobei die Exportdateien in einem Ordner liegen sollen und jede Programmorganisationseinheit in einer eigenen Datei liegt
3) in [mc]square wählt der Programmierer das Programm PLC_PRG aus und alle abhängigen Dateien lädt [mc]square automatisch aus dem Ordner nach
4) Überprüfung des Programms mit Hilfe des CTL-Model-Checkers
Der Implementierungsteil der Diplomarbeit ist fast fertig. (Noch Rückintegration und Gui polieren ) Ich bin auf der Suche nach Programmen in AWL. Wie bei jedem Model-Checker kämpfen wir dabei mit dem Problem der Zustandsraumexplosion. Ich habe mich bei der Lösung des Problems auf SPS Eingänge konzentiert. Dazu habe ich einen abstrakten Simulator implementiert, der Eingangskombinationen für BYTE-, WORD- und DWORD-Eingänge zusammenfasst.
Deshalb bin ich besonders an Programmen oder auch Einsatzgebiete von SPSen interessiert, die solche Eingänge benutzen.
Vielleicht könnt ihr mir weiterhelfen.
Gruß Ovigomy
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Hallo zusammen!
Ich bin Informatikstudent an der RWTH-Aachen und schreibe gerade meine Diplomarbeit am Lehrstuhl Informatik 11.
In meiner Diplomarbeit habe ich unseren Model-Checker [mc]square für SPSen erweitert. Das SPS Modell ist eine "konventionelle SPS" mit einer Konfiguration, einer Ressource und einem zyklischen Task, der ein Programm steuert. Da [mc]square für Mikrocontroller auf Assemblercode arbeitet, haben wir wegen der Ähnlichkeit die Sprache Anweisungsliste gewählt.
Ich habe mir für die Verwendung von [mc]square folgendes ausgedacht:
1) der Programmierer schreibt sein Programm in CoDeSys und prüft auf syntaktische Korrektheit
2) dann exportiert er sein Programm, wobei die Exportdateien in einem Ordner liegen sollen und jede Programmorganisationseinheit in einer eigenen Datei liegt
3) in [mc]square wählt der Programmierer das Programm PLC_PRG aus und alle abhängigen Dateien lädt [mc]square automatisch aus dem Ordner nach
4) Überprüfung des Programms mit Hilfe des CTL-Model-Checkers
Der Implementierungsteil der Diplomarbeit ist fast fertig. (Noch Rückintegration und Gui polieren ) Ich bin auf der Suche nach Programmen in AWL. Wie bei jedem Model-Checker kämpfen wir dabei mit dem Problem der Zustandsraumexplosion. Ich habe mich bei der Lösung des Problems auf SPS Eingänge konzentiert. Dazu habe ich einen abstrakten Simulator implementiert, der Eingangskombinationen für BYTE-, WORD- und DWORD-Eingänge zusammenfasst.
Deshalb bin ich besonders an Programmen oder auch Einsatzgebiete von SPSen interessiert, die solche Eingänge benutzen.
Vielleicht könnt ihr mir weiterhelfen.
Gruß Ovigomy