000260314 001__ 260314
000260314 005__ 20260217173116.0
000260314 0247_ $$aG:(GEPRIS)419850228$$d419850228
000260314 035__ $$aG:(GEPRIS)419850228
000260314 040__ $$aGEPRIS$$chttp://gepris.its.kfa-juelich.de
000260314 150__ $$aKoalgebraische Modellprüfung (CoMoC2)$$y2019 -
000260314 371__ $$aProfessor Dr. Stefan Milius
000260314 371__ $$aProfessor Dr. Lutz Schröder
000260314 450__ $$aDFG project G:(GEPRIS)419850228$$wd$$y2019 -
000260314 5101_ $$0I:(DE-588b)2007744-0$$aDeutsche Forschungsgemeinschaft$$bDFG
000260314 680__ $$aEines der zentralen Verifikationsprobleme in der formalen Systementwicklung ist die Modellprüfung, d.h. zu entscheiden, ob ein gegebenes Modell eines Hard- oder Softwaresystems eine gegebene Spezifikation erfüllt, wie etwa Sicherheit, Verklemmungsfreiheit, verlässliche Anfragebeantwortung u.v.m. Eine Spezifikation kann dabei in einer geeigneten Temporallogik formuliert sein, alternativ aber etwa auch als ein weiteres System, das vom zu verifizierenden System in geeigneter Weise verfeinert werden soll. Sich anschließende algorithmische Fragestellungen reichen von der theoretischen Komplexitätsanalyse über die Entwicklung effizienter Modellprüfungsalgorithmen bis hin zu deren Implementierung in automatischen Verifikationswerkzeugen; in diesem Sinne ist die Modellprüfung eine sowohl wissenschaftlich als auch industriell etablierte Forschungsrichtung. Nachdem unter Systemmodellen ursprünglich vor allem relativ einfache relationale Strukturen verstanden wurden, haben mittlerweile ausdrucksstärkere Modelle starke Verbreitung gefunden, in denen die Systemevolution beispielsweise auch probabilistische, gewichtete oder spieltheoretische Aspekte beinhaltet. Damit einher gehen eine entsprechende Auffächerung und zahlenmäßige Vervielfachung von Formalismen zur Modellierung solcher Verhaltensweisen; bekannte Beispiele sind etwa probabilistische Temporallogiken, Game Logic und alternierende Temporallogiken. Ziel von CoMoC ist die Erforschung generischer Formalismen, Methoden und Algorithmen zur einheitlichen Behandlung von Modellprüfungsproblemen über verschiedenen Systemtypen und Systemsemantiken. Erreicht wird dies mittels eines parametrisierten Rahmenwerks: Wir verkapseln den Systemtyp gemäß dem Paradigma der universellen Koalgebra als einen Mengenfunktor, wir abstrahieren lokale Modalitäten mittels Begriffen der koalgebraischen Logik, und wir bilden auf verallgemeinerten linear-time-branching-time-Spektren angesiedelte Systemsemantiken verschiedener Granularität mittels gradierter Monaden ab. In der zweiten Projektphase CoMoC2 werden wir den Anwendungsbereich der generischen Theorie und der aus ihr erwachsenden Algorithmen und Werkzeuge erweitern, mit besonderem Augenmerk auf der Entwicklung effizienter Modellprüfungsalgorithmen für alternierungsfreie Fixpunktlogiken sowie auf Techniken der beschränkten und symbolischen Modellprüfung. Ferner werden wir generische Ausdruckssprachen zur Repräsentation koalgebraischer Systeme im Stile der Prozessalgebra weiterentwickeln, woran sich als weiterer Schwerpunkt der zweiten Projektphase eine Perspektive auf Modellprüfung als Verfeinerung von Ausdrücken anschließt, wie sie klassischerweise etwa für die Prozessalgebra CSP Verwendung findet. Insgesamt entsteht so ein hochgradig generisches Rahmenwerk - parametrisch sowohl im Systemtyp als auch in der Systemsemantik - an Modellrepräsentationssprachen und Spezifikationslogiken mit entsprechenden Modellprüfungsalgorithmen und -werkzeugen.
000260314 909CO $$ooai:juser.fz-juelich.de:926917$$pauthority$$pauthority:GRANT
000260314 909CO $$ooai:juser.fz-juelich.de:926917
000260314 980__ $$aG
000260314 980__ $$aAUTHORITY