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.
ProR / Requirements Engineering
Submitted by Michael Jastram on Tue, 05/05/2015 - 09:51
Thousands of users are using formalmind Studio on a regular basis, and we get a lot of positive feedback and words of encouragement. But there is one thing that drives many users mad: If an attribute is large, then it is not shown as a whole, but "truncated". This is particularly annoying for embedded images. While there has been a work-around (using edit mode), this was cumbersome and not really that user-friendly.
Therefore, we finally addressed this issue, by building a new Specification editor. Don't worry the old one is still there, in case you prefer it.
Where do I get it?
If you don't use formalmind Studio yet, get the free download. If you have formalmind installed, you should get a notification of the update. You can trigger the update manually via Help | Check for Updates.
The new Specification Editor
The Specification Editor is probably the most important editor in formalmind Studio: It shows a single "Specification", a hierarchical list of requirements. Users can customize it to show only those attributes of interest.
Choosing between Editors
Rather than changing the existing editor, we created a new one. If you find an issue with the new you can always go back. To do so, right-click the .reqif file in the Project View and select Open With... | Reqif10 Model Editor. This choice is remembered for that file. To use the new editor, select Open With... | fmStudio Main Editor.
With the latest version of formalmind Studio, the new editor is the default. Which one is used can be recognized by the editor icon: the new one or the old one .
Rearrange Columns with Drag and Drop
The new editor also finally allows the moving of columns using drag and drop. Grabbing the column header and dropping it on another one will insert it to the left of the target column.
Seeing truncated content
The screenshot below demonstrates how the showing of truncated content works: simply move the mouse over a truncated cell, and after a short delay, the complete content is shown. The preview extends as far down as needed, showing scrollbars if necessary. The preview stays visible until the mouse is moved away (or the user hits escape). Scrolling works both with mouse and keyboard.
You may notice that the outline has also changed in multiple ways. First, it only shows the elements of the opened Specification, removing the clutter that was shown before (other Specifications, list of all SpecObjects, etc.). These are still accessible when the main editor is active.
Second Specification Editor and Outline are always synchronized.
Third, each Specification Editor has its own selection. So if a model has multiple Specifications and you open them all, the outline selection changes with the active editor.
Bug Fixes and Improvements
Last, there were some scenarios where the selection in the editor was lost, resulting in the cursor jumping to the beginning of the table. Obviously, this can be very annoying, especially with large specification. This should not happen any more.
There are many more small bug fixes and improvements, which should make working with formalmind Studio more pleasant. Enjoy!
Image courtesy of vectorolie at FreeDigitalPhotos.net
Submitted by Michael Jastram on Fri, 12/20/2013 - 10:39
Another year has passed, and we would like to thank our customers and the users of our technologies for working with us.
The holiday season is a good time for reflecting, and we are proud to see our motto - science for systems engineering - applied in practice. What we achieved has been made possible by customers who believe in our technologies and who subscribe to our principles. One of our most valued principles is openness: science should not be an end in itself: It is a means for making this world a better place. We believe that openness acts as a multiplier that increases overall wealth. Here are three examples of our modest contributions in this respect in 2013:
If you need to comply with ISO 26262, IEC 61508 or similar standards, you may need to work more formal
Submitted by Michael Jastram on Wed, 11/13/2013 - 17:34
It's quite impressive how safe cars, planes and trains are today. Looking at this, it seems that we understand really well how to build reliable systems. This is in part due to safety standards. When they are not followed, as it seems to have been the case with Toyota, things can go wrong. Safety standards evolve, for two reasons: They evolve as we learn more about safety, and they evolve, as they need to adapt to the complexity found in today's systems. That's why they started to recommend the use of formal methods.
Before we look into formal methods, and how they relate to requirements, let's get an overview of safety standards. The following figure has been taken from the Deploy Wiki, which provides quite a bit of analysis.
Submitted by Michael Jastram on Mon, 09/30/2013 - 14:48
The Requirements Interchange Format (ReqIF) came a long way, ever since its inception in 2004, when members of the Herstellerinitiative Software (HIS), a trade association of five major car manufacturers, decided to commission the creation of a requirements exchange format. Step by step, the standard became more mature and was changing patronage, until it finally became an international standard of the Object Management Group (OMG), a not-for-profit computer industry standards consortium.
Recently the focus for ReqIF changed from standardization (pretty much done) to applicability. In particular, users and tool vendors are actively ensuring interoperability of the various tools that support ReqIF, by working together in an Implementor Forum that is lead by ProSTEP iViP, an association for the manufacturing industry. Eight tool vendors work peacefully together to ensure that requirements data exported by one tool can be processed by another.
This is good news for manufacturers and suppliers of industries where requirements are exchanged. But what does this all mean? Who is affected, what changes are expected? This article makes an attempt to answer some of these questions.
Submitted by Michael Jastram on Mon, 08/12/2013 - 14:30
The RMF team is proud to announce the 0.8.0 version of RMF and ProR (Download) to spice up your summer. The most visible improvements regards the handling of default values, which we will describe further below. You can also import examples into your workspace via File | New | Example.... This should be useful to new users, to get an idea of what's possible.
But there are also a number of back-end improvements that either resolve issues or speed up things. We hope that you will give ProR 0.8.0 a try. If you have ProR already installed, you can update via Help | Check for Updates.
Submitted by Michael Jastram on Fri, 08/02/2013 - 10:46
We've all seen it: You need to write a spec, so you open Word, write some text, you copy a state diagram from Enterprise Architect, and eventually send it off as a PDF.
Okay, things are slightly better now. In the Eclipse ecosystem, maybe you are using Papyrus for modeling with UML or SysML. You may even use a real requirements tool, like Eclipse ProR. But again, you need to get that diagram into the model, so you will still perform the dreaded copy & paste operation, which will inevitably convert your beautiful model into a lifeless bitmap.
There have been attempts to correct this, for instance by connecting the models with a traceability framework. This is a step forward and allows you to create and analyze your traceability, but it ignores the issue of presentation.
An RMF-based Canvas
What we've been experimenting with, and where we see a lot of potential is RMF-based model integration and traceability. The Requirements Modeling Framework is an established project for working with textual requirements, which uses ReqIF, an OMG standard, as the underlying data model. We noticed that ReqIF already contains everything you need for traceability: atomic requirements ("SpecObjects") that can by customized with an arbitrary number of typed attributes, and traces ("SpecRelations"), that likewise can hold any number of attributes. But on the downside, you are confined to the ReqIF universe: You can only create traces between SpecObjects.
But here is the idea: Introduce SpecObjects that act as proxies. These contain references, which are resolved upon rendering. ProR renders information in a grid structure, not unlike Excel (but with a hierarchy). Every box represents the value of a SpecObject, so it is contained in an atomic fashion, with a neat rectangular border around it. We've already implemented this for traceability to Event-B (formal) models, but we are currently working on a generic solution for EMF-based models.
So this is the vision: You work within Eclipse, e.g. you create a UML state diagram in Papyrus. You then drag it into ProR (the RMF user interface), where a proxy element is constructed that renders the diagram seamlessly in your specification (in a box with a border around it). Suddenly, what used to be a requirements tool, becomes a drawing board with boxes that can be filled with content from anywhere - content that is referenced, and rendered on demand. The user does not care whether the content is retrieved from another model that is active within Eclipse, or via a web service, or OLSC, from half across the world.
We broadly identified three integration models, that we would like to present here:
Proxy element in text flow
A proxy element can be inserted simply into the flow of SpecObjects, as shown above. This is the equivalent of "copy and paste" (no traceability), but at least the content is always up to date. In the above figure, the proxy element is a child (as seen from the indentation), to indicate the parent-child relationship.
Proxy element with additional attributes
A proxy element can be enriched with "normal" attributes, which tightly connects all values - they represent one unit. This is shown in the above figure, that shows a ReqIF-value and proxy-value next to each other.
Proxy element via SpecRelation
Last, a "classical" traceability can also be realized. But in contrast to external solutions, we use (ReqIF) SpecRelations for the traceability. As a result, the link target's name that is shown in the main view is provided by the model (in this example "safety_property (mac)". The actual value can be inspected in the Properties View, by simply selecting the link target.
Put it to work
Of course, these three approaches can be mixed and matched, to maximize value. For instance, it makes a lot of sense to establish a linked-based traceability, for instance to check the modeling coverage or to analyze the impact of changes.
There are a number of advantages to this approach: The user can find the most convenient presentation, referencing other content in-line (in a box) or via a link; to analyze the traceability, only the ReqIF data structures have to be known, the analyzer can be oblivious to where the content is pulled from; And last, is is possible to store a cashed version of the content, in addition to the ID. This means that by sharing the ReqIF model, the traceability is shared as well. You could open the exported .reqifz file in Rational DOORS, and you would see all the referenced content (which of course may be stale and cannot be edited here, but hey, it's in DOORS). Even better, you could use DOORS' powerful traceability analysis tools.
Next in line: Papyrus (UML and SysML)
What we just described has been realized and is available for the (Eclipse-based) Rodin platform, which supports the Event-B modeling language. But Event-B is rather exotic. Therefore, we are working on a Papyurs-integration right now.
Image courtesy of digitalart / FreeDigitalPhotos.net
Submitted by Said Salem on Mon, 07/08/2013 - 17:43
ProR doesn't yet support mature reporting features. Right now only a simple HTML-Version of a requirements document can be generated (you can access this via the print menu). A better visual representation of the requirements document has been requested many times by users. For instance, such a reporting mechanism would support analysis and traceability.
We are pleased to announce that we will develop better reporting in collaboration with the Heinrich-Heine University of Düsseldorf. This work will be realized in the context of a Master's thesis. Consequently, the resulting solution will be donated to the Eclipse Foundation and will be open source.
There are several reporting frameworks which could be used for the report generation of ProR. These frameworks offer a diverse range of reporting features. The choice should be based on the stakeholder needs.
This is where you come in: We would like to know which reporting features you consider important or not in the scope of requirements management. To ease elicitation, a survey was created to identify these features. It consists of very few questions and should take about three minutes. Based on the survey results we will identify the essential requirements for a reporting tool for ProR and decide which reporting framework would be the best fit.
If you are interested in participating in this survey, just follow the link:
Also, please feel free to forward this request to colleagues, friends and other interested parties.
Image (Reporting) courtesy of [Pong] / FreeDigitalPhotos.net
Submitted by Michael Jastram on Sun, 07/07/2013 - 10:35
Use Cases are a popular method for recording requirements. With little effort, ProR can make recording Use Cases easy and traceable. To demonstrate this, we use ProR itself as an example. Below is a screenshot of ProR, recording the use case "Create a new SpecObject". You can download this requirements model from the Eclipse git repository. In the following, we point out where this model specifically takes advantage of ProR's features, and conclude in the end how further integration with other models (SysML modeling, testing), could be realized.
Line 1: Headline and IDs
The Use Case has an ID (UC-1). This ID is generated by the ID Presentation. Also, the line is shown in a large, boldface font. This has been realized with the Headline Presentation.
Line 1 (below): Link to Actor
Use Cases have a primary actor, which is realized with a link. In this example, the primary actor is the "Requirements Engineer". There is a separate document (Specification), where all actors are defined (see screenshot right). The role "Primary Actor" is also selected from a list of pre-defined roles from a drop-down.
Line 1.1: Explanatory Text
Information text can be added anywhere and does not have an ID (as none is needed)
Lines 1.3, 1.4 and 1.5: Scenarios
Scenarios have their own SpecType. Via the Headline Presentation, it is also formatted in a more visible manner. In addition, it has a status field, which allow the tracking of the implementation status of the various scenarios.
The result of this approach is a document-like description of use casees. A handful of SpecTypes are used to manage appearance and to keep the model free of formatting information. This makes reuse and linking of models outside ProR easier. References (Actors) and selection lists (Status, Relationship) are used to prevent duplicating of information and to lead and support the requirements engineer in their work.
What we just presented can be realized with ProR stand-alone. However, we are currently investigating simple integrations that could add significant value. These include:
UML/SysML (Use Cases, Actors)
Papyrus is an Eclipse-Project that allow UML and SysML modeling. The approach for modeling use cases could leverage Papyrus for UML/SysML integration. Such an integration would:
- Keep UML and ProR Use Cases synchronized: Creating a UML Use Case would automatically generate the corresponding elements in ProR.
- While in Papyrus, only Use Case ID and name would be shown, the content could be managed (and enriched) with ProR.
- Use Case-Actor-Associations could still be realized in Papyrus. But the relationship would appear synchronized in ProR.
The benefit would be a textual representation, as preferred by many stakeholders, while allowing the reuse of modeling element is UML/SysML
Mylyn (Project Management)
Mylyn is a popular tool for bug and feature tracking that seamlessly integrates in Eclipse. An Integration could create and track a Mylyn issue for each scenario. The status shown in ProR could be taken directly from Mylyn. Using Mylyn would abstract the tracking system from the integration: It would not matter whether Mylyn uses (for example) Bugzilla or Jira underneath.
JUnit (Implementation Status)
If would be possible to associate unit tests with individual scenarios. Then a status field could be managed automatically by analyzing the associated unit tests: If only one test fails, the scenario would be marked as broken.
We hope that this little example demonstrates how using a specialized tool can improve the requirements engineering process significantly. While the integrations do not exists, they could be implemented with a few day's work each by an experienced developer. The Eclipse ecosystem ensures that the resulting code is compact and maintainable.
Submitted by Maha Jastram on Wed, 05/15/2013 - 10:04
Formal Mind is pleased to invite you to the following event with
Professor Jan Peleska and Professor Wen-Ling Huang:
SysML, Formal Semantics and Their Uses in Model-Based Testing
Monday, May 27th, 2013, 10:00-12:30
University of Düsseldorf
Lecture will be held in German. Participation is free of charge.
Non-Faculty members, please rsvp at firstname.lastname@example.org
Abstract: Over the las few years, the published UML and SysML specifications from the OMG have been continuously improved. Today they deliver an exceptional foundation for semantic interpretation. In regards to formal syntax and statistical semantics, the use of Object Constraint Language (OCL) an extensive degree of precision has been reached – this includes situations where one has to reckon with faulty OCL interpretations or conflicting textural and formal data. Natural language rules apply in relation to behavioral semantics. These are clear enough and can be implemented in a formal specification. There are ambiguities with respect to Semantic Variation Points, which need to be defined in a project specific or tool specific manner.
We will demonstrate how to construct a a formal real-time semantic specification and how the behavior can be expressed through block-operations and state machines. This construction leads to a transitional relationship which combines discrete steps in zero time with delays, producing a real-time semantic with either dense time or discrete time, synchronous or interleaving semantics. We will demonstrate the practical application of construction in model-based testing and Bounded Model Checking with the help of the RT-Tester tool, which was developed by Verified Systems with the cooperation of the University of Bremen.
Submitted by Michael Jastram on Fri, 05/10/2013 - 10:39
We are proud to announce the release of RMF ProR 0.7.0 and ProR Essentials 0.7.0. Download them now from the Eclipse website. If you already have ProR 0.5.0 or newer, simply update via Help | Check for Updates.
In Version 0.7.0, 16 features and bugs have been implemented/fixed. The biggest visible improvement for users is a new way of creating links between requirements (SpecObjects).
The old way of linking...
Before 0.7.0, linking was established by using drag and drop. By holding down a modifier key (platform dependent), using drag and drop would not move the dragged elements, but link them instead. While this works fine, there are some disadvantages to this approach: Only one link at a time would be created; the resulting link was untyped (requiring additional clicks to assign a type); "long distance" linking was tedious.
The old way of linking still exists, but a new way of linking as been added.
... and the new way of linking
With the new approach, starting a link and completing the link are two distinct steps. Further, linking is not limited to creating one link at a time, but "n to m" linking is possible. And last, the links can be created with a specific type. Here is a demonstration on the new link process:
- Right-click the element or elements that you would like to link with. The context menu now contains an entry Initiate Linking. The number in parentheses indicates how many requirements are selected (see screenshot).
- Select the requirement or requirements that you want to link to. Right-click the element or elements to link the previously stored requirements with. You will now see two additional context menus: Complete Linking to selection and Complete Linking from selection. The number in parenthesis indicates how many requirements have been stored previously. In the screenshot below, two elements have been selected, but previously, one requirement has been stored. You also see that it is still possible to create untyped links, but that all existing types are available (in this case Realizes Link and isRelated Link).
- The selection of requirements that the process has been initiated with is not cleared. Therefore, you can repeat the previous step as many times as you need, to link from/to those stored requirements.
Please spread the word and tell us what you think
We are thrilled that ProR is now being downloaded 200 times every month. We are genuinely interested in hearing how you use ProR, what is good, what is bad, etc. Please take a minute or two and tell us. You can just reply to this email, or use the Formal Mind Forum or the Eclipse Forum.
If you like to hear about ProR, RMF and requirements on a regular basis, consider subscribing to our newsletter. We send relevant and useful information once or twice a month. Also, please forward this newsletters to your colleagues.