Rodin-Handbuch jetzt in gedruckter Form erhältlich

Vor einiger Zeit unterstützten wir das EU-Projekt Deploy und produzierten eine Handbuch für die Rodin-Plattform, ein Werkzeug zur Erstellung formaler Spezifikationen mit der Event-B-Methode. Dieses Buch war ein großer Erfolg, aber nur elektronisch verfügbar (kostenlos, unter einer Creative Commons Lizenz).

Aufgrund der hohen Nachfrage, insbesondere von Universitäten, die formale Methoden lehren, haben wir uns entschlossen, eine gedruckte Version des Handbuchs zu erstellen. Wir freuen uns, die Verfügbarkeit des Rodin Handbuchs in gedruckter Form bekannt zu geben – Sie können kaufen Sie Ihr Exemplar bei Amazon – natürlich, Die elektronische Version wird immer kostenlos sein.

Was ist Rodin und warum sollte es mir wichtig sein?

Rodin ist ein Open-Source-Softwarewerkzeug zum Schreiben Formale Spezifikationen.Eine formale Spezifikation nutzt eine formale Notation anstelle natürlicher Sprache, um zu beschreiben, was gebaut werden muss. Zunächst einmal, macht dies die Sache schwieriger: Benutzer müssen lernen, die Sprache zu lesen und zu schreiben. Aber sobald diese Hürde überwunden ist, ist das Ergebnis mächtiger als Text: Eine formale Spezifikation ermöglicht es Ihnen:

• Überprüfen Sie automatisch, ob Ihre Spezifikation konsistent ist. Widersprüche werden zuverlässig erkannt.
• Beschreiben Sie Ihr System auf einer hohen, abstrakten Ebene und verwenden Sie Verfeinerung eine konkrete Implementierung zu erstellen
• Überprüfen Sie automatisch, ob Ihre Implementierung mit Ihrer Spezifikation übereinstimmt.
• Animieren oder visualisieren Sie Ihre Spezifikation, auch wenn diese abstrakt ist.
• Generieren Sie Tests aus Ihren Modellen oder sogar ausführbaren Code.

Darüber hinaus empfehlen oder fordern viele Standards für die Entwicklung sicherheitskritischer Systeme, wie die IEC 61508 oder die ISO 26262, die Verwendung von formalen Methoden., wie wir zuvor berichtet haben.

Event-B im Vergleich zu anderen Modellierungssprachen

Event-B ist die formale Sprache, die von Rodin unterstützt wird. Es ist eine textuelle Sprache und kann sehr einschüchternd sein. Die meisten Menschen finden semi-formale Sprachen wie UML oder SysML zugänglicher – aber diese Sprachen sind auch weniger mächtig. Event-B zeigt sehr gut, wozu formale Sprachen fähig sind, vom Theorembeweis bis zur Codegenerierung. Daher empfehlen wir Event-B und Rodin, um formale Methoden zu erlernen. 

Rodin nutzt auch das Eclipse-Ökosystem. Unter vielen anderen Erweiterungen haben wir eine Integration mit ProR für Anforderungstransparenz.

Crashkurs in Formalen Methoden

Wenn Sie formale Methoden verstehen müssen, ist das Rodin-Handbuch ein guter Ausgangspunkt:

• Das Buch erfordert keine Vorkenntnisse über formale Methoden, nur etwas grundlegende Mathematik.
• Es enthält eine detaillierte Anleitung, die Sie Schritt für Schritt durch den Aufbau Ihrer ersten formalen Modelle führt.
• Durch die Befolgung des Tutorials und die Nutzung des kostenlosen Rodin-Tools erhalten Sie praktische Erfahrung mit formalen Methoden.
• Das Tutorial kann in wenigen Tagen abgeschlossen werden, danach sollten Sie ein solides Verständnis für das Thema haben.
• Die umfangreichen Referenz- und FAQ-Abschnitte des Buches decken alle Aspekte ab, die Ihnen beim Verfassen Ihrer eigenen formalen Spezifikationen begegnen können.
• Wenn Sie sich entscheiden, andere formale oder semi-formale Modellierungssprachen zu evaluieren, bietet Ihnen Event-B eine solide Messlatte.

Schulung verfügbar

Schließlich bieten wir professionelle Schulungen zu Formalen Methoden im Allgemeinen sowie zu Rodin und Event-B im Besonderen an. Bitte Kontaktieren Sie uns falls das für Sie von Interesse ist.