imported>Leuschel |
imported>WikiSysop |
| Line 1: |
Line 1: |
| − | = Model Animation = | + | = Rodin User and Developer Workshop, 27-29 February 2012, Fontainebleau, France = |
| | | | |
| − | == Overview ==
| |
| − | === Siemens Application===
| |
| − | The most important additions of the last 12 months are:
| |
| − | * Application of ProB in three active deployments, namely the upgrading of the Paris Metro Line 1 for driverless trains, line 4 of the S\~{a}o Paulo metro and line 9 of the Barcelona metro. We also briefly report on experiments on the models of the CDGVAL shuttle. The paper <ref>Leuschel et al. FM'2009</ref> only contained the initial San Juan case study, which was used to evaluate the potential of our approach.
| |
| − | * In this article we describe the previous method adopted by Siemens in much more detail, as well as explaining the performance issues with Atelier B.
| |
| − | * Comparisons and empirical evaluations with other potential approaches and alternate tools (Brama, AnimB, BZ-TT and TLC) have been conducted.
| |
| − | * We provide more details about the ongoing validation process of ProB, which is required by Siemens for it to use ProB to replace the existing method.
| |
| | | | |
| − | The validation also lead to the discovery of errors in the English version of the Atelier B reference manual.
| + | Event-B is a formal method for system-level modelling and analysis. The Rodin Platform is an Eclipse-based toolset for Event-B that provides effective support for modelling and automated proof. The platform is open source and is further extendable with plug-ins. A range of plug-ins have already been developed including ones that support animation, model checking and UML-B. |
| − |
| + | The [http://wiki.event-b.org/index.php/Rodin_Workshop_2009 first Rodin User and Developer Workshop was held in July 2009 at the University of Southampton] while the [http://wiki.event-b.org/index.php/Rodin_Workshop_2010 second took place at the University of Düsseldorf in September 21-23, 2010]. The 2012 workshop will be part of the [http://www.bmethod.com/php/federated-event-2012-en.php DEPLOY Federated Event]. |
| − | Also, since <ref>Leuschel et al. FM'2009</ref>, ProB itself has been further improved inspired by the application, resulting in new optimisations in the kernel (see below).
| |
| | | | |
| − | More details:
| + | While much of the development and use of Rodin takes place within the [http://www.deploy-project.eu EU FP7 DEPLOY Project], there is a growing group of users and plug-in developers outside of DEPLOY. The purpose of this workshop is to bring together existing and potential users and developers of the Rodin toolset and to foster a broader community of Rodin users and developers. |
| − | * <ref>Leuschel et al. FAC, special issue of FM'2009</ref>
| |
| − | * <ref>Leuschel et al. Draft of Validation Report</ref>
| |
| | | | |
| − | === Multi-level Animation ===
| + | For Rodin users the workshop will provide an opportunity to share tool experiences and to gain an understanding of on-going tool developments. For plug-in developers the workshop will provide an opportunity to showcase their tools and to achieve better coordination of tool development effort. |
| − | (ABZ'2010 & SCP journal paper)
| |
| | | | |
| − | === Improvements to the ProB Constraint solver and empirical evaluation ===
| + | The format will be presentations together with plenty of time for discussion. On Day 1 a Developer Tutorial will be held while Days 2 and 3 will be devoted to tool usage and tool developments. The workshop will be followed by an open [http://www.bmethod.com/php/federated-event-2012-en.php Industry Day]. |
| − | Various industrial applications have shown the need for improved constraint-solving capabilities (see CBC Deadlock, Test-Case Generation). In order to evaluate ProB, and detect areas for improvement, we have studied to what extent classical constraint satisfaction problems can be conveniently expressed as B predicates, and then solved by ProB. In particular, we have studied problems such as the n-Queens problem, graph colouring, graph isomorphism detection, time tabling, Sudoku, Hanoi, magic squares, Alphametic puzzles, and several more. We have then compared the performance with respect to other tools, such as the model checker TLC for TLA+, AnimB for Event-B, and Alloy.
| |
| − |
| |
| − | The experiments show that some constraint satisfaction problems can be expressed very conveniently in B and solved very effectively with ProB. For example, TLC takes 8747 seconds (2 hours 25 minuts) to solve the 9-queens problem expressed as a logical predicate; Alloy 4.1.10 with minisat takes 0.406 seconds, ProB 1.3.3 takes 0.01 seconds. For 32 queens, ProB 1.3.3 takes 0.28 seconds, while Alloy 4.1.10 with minisat takes over 4 minutes. For some others, the performance of ProB is still sub-optimal with respect to, e.g., Alloy; we plan to overcome this shortcoming in the future. Our long term goal is that B can not only be used to as a formal method for developing safety critical software, but also as a high-level constraint programming language.
| |
| | | | |
| − | === Constraint-Based Deadlock Checking ===
| + | If you are interested in giving a presentation at the Rodin workshop, send a short abstract (1 or 2 pages of A4) to rodin@ecs.soton.ac.uk by 16 January 2012. Indicate whether it is a tool usage or tool development presentation. Plug-in presentations may be about existing developments or planned future developments. We will endeavour to accommodate all submissions that are relevant to Rodin and Event-B. |
| − | Ensuring the absence of deadlocks is important for certain applications, in particular for Bosch's Adaptive Cruise Control. We are tackling the problem of finding deadlocks via constraint solving rather than by model checking. Indeed, model checking is problematic when the out-degree is very large. In particular, quite often there can be a practically infinite number of ways to instantiate the constants of a B model. In this case, model checking will only find deadlocks for the given constants
| |
| − | chosen.
| |
| | | | |
| − | Idea: solve constraints of axioms, invariant together with a constraint specifying a deadlock.
| |
| | | | |
| − | Required Developments:
| + | '''Organisers''' |
| − | * implementation of the algorithm, with semantic relevance filtering (to be able to restrict the deadlock search to certain scenarios: in Bosch's case due to the flow plugin, one wants to restrict deadlock checking e.g. to states with the variable Counter set to 10).
| |
| − | * Improvements to ProB's constraint solving engine: (reification of constraints, more precise information propagation for membership constraints, performance improvments in the typchecker and other parts of the kernel)
| |
| | | | |
| − | Success: Model 1 and Model 2: CrCtrl_Comb2Final;
| + | Michael Butler, University of Southampton |
| − | relevance of Counter=10 due to flow
| |
| | | | |
| − | Deadlock Freedom PO: 34 pages of ASCII, could not be loaded in Rodin "Java Heap Space Error". Counter examples found for 8 versions in 1-18 seconds.
| + | Stefan Hallerstede, University of Aarhus |
| | | | |
| − | === BMotionStudio for Industrial Models ===
| + | Thierry Lecomte, ClearSy |
| | | | |
| − | Previously, we presented BMotion Studio, a visual editor which enables the developer of a formal model to set-up easily a domain specific visualization for discussing it with the domain expert. However, BMotion Studio had not yet reached the status of an Industrial strength tool due to the lack of important features known from modern editors.
| + | Michael Leuschel, University of Düsseldorf |
| | | | |
| − | In this work we present the improvements to BMotion Studio mainly aimed at upgrading it to an industrial strength tool and to show that we can apply the benefits of BMotion Studio for visualizing more complex models which are on the level of industrial applications. In order to reach this level the contribution of this work consists of three parts:
| + | Alexander Romanovsky, University of Newcastle |
| | | | |
| − | * We added a lot of new features to the graphical editor known from modern editors like: Copy-paste support, undo-redo support, rulers, guides and error reporting. One step towards was the redesign of the graphical editor with GEF.
| + | Laurent Voisin, Systerel |
| − | * Since extensibility is a very important design principle for reaching the level of an industrial strength tool we pointed up the extensibility options of BMotion Studio.
| |
| − | * We introduced the visualization for two models which are on the level of industrial applications in order to demonstrate that we can apply the benefits of BMotion Studio for visualizing more complex models. The first model is a mechanical press controller and the second model is a train system which manages the crossing of trains in a certain track network.
| |
| − | | |
| − | === Various other improvements ===
| |
| − | | |
| − | mainly inspired by Siemens and Bosch Applications
| |
| − | | |
| − | Improved AVL algorithms, more operators
| |
| − | | |
| − | record support, treatment of infinite sets,
| |
| − | | |
| − | == Motivations ==
| |
| − | | |
| − | The above works were motivated mainly to support the following three industrial deployments:
| |
| − | * Siemens: enable Siemens to use ProB in their SIL4 development chain, replacing Atelier B for data validation.
| |
| − | * Bosch: provide animation and constraint-based deadlock detection for the Adaptive Cruise Control
| |
| − | * SAP: provide a way to generate test cases using constraint-based animation
| |
| − | | |
| − | == Available Documentation ==
| |
| − | | |
| − | === References ===
| |
| − | <references/>
| |
| − | | |
| − | == Planning ==
| |
| − | | |
| − | * Finish Validation Report
| |
| − | * Write up Constraint-Based Deadlock Checking and integrate fully into Rodin Platform
| |
| − | * Support mathematical extensions in ProB
| |
| − | * Further improvements in the constraint-solving kernel of ProB; in particular for relations and operators. A Kodkod translator is being developed.
| |
Rodin User and Developer Workshop, 27-29 February 2012, Fontainebleau, France
Event-B is a formal method for system-level modelling and analysis. The Rodin Platform is an Eclipse-based toolset for Event-B that provides effective support for modelling and automated proof. The platform is open source and is further extendable with plug-ins. A range of plug-ins have already been developed including ones that support animation, model checking and UML-B.
The first Rodin User and Developer Workshop was held in July 2009 at the University of Southampton while the second took place at the University of Düsseldorf in September 21-23, 2010. The 2012 workshop will be part of the DEPLOY Federated Event.
While much of the development and use of Rodin takes place within the EU FP7 DEPLOY Project, there is a growing group of users and plug-in developers outside of DEPLOY. The purpose of this workshop is to bring together existing and potential users and developers of the Rodin toolset and to foster a broader community of Rodin users and developers.
For Rodin users the workshop will provide an opportunity to share tool experiences and to gain an understanding of on-going tool developments. For plug-in developers the workshop will provide an opportunity to showcase their tools and to achieve better coordination of tool development effort.
The format will be presentations together with plenty of time for discussion. On Day 1 a Developer Tutorial will be held while Days 2 and 3 will be devoted to tool usage and tool developments. The workshop will be followed by an open Industry Day.
If you are interested in giving a presentation at the Rodin workshop, send a short abstract (1 or 2 pages of A4) to rodin@ecs.soton.ac.uk by 16 January 2012. Indicate whether it is a tool usage or tool development presentation. Plug-in presentations may be about existing developments or planned future developments. We will endeavour to accommodate all submissions that are relevant to Rodin and Event-B.
Organisers
Michael Butler, University of Southampton
Stefan Hallerstede, University of Aarhus
Thierry Lecomte, ClearSy
Michael Leuschel, University of Düsseldorf
Alexander Romanovsky, University of Newcastle
Laurent Voisin, Systerel
