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.