Formal Geist freut sich, Sie auf der folgenden Veranstaltung mit
Professor Jan Peleska und Professor Wen-Ling Huang laden:

n

n

SysML, formale Semantik und ihre Anwendung beim modellbasierten Testen

Monday, May 27^th, 201310:00-12:30

University of Düsseldorf

Room 25.12.2.55

Vortrag wird in deutscher Sprache abgehalten werden.

Nicht-Mitglieder des Lehrkörpers, Anmeldung erbeten bei info@formalmind.com

Abstract: Die von der OMG publizierten Spezifikationen von UML und SysML sind in den letzten Jahren kontinuierlich verbessert worden, so dass sie heute eine ausreichende Grundlage für die semantische Interpretation liefern: In Bezug auf die formale Syntax und statische Semantik wurde unter Zuhilfenahme der Object Constraint Language OCL ein erheblicher Grad an Präzision erreicht – auch wenn man immer noch an einigen Stellen mit fehlerhaften OCL Ausdrücken oder Widersprüchen zwischen textueller und formaler Beschreibung rechnen muss. In Bezug auf die Verhaltenssemantik liegen nur natürlich-sprachliche Regelungen vor. Diese sind jedoch inzwischen ausreichend klar, so dass sie sich in eine formale Beschreibung umsetzen lassen. Nur bei sogenannten Semantic Variation Points werden unterschiedliche Interpretationen zugelassen, die projekt- oder werkzeugspezifisch festgelegt werden müssen.

In diesem Vortrag demonstrieren wir die systematische Konstruktion einer formalen Echtzeit-Semantik für SysML Spezifikationen, in denen Verhalten durch Block-Operationen und Zustandsmaschinen beschrieben wird. Diese Konstruktion führt zu einer Transitionsrelation, welche diskrete Schritte in Nullzeit mit Verzögerungen kombiniert, so dass eine Echtzeit-Semantik entsteht, die wahlweise nach dem Dense Time oder Discrete Time Paradigma mit synchronem oder verschränktem (interleaving semantics) Verhalten ausgeprägt ist. Wir demonstrieren die praktische Anwendung dieser Konstruktion im modellbasierten Testen und beim Bounded Model Checking anhand des Werkzeugs RT-Tester, welches von Verified Systems International in Kooperation mit der Universität Bremen entwickelt wurde.