We want to share our latest insights regarding formal methods and requirements as well as the latest developments regarding our OpenSource tools, ProB and ProR. We will post new information roughly twice a month, so you won't be overwhelmed. You can either subscribe via email (below), subsribe to our RSS Feed or visit this page.
Integrating Requirements and Models
Submitted by Michael Jastram on Tue, 05/15/2012 - 14:30
While requirements engineering in itself is already useful, integrating it with other elements from the system development process can increase its value significantly. We already hinted at this in our scientific work with respect to traceability, or our thoughts of an integration with Topcased. Our latest ideas were just submitted for publication.
Picture a scenario where you work on your requirements, while at the same time buiding a model. The tool manages the data model (and in a sense, a glossary) on the fly, and even provides feedback using color highlighting:

The above screenshot has been produced using the integration of ProR with Rodin. It has been taken from a paper we just submitted outlining an approach to traceability. Rodin is a platform for the Event-B formal modeling language, but the same concepts could be used with other models, SysML, for instance.
So what value does such an integration provide? Imagine getting a set of initial requirements, and the task of creating a specification. A typical first step is to identify nouns in the requirements text as the starting point for modeling the domain. The integration allows the domain modeling to be done in Event-B. As soon as the first elements are modeled, they will appear with a squiggly red underline, alerting you to the fact that you may have missed declaring an element. Once you put square brackets around them, they turn blue to indicate that this is a modeled element.
The approach can be turned around: First mark all domain elements by surrounding them with square brackets in the requirements text. They will turn red, showing that they have not been modeled yet. Upon modeling (or renaming, if you found a synonym), they'll turn blue.
The integration already allows the creation of traces - this is shown in the right column of the screenshot. While links are generic in ProR, in our approach we use traces to document a "realizes" relationship: A linked element contributes to the realization of a requirement. It is possible to link elements from the model (e.g. an invariant), or other ProR elements (e.g. SpecObjects that are part of the specification).
As work progresses, the specification, requirements or model elements change. If there is a trace, it is marked as "suspect" with a yellow triangle to alert the user that the relationship may be suspect.
You get the idea - in the end, you can use traces to find unrealized requirements, domain objects that have not been modeled, and so forth. If you follow the approach outlined in our paper, you can even verify the consistency of the system description. (Disclosure: our integration does not support the validation of all the consistency properties that we identified - we're working on this.)
If you're interested in learning more, please don't hesitate to contact us.
Anforderungs-Templates mit ProR
Submitted by Michael Jastram on Tue, 04/24/2012 - 23:02
English-Readers: Please excuse that the following article is written in German.
Im HOOD-Blog wurde vor kurzem gezeigt, wie man mit Anforderungs-Templates besser im Projekt arbeiten kann. Seit dem letzten Release sind in ProR alle Features vorhanden, um mit solchen Templates umgehen zu können. Das Ergebnis ist im folgenden Screenshot zu sehen, und die ReqIF-Datei kann hier heruntergeladen werden.

Durch die Nutzung von ProR ergeben sich einige Abweichungen von dem ursprünglichen Template. Zum Beispiel wurde die Spalte "Typ" weggelassen und statt dessen mit unterschiedlichen SpecObject-Typen realisiert. Das bedeutet, dass "Informations"-Elemente automatisch korrekt formatiert sind, und dass IDs nur für Anforderungen vergeben werden.
ProR kann von der Eclipse RMF Webseite heruntergeladen werden.
Well Worth the Wait: New ProR Integration Release (0.2.0)
Submitted by Michael Jastram on Mon, 04/16/2012 - 13:33
The RMF team is proud to announce the i12.03 Integration build, which brings significant improvements both in the core and the ProR user interface. Please download it at the RMF download site.
In this iteration, we were focusing on the GUI and on the integration of a new core, as well as infrastructure. Most of the work was done in a 3-day coding session end of March. In addition to project leads Michael Jastram and Mark Brörkens, committer Lukas Ladenberger and students Ingo Weigelt and Said Salem participated (photo below).
So what has changed? All in all, 30 bugs were fixed since the last integration build (Bugzilla querry) Read on to learn more:

The Sprint Team: Lukas Ladenberger, Mark Brörkens, Ingo Weigelt, Said Salem, Michael Jastram
New ReqIF 1.0.1 Core
The core that Nirmal Sasidharan initially created performed well, but had a complicated architecture. Specifically, it used two EMF models under the hood, One was part of the API, the other existed for persistence only.
The new model, written by Mark Brörkens, uses only one data model, simplifying the code base significantly. And even though the original core was already fast, the new core is significantly faster. It also improves handling of tool extensions and XHTML. It will form a solid foundation for future RMF work.
There has also been a strong focus on ReqIF compliance with respect to the ReqIF 1.0.1 standard, as well as robustness when processing input files with problems. As two of the parties involved in RMF (Formal Mind and itemis) are part of the ProSTEP implementor forum, we will ensure that RMF is compatible with commercial ReqIF implementations, once they become available.
ProR Improvements (GUI)
The focus for ProR was on removing little annoyances and bugs to improve the user experience - few new features were implemented. Such improvements include:
- Visual Feedback on Drag and Drop
- No more disappearing scrollbars
- Improved ordering in the Properties View
- Improved Handling of Keyboard actions when editing in the Specification View
Many other issues have been addressed, some of which didn't affect end users directly (unhandled exceptions, redundant internal notifications, etc.). Due to some bugs in the old core, tool extensions were not persisted correctly. With the new core, this has been fixed as well.
Infrastructure at eclipse.org
Last, RMF now takes better advantage of the Eclipse infrastructure. RMF is now fully integrated into the Hudson-based Continuous Integration System. new builds are triggered every time code is checked in and is publicly accessible. Further, the system runs all unit tests (153 as of this writing, all passing).
The system creates binaries for Linux, Mac and Windows, for both 32 and 64 bit systems. The binaries are P2 enabled, meaning that additional plugins and updates can be installed through the GUI.
How to Provide Feedback
We hope that you check out the latest snapshot. Please don't hesitate to give feedback: The RMF Forum can be used for questions that may be of interest to other people as well. For development-related issues, please use the dev mailing list. And bugs can be reported directly in Bugzilla.
Best regards,
- The RMF Team
ProB Logic Calculator
Submitted by Michael Leuschel on Fri, 03/30/2012 - 15:43
A first prototype of a ProB Logic Calculator is now available online. With it you can evaluate arbitrary expressions and predicates (using B Syntax). It is a great way to learn about B, predicate logic and set theory or even just to solve arithmetic constraints and puzzles.
Next ProR snapshot coming up soon - please help us prioritize!
Submitted by Michael Jastram on Fri, 03/16/2012 - 18:01
The presentation of ProR and RMF at the ReConf in Munich this week was well received. We got plenty of constructive feedback both from real and potential users, as well as from contributors.
We pledged to create a snapshot build every two months, and we will now focus on getting the March snapshot ready. The focus of that snapshot is threefold:
- Improve the usability of the GUI
- Activate the new core
- Migrate documentation
First, we are keenly aware that the ProR user interface still has a number of issues. The user interface represents the "face" of RMF, and is often the first contact, We want a good first impression, and this is clearly not the case right now. We will organize a three-day "mini-sprint" at the University of Düsseldorf, specifically to work on GUI and usability. To make the most of this, we need your help:
- If you have GUI-related feature requests, please check out the roadmap for the March iteration in the Eclipse wiki. You'll find instructions on how to add your requests. If you are unsure, you can also discuss your issues in the forum or on the dev mailing list. Or you can just email me, if you prefer.
- For actual bugs, please submit it to Bugzilla. Again, you can just email me, if you prefer.
- We could accommodate guests for the sprint. If you are interested in this, please contact me. The sprint is planned for March 26th - 28th.
Second, Mark has been working hard on implementing a new core. So far we used the core implemented by Nirmal. Nirmal did a fabulous job, but the code was quite complex, as it was realized using two models and a transformation from one to the other. This created some headaches in particular when handling <ANY>-elements, which are used for XTHML and tool extensions. Mark reimplemented the core, leveraging his experience from Autosar. This should make maintenance easier and improve performance further.
And last, we are also aware that the documentation is in bad shape. First it was out of date, and currently it is inaccessible. The objective of the sprint is to improve the software, so the improvements to documentation will be limited for now. Please be assured that documentation is a long-term issue for us.
We hope to get plenty of constructive feedback from you on how to make ProR better.
Image: graur razvan ionut / FreeDigitalPhotos.net
Image: jscreationzs / FreeDigitalPhotos.net
Science meets Industry (20.03.2012)
Submitted by Michael Jastram on Mon, 03/05/2012 - 23:37
(Apologies to English speakers: This is an announcement in German for a German-language event)
Innovationen vorstellen, Wissen austauschen und Kooperationen anregen – das ist das Motto der Veranstaltungsreihe Science meets Industry an der Heinrich-Heine-Universität Düsseldorf (HHU). Beim nächsten Treffen am 20. März 2012 werden die Projekte aus dem Bereich Softwaretechnik und dynamischen Programmiersprachen vorgestellt, von denen einige die Grundlage für Formal Mind's Technologien bilden.
In den drei Fachvorträgen geht es um aktuelle Forschungsfragestellungen im Bereich
Softwaretechnik und dynamischen Programmiersprachen. Prof. Leuschel wird eine Einführung in dieses Thema geben. Im folgenden werden konkrete Projekte vorgestellt: Zum Beispiel die Anforderungsplattform "ProR", die sich in kurzer Zeit von einem Forschungsprojekt zu einem OpenSource-Projekt der Eclipse-Foundation entwickelt hat und inzwischen erhebliches Industrieinteresse weckt. Ein weiteres Beispiel ist die grafische Darstellung von Softwaremodellen, was dessen Verständnis erheblich verbessert und die Kommunikation mit Stakeholdern erleichtert.
Wir würden uns freuen, Sie bei dieser kostenlosen Veranstaltung begrüßen zu dürfen:
20. März 2012, 16:00 bis 17:30 Uhr
Universitätsbibliothek, Geb. 24.41
Um Anmeldung unter info@diwa-dus.de wird gebeten.
Flyer mit Details
ProR, RMF and Formal Mind at ReConf 2012
Submitted by Michael Jastram on Fri, 02/24/2012 - 13:30
ReConf is one of the biggest requirements conferences in Europe, and Michael Jastram has been a regular speaker since 2007. This year, he will give two talks:
Structuring of Requirements for a tight integration with Models: requirements management and modeling are related and complementary, but how tightly are they integrated in practice? Take SysML for example, which allows traceability, but in the end, requirements are little more than text blocks. In this talk, an approach is presented that improves traceability between natural language requirements and models. It is based on the WRSPM reference model by Gunther. This alone improves the quality of the requirements. But more importantly, it enables a deep integration with the model. The approach works with various modeling approaches, here we use the formal Event-B method that our research is based on. One key advantage of this method is, that not all requirements have to be modeled. Tool support is available through an integration between ProR and Rodin.
ReqIF in the Open Source: The Eclipse Requirements Modeling Framework: After the release of the ReqIF standard in April 2011 by the OMG, there finally is an international standard that allows working with complex requirements. This could allow ReqIF to become for requirements, what UML became for modeling: a common standard for the community to converge on. This talk presents the Requirements Modeling Framework (RMF). RMF is a new Eclipse Foundation project, consisting of a RIF/ReqIF core and a user interface. RMF grew out of two academic research projects.
If you are interested in meeting Michael Jastram at ReConf, please contact us.
ProR Snapshot Build available
Submitted by Michael Jastram on Fri, 01/20/2012 - 22:53
Good news to everyone interested in ProR - we finally have a snapshot build available on the RMF website. If you are interested in ProR, ReqIF, etc., please give it a spin.
The last release took place in August 2011 - an eternity ago, as far as software is concerned. The reason for this long delay had been announced before: We migrated ProR to Eclipse, where it became the GUI for the Requirements Modeling Framework (RMF). Becoming an Eclipse Foundation process is a huge endeavor: A project has to undergo a comprehensive intellectual property review, and once migrated, there are strict rules to ensure that all IP is accounted for. As if this is not enough, we also performed some major refactoring of the code base.
But we are happy with the result. What we published is not an official release, for which the Eclipse Foundation also has strict rules. Instead, we published a snapshot, representing the current state of the code base. Until we have a continuous integration system, there will be ad hoc releases as needed. In addition, we will work with two month development iterations. At the end each iteration, we will create integration builds. This is documented in our build process.
So, what has actually changed? Here is a high-level summary:
- ProR now supports ReqIF 1.0.1 instead of RIF 1.2
- Much more stable GUI, in part thanks to over 100 new unit tests
- ProR is much more tolerant to issues with the ReqIF file being loaded
- Various small GUI improvements, like automatic creation of columns for Specifications
There are more changes that are not visible to the user. For instance, the source code got broken up into five git repositories.
We already got requests to provide some kind of RIF 1.2 compatibility. Rest assured, the core code for RIF is still present, but it was just not feasible at this point to support more than one version in the GUI, and ReqIF just makes more sense. If you desperately need RIF support in the GUI, then please contact us to find a way to make it possible.
ProR still lacks support for rich text and embedded data. Still, in its current form, it can already be useful for inspecting ReqIF data.
Another major issue is the inability to restore tool data. A lot of functionality is currently provided via Presentation plugins, but their configuration is lost upon reopening a ReqIF file. This results in only limited usefulness for composing requirements with ProR at this point.
We hope that both issues will be resolved by the next integration checkpoint, scheduled for March 2012.
And last, Formal Mind, together with itemis, represents RMF at the ProSTEP ReqIF implementor forum, ensuring that ProR will provide interoperability with industry tools, once they support ReqIF.
Requirements + UML = SysML
Submitted by Michael Jastram on Wed, 12/21/2011 - 18:08
What happens if you start with UML, take a little away, add something new and tweak it a bit? Depending on what exactly you add, you may end up with SysML. SysML created some excitement in the requirements engineering (RE) community, as it provides some rudimentary tools for creating traceability between requirements and model elements.
What does SysML offer to RE?
SysML adds the Requirements Diagram, Requirements Notation, as well as as four dependency relationships (Derive, Verify, Refine, Trace). It includes the Requirements Table as a tool to aggregate all requirements in list form in one place. Here is an example of a requirements diagram, taken from the SysML specification:

Requirements diagrams are fairly straight forward: They consist of boxes labeled with the requirement stereotype which have certain attributes like id and text. They can have relationships (the unlabeled relationships on the right represent the containment relationship).
The relationships shown here are not that exciting, as they concern just requirements. Things get really interesting if relationships to other model elements are created.
How formal is SysML?
There is no formality involved in SysML, just conventions, which can still be useful. Even without rigorous formality, process can be employed for using the manually created and maintained traceability to validate and verify model and requirements.
How useful this is in practice also depends on tool support, and the tool's reporting facilities in particular. If the source or target of a trace changes, it is highly desirable that the tool records this, so that the link can be inspected to see whether it is still valid. Providing this is no rocket science, and process is needed to make such a feature useful in the context of systems development.
ProR as a tool platform for SysML requirements?
The requirements structures defined by SysML could easily be modeled on top of the ReqIF data model: containment relationships would correspond to the hierarchy of specifications, while SpecRelationTypes could model the types of traces. An integration with an Eclipse-based SysML editor like Topcased would be fairly straight forward (see our paper "Requirement Traceability in Topcased with the Requirements Interchange Format (RIF/ReqIF)").
What would be the advantages? First, the ProR requirements editor is more powerful than the requirements table defined by SysML. Second, an arbitrary number of attributes could be added to the requirements and to the traces. Third, ProR could act as the bridge to existing RE tools, thereby facilitating the introduction of model tracing into existing processes. And last, Eclipse-based reporting facilities could be used for analyzing the traceability.
Please tell us what you think about this at the Formal Mind Blog.
Graphics have been taken from the OMG SysML specification under the license terms and copyrights stated therein.
ProB 1.3.4 released
Submitted by Michael Leuschel on Fri, 12/09/2011 - 18:29
ProB 1.3.4 is available. The highlights of this release are:
- an "Evaluation View" to inspect formulas and values,
- an interactive "Eval" window to evaluate expressions and predicates,
- support for CSP assertion checking,
- an improved editor, e.g., with on-the-fly syntax highlighting,
- 64-bit versions for Mac and Linux are now available,
- several performance improvements.
Go to the ProB download page.
