Initially, the Rodin platform for Event-B did away with a textual representation for models. In this paper, we explain why a textual representation was required after all and we present the semantic-aware text editor Camille for Rodin. We explain the design choices of Camille, such as splitting the syntax into two-levels for machine and formula syntax. We also describe the challenges, such as synchronizing the textual representation with the Rodin database, and how they were overcome using an EMF abstraction layer.

Gute Werkzeugunterstützung ist ein wichtiger Aspekt im Requirements Engineering. Es gibt zwar ein breites kommerzielles Angebot, aber wenige offene Lösungen. ProR ist eine OpenSource Software zum Arbeiten mit natürlichsprachigen Anforderungen. Es basiert auf dem Requirements Interchange Format (RIF), womit wir die Interoperabilität mit anderen Werkzeugen gewährleisten. Wir legen großen Wert auf die Erweiterbarkeit der Plattform, was wir mit einem Integrations-Plugin für die formale Event-B-Methode belegen.

One important step of the systems engineering process is requirements engineering. Parallel to the development of Topcased, which includes tooling for requirements engineering, a new standard for requirements exchange is emerging at the OMG under the name “ReqIF” (formally called RIF). In our talk we introduce the activities of two research projects and their tool developments, VERDE (Yakindu Requirements) and Deploy (ProR) and discuss possible synergies with Topcased.

Tracing between informal requirements and formal models is challenging. A method for such tracing should permit to deal efficiently with changes to both the requirements and the model. A particular challenge is posed by the persisting interplay of formal and informal elements.

In this paper, we describe an incremental approach to requirements validation and systems modelling. Formal modelling facilitates a high degree of automation: it serves for validation and traceability.

The foundation for our approach are requirements that are structured according to the WRSPM reference model. We provide a system for traceability with a state-based formal method that supports refinement. We do not require all specification elements to be modelled formally and support incremental incorporation of new specification elements into the formal model. Refinement is used to deal with larger amounts of requirements in a structured way.

We provide a small example using Problem Frames and Event-B to demonstrate our approach.

Requirements engineering (RE) is a crucial aspect in systems development and is the area of ongoing research and process improvement. However, unlike in modelling, there has been no established standard that activities could converge on.

In recent years, the emerging Requirements Interchange Format (RIF/ReqIF) gained more and more visibility in industry, and research projects start to investigate these standards. To avoid redundant efforts in implementing the standard, the VERDE and Deploy projects cooperate to provide a stable common basis for RIF/ReqIF that could be leveraged by other research projects too. In this paper, we present an Eclipse-based extensible implementation of a RIF/ReqIF-based requirements editing platform.

In addition, we are concerned with two related aspects of RE that take advantage of the common platform. First, how can the quality of requirements be improved by replacing or complementing natural language requirements with formal approaches such as domain specific languages or models. Second, how can we establish robust traceability that links requirements and model constructs and other artefacts of the development process. We present two approaches to traceability and two approaches to modelling.

We believe that our research represents a significant contribution to the existing tooling landscape, as it is the first clean-room implementation of the RIF/ReqIF standard. We believe that it will help reduce gaps in often heterogeneous tool chains and inspire new conceptual work and new tools.

Proper tool support in requirements engineering is important. A number of proprietary solutions are available in the market place, but few open solutions, and none that are widespread at this time.

In this paper, we introduce ProR, an open platform for requirements engineering. The project was initiated by the EU FP7 Project ``Deploy'', which has the goal to make major advances in engineering methods for dependable systems through the deployment of formal engineering methods. Rather than building a project-specific solution, we decided to develop an extensible, general purpose platform.

We based the tool's data model on the Requirements Interchange Format (RIF / ReqIF), a standard driven by the automotive industry. This gives us interoperability with a number of existing tools. The tool is based on the Eclipse Platform and uses the Eclipse Modeling Framework (EMF). We managed to establish a cooperation with the ITEA-Project ``Verde'', which supplied the implementation of the RIF data model.

In this paper, we will introduce the tool, describe its architecture, and present a small case study. ProR is still under development, and we welcome contributors and are very interested in potential users to validate our approach. Please visit www.pror.org for more information, and to download the current development version.

Formal modeling of computing systems yields models that are intended to be correct with respect to the requirements that have been formalized. The complexity of typical computing systems can be addressed by formal refinement introducing all the necessary details piecemeal. We report on preliminary results that we have obtained for tracing informal natural-language requirements into formal models across refinement levels. The approach uses the WRSPM reference model for requirements modeling, and Event-B for formal modeling and formal refinement. The combined use of WRSPM and Event-B is facilitated by the rudimentary refinement notion of WRSPM, which provides the foundation for tracing requirements to formal refinements.

We assume that requirements are evolving, meaning that we have to cope with frequent changes of the requirements model and the formal model. Our approach is capable of dealing with frequent changes, making use of corresponding techniques already built into the Event-B method.

Localization Localization is the process of determining the rigid-body translations and rotations that must be performed on a set of points measured on a manufactured surface (like a propeller blade) to move those points into the closest correspondence with the ideal design surface. An additional parameter is an offset distance, such that the Euclidean motion brings the measured points as close as possible to an offset of the design surface. An algorithm to determine the seven parameters (three rotations, three translations, one offset) was developed in 1991 by R. A. Jinkerson. But that algorithm makes some assumptions about the surface and the measured points, which are sometimes not fulfilled. Specifically, it assumes, that a measured point has always an orthogonal projection on the offset surface, regardless of the translation and rotation parameters. This thesis extends Jinkerson's algorithm, so that these assumptions are not necessary any longer. This involves the development of a new objective function and its gradient.

Feature extraction During the manufacturing process, a propeller blade surface is subject to manufacturing inaccuracies, that result in small changes to the data describing its features. It is therefore desirable to recompute these features for comparison with the original design data. Most of the characteristics of a propeller blade are embedded in the camber lines of its hydrofoil sections. The objective of this part of the thesis is to recompute the camber line from a hydrofoil shape curve. An algorithm for this task has already been developed, but it makes the assumption that the blade thickness has a single maximum, which is often not fulfilled, especially, if the hydrofoil has been generated from measured data. In this thesis, a new algorithm has been developed. It generates a highly accurate camber line by using a two pass iteration method: The first pass generates an approximation of the camber line, and the second pass refines this approximation to the desired accuracy.