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.

We provide a detailed description of refinement in Event-B, both as a contribution in itself and as a foundation for the approach to simultaneous animation of multiple levels of refinement that we propose. We present an algorithm for simultaneous multi-level animation of refinement, and show how it can be used to detect a variety of errors that occur frequently when using refinement. The algorithm has been implemented in ProB and we applied it to several case studies, showing that multi-level animation is tractable also on larger models. We present empirical results and discuss how the algorithm can be combined with symmetry reduction.

Establishing the absence of deadlocks is important in many applications of formal methods. The use of model checking for finding deadlocks in formal models is limited because in many industrial applications the state space is either infinite or much too large to be explored exhaustively. In this paper we propose a constraint-based approach to finding deadlocks employing the ProB constraint solver to find values for the constants and variables of formal models that describe a deadlocking state. We discuss the principles of the technique implemented in ProB's Prolog kernel and present some results of a larger case study to which we have applied the approach.

The development of the Event-B formal method and the supporting tools Rodin and ProB was guided by practical experiences with the B-Method, the Z specification notation, VDM and similar practical formal methods. The case study discussed in this article - a cruise control system - is a serious test of industrial use. We report on where Event-B and its tools have succeeded, where they have not. We also report on advances that were inspired by the case study. Interestingly, the case study was not a pure formal methods problem. In addition to Event-B, it used Problem Frames for capturing requirements. The interaction between the two proved to be crucial for the success of the case study. The heart of the problem was tracing informal requirements from Problem Frames descriptions to formal Event-B models. To a large degree, this issue dictated the approach that had to be used for formal modelling. A dedicated record theory and dedicated tool support were required. The size of the formal models rather than complex individual formulas was the main challenge for tool support.

Establishing the absence of deadlocks is important in many applications of formal methods. The use of model checking for finding deadlocks in formal models is limited because in many industrial applications the state space is either infinite or much too large to be explored exhaustively.

In this paper we propose a constraint-based approach to finding deadlocks employing the ProB constraint solver to find values for the constants and variables of formal models that describe a deadlocking state. We present the general technique, as well as various improvements that had to be performed on ProB's Prolog kernel, such as reification of membership and arithmetic constraints.

ProB typically finds counter examples to deadlock-freedom constraints, a formula of about 900 partly nested conjunctions and disjunction among them 80 arithmetic and 150 set-theoretic predicates (in total a formula of 30 pages), in under two seconds.

We also present other successful applications of this new technique, in particular to BPEL processes. Experiments using SAT and SMT solvers on these constraints were thus far unsuccessful.

In Event-B a system is developed using refinement. The language is based on a relatively small core; in particular there is only a very small number of substitutions. This results in much simpler proof obligations, that can be handled by automatic tools. However, the downside is that, in case of software development, structural information is not explicitly available but hidden in the chain of refinements. This paper discusses a method to uncover these implicit algorithmic structures and use them in a model checker. Other applications are code generation, model comprehension, and testcase generation.

Meta-tracing JIT compilers can be applied to a variety of differ- ent languages without explicitly encoding language semantics into the compiler. So far, they lacked a way to give the language im- plementor control over runtime feedback. This restricted their per- formance. In this paper we describe the mechanisms in PyPy’s meta-tracing JIT that can be used to control runtime feedback in language-specific ways. These mechanisms are flexible enough to express classical VM techniques such as maps and runtime type feedback.

The performance of many dynamic language implementations suffers from high allocation rates and runtime type checks. This makes dynamic languages less applicable to purely algorithmic problems, despite their growing popularity. In this paper we present a simple compiler optimization based on online partial evaluation to remove object allocations and runtime type checks in the context of a tracing JIT. We evaluate the optimization using a Python VM and find that it gives good results for all our (real-life) benchmarks.

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.