Automated Property Verification for Large Scale B Models with ProB
[PDF] [Bibtex]Formal Aspects of Computing, 23(6): 683-709, 2011.
In this paper we describe the successful application of the ProB validation tool for several industrial applications. The initial case study centred on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for Atelier B. Atelier B, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense (and they need to be revalidated whenever the rail network infrastructure changes).
In this paper we show how we were able to use ProB to validate all of the about 300 properties of the San Juan deployment, detecting exactly the same faults automatically in a few minutes that were manually uncovered in about one man-month. We have repeated this task for three ongoing projects at Siemens, notably the ongoing automatisation of the line 1 of the Paris Metro. Here again, about a man month of effort has been replaced by a few minutes of computation.
This achievement required the extension of the ProB kernel for large sets as well as an improved constraint propagation phase. We also outline some of the effort and features that were required in moving from a tool capable of dealing with medium-sized examples towards a tool able to deal with actual industrial specifications. We also describe the issue of validating ProB, so that it can be integrated into the SIL4 development chain at Siemens.
Constraint-Based Deadlock Checking of High-Level Specifications
[PDF] [Bibtex]Theory and Practice of Logic Programming, 11(4-5): 767-782, 2011.
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.
Developing Camille, a text editor for Rodin
[Bibtex]Software: Practice and Experience, 41(2): 189-198, 2011.
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.
ProR - Eine Softwareplattform für Requirements Engineering
[PDF] [Bibtex]Softwaretechnik-Trends, 31(1), 2011.
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.
Requirement Traceability in Topcased with the Requirements Interchange Format (RIF/ReqIF)
[PDF] [Bibtex]First Topcased Days Toulouse, 2011.
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.
Validation of Formal Models by Refinement Animation
[PDF] [Bibtex]Science of Computer Programming, In Press, Corrected Proof, 2011.
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.
Finding Deadlocks of Event-B Models by Constraint Solving
[PDF] [Bibtex]In B2011 Workshop (short paper), 2011.
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.
In Proceedings ICFEM'2011, volume 6991 of Lecture Notes in Computer Science, Springer, 2011.
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.
In Proceedings of Fundamental Approaches to Software Engineering (FASE) 2011, volume 6603 of Lecture Notes in Computer Science, Springer, 2011.
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.
Runtime Feedback in a Meta-Tracing JIT for Efficient Dynamic Languages
[Bibtex]In Proceedings of the 6th workshop on the Implementation, Compilation, Optimization of Object-Oriented Languages and Programming Systems series = ICOOOLPS '11, 2011.
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.
Allocation removal by partial evaluation in a tracing JIT
[PDF] [Bibtex]In PEPM, 2011.
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.
Mixing Formal and Informal Model Elements for Tracing Requirements
[PDF] [Bibtex]In booktitle, AVOCS 2011, 2011.
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, Traceability and DSLs in Eclipse with the Requirements Interchange Format (RIF/ReqIF)
[PDF] [Bibtex]Technical Report, Dagstuhl-Workshop MBEES 2011: Modellbasierte Entwicklung eingebetteter Systeme, 2011.
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.
