Eclipse Requirements Modeling Framework

At the core of the B-Method is a very expressive language rooted in predicate logic, set theory, relational calculus, higher-order functions and arithmetic. At the heart of our ProB toolset is an evaluator and constraint solver for this language. We ... [More] strive for both efficiency and correctness, such that the tool can be used in a safety-critical context. The company ClearSy has posted an interesting success story about using our tool ProB for a railways reverse-engineering project, where they have made use of ProB's constraint solver in a new way. The article says "Data validation principles have been applied recently to a railways reverse-engineering project with great success. B and ProB have demonstrated again how efficient they are when used in combination. ... This problem was solved elegantly by using data validation principles: a B model representing the two graphs and their properties were elaborated, and ProB used for finding a solution." Below is the matching graph generated by the ProB constraint solver between the application binary and the high-level source code: [Less]

Formal Mind freut sich, Sie zu der folgenden Veranstaltung mitProfessor Jan Peleska und Professor Wen-Ling Huang einzuladen:   SysML, formale Semantik und ihre Anwendung beim modellbasierten Testen Montag, 27. Mai 2013, 10:00-12:30 Heinrich-Heine ... [More] Universität Düsseldorf Room 25.12.2.55 Vortrag wird in deutscher Sprache gehalten. Die Teilnahme ist kostenlos. Nicht-Mitglieder des Lehrstuhls bitte unter [email protected] anmelden   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.   [Less]