imported>Leuschel |
imported>Nicolas |
| Line 1: |
Line 1: |
| − | = Overview =
| + | The Developer Support provides resources for developing plug-ins for the Rodin Platform. |
| − | This part of the deliverable describes improvement of the ProB animation and model checking plugin.
| |
| | | | |
| − | The improvements and development of ProB were mainly carried out by University of Düsseldorf, with some support by the University of Southampton.
| |
| − | Furthermore, the work was driven by requirements of Siemens and SAP; some tool development was also undertaken by SAP.
| |
| | | | |
| − | New features:
| + | == Rodin Platform Overview == |
| − | * Multi-level animation and validation
| + | [[Getting Started]] |
| − | * B-Motion Studio
| |
| − | * Disprover Support
| |
| − | * first steps towards test-case generation
| |
| | | | |
| − | Improvements:
| + | == Architecture of the Rodin Platform == |
| − | * Scalability improvements driven by Siemens and SAP applications
| |
| − | * Using proof information to improve model checking
| |
| | | | |
| − | Other works:
| + | === Rodin Platform Core === |
| − | * First steps towards validation of ProB for usage by Siemens in SIL-4 chain
| |
| − | * Evaluation against SAT/SMT/BDD-based approaches
| |
| | | | |
| − | = Motivations =
| + | * [[Database]] |
| − | This paragraph shall express the motivation for each tool extension and improvement. More precisely, it shall first indicate the state before the work, the encountered difficulties, and shall highlight the requirements (eg. those of industrial partners). Then, it shall summarize how these requirements are addressed and what are the main benefits.
| |
| | | | |
| | + | * [[Builder]] |
| | | | |
| − | === Multi-level Animation and Validation ===
| + | * [[Rodin Index Design]] |
| | | | |
| − | Thus far ProB only alllowed single-level animation, i.e., the animator would animate a single refinement level in isolation.
| + | * [[Indexing System]] |
| − | This meant that ProB was not able to detect a large class of potential errors in the model:
| |
| − | * a broken gluing invariant | |
| − | * an invalid witness
| |
| − | * violation of guard strengthening
| |
| − | * violation of variant decrease (resp. decrease or stability) for convergent (resp. anticipated) events
| |
| | | | |
| − | The new validation algorithm now can animate a range of refinements together. The user can decide which levels are to be animated together.
| + | * [[Undo Redo]] |
| − | As such, all of the above errors can now be detected by ProB.
| |
| − | User experience is also improved, as he or she can inspect also the abstract variables.
| |
| − | The new algorithm has been sucessfully applied to various case studies, and thus far up to 14 levels have been animated concurrently without problem.
| |
| | | | |
| | + | * [[File Root Separation]] |
| | | | |
| − | === B-Motion Studio === | + | === Event-B User Interface === |
| | | | |
| − | It is often very important to be able to show a formal model to a domain expert or manager, not versed in formal methods.
| + | The Event-B User Interface of the Roding Platform has two major components that are concerned with either [[Modelling User Interface|modelling]] in Event-B or [[Proving User Interface|proving]] properties of models. |
| − | For example, only a domain expert will be able to detect certain mistakes in the formal model.
| |
| − | To enable to easily and quickly build graphical visualisations of Rodin models, we have developed B-Motion Studio.
| |
| − | B-Motion Studio comes with a graphical editor to arrange graphical components and link them with the formal model. | |
| − | No new programming language has to be learned: the linking is described in B itself.
| |
| − | To run a graphical visualisation, the ProB animator is used.
| |
| | | | |
| − | === Test-Case Generation ===
| + | * [[Modelling User Interface]] |
| | | | |
| − | During deployment in the SAP workpackage it became clear that test-case generation from the Event-B models
| + | * [[Proving User Interface]] |
| − | is required for success.
| |
| − | In this task, we have developed a first algorithm for test-case generation, which ensures complete transition coverage of a high-level model, and translates the test-cases into traces of a refined model, so that the tests can be run on the "real" system.
| |
| − | Optimisations, to reduce the length and number of test cases, as well as to minimise race conditions, have been implemented.
| |
| | | | |
| − | === Scalability and Validation ===
| + | Apart from these are more minor components. |
| − | We tackled a case study in WP2, which centres 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 AtelierB. AtelierB, 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). I
| |
| | | | |
| − | The motivation then was to try and use ProB for this task.
| + | * [[Proof Purger Design|Proof Purger]] allows to delete unused proofs. |
| − | This required a considerable amount of work on improving the scalability of the ProB kernel, to be able to deal with large sets and relations.
| |
| − | The ProB parser and type checker also had to be re-developed to be able to deal with large industrial specifications.
| |
| | | | |
| − | The case study was a succcess:ProB was able to validate all of the about 300 properties of the San Juan deployment, detecting exactly the same faults automatically in around 17 minutes that were manually uncovered in about one man-month.
| + | * [[Proof Skeleton Design]] is a view that displays skeletons of existing proofs |
| | | | |
| − | This leads to the next task: the issue of validating ProB, so that it can be integrated into the SIL4 development chain at Siemens
| + | * [[Auto-Completion Design]] proposes a list of names to the user editing a model |
| | | | |
| − | === Proof Directed Model Checking === | + | === Event-B Component Library === |
| | | | |
| − | Jens: can you insert something?
| + | Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an [[Abstract Syntax Tree|abstract syntax tree]]. Abstract syntax trees are manipulated by means of a class library that can be used independently of Eclipse. They are saved in the database in human-readable form as Unicode character strings. Event-B constructs, such as contexts and machines, are not represented as abstract syntax trees. They are stored and retrieved directly from the database (by contrast, mathematical formulas need additional parsing). Well-formedness of Event-B constructs is verified by a [[Static Checker|static checker]]. The static checker has two main purposes: (1) it generates error messages for ill-formed constructs, and (2) it filters well-formed parts of components to be subjected to proof obligation generation. The [[Proof Obligation Generator|proof obligation generator]] uses those parts of constructs that are well-formed and generates proof obligations from them. Finally, the [[Proof Manager|proof manager]] attempts to prove proof obligations and maintains existing proofs associated with proof obligations. The proof manager works automatically and interactively. When new proof obligations have been generated it attempts to discharge them automatically. If it does not succeed, it permits interactive proof (by means of the [[Proving User Interface|proving user interface]]). |
| | | | |
| | + | * [[Abstract Syntax Tree]] |
| | | | |
| − | === SAT/SMT/Kodkod ===
| + | * [[Static Checker]] |
| | | | |
| − | In this subtask we investigate alternate approaches for validating high-level B models using techniques and tools based on BDDs, SAT-solving and SMT-solving.
| + | * [[Proof Obligation Generator]] |
| − | The overall motivation is to improve the scalability of the animator and model checker.
| |
| | | | |
| − | === Disprover ===
| + | * [[Proof Manager]] |
| | | | |
| − | In order to help the user, we wanted to make it possible to apply ProB to individual proof obligations.
| + | * [[Proof Simplification]] |
| − | In some cases, this enables proving a sequent by exhaustive case analysis.
| |
| − | Also, if ProB finds a counter example, the user gets important feedback: the proof obligation cannot be discharged, along with a reason why.
| |
| | | | |
| − | = Choices / Decisions = | + | == Extending Rodin == |
| − | This paragraph shall summarize the decisions (eg. design decisions) and justify them. Thus, it may present the studied solutions, through their main advantages and inconvenients, to legitimate the final choices.
| |
| | | | |
| − | = Available Documentation =
| + | * [[Getting Started]] |
| | | | |
| − | == User Manual ==
| + | * [[Plug-in Tutorial]] |
| | | | |
| − | [http://asap0.cs.uni-duesseldorf.de/trac/prob/wiki/ ProB User Manual] | + | * [[Extending the project explorer]] |
| | | | |
| − | == Published Papers ==
| + | * [[Extending the Proof Manager]] |
| | | | |
| − | Below is a list of published papers, along with an abstract.
| + | * [[Extending the Index Manager]] |
| | | | |
| − | === Improved Kernel to deal with large sets and relations ===
| + | * [[Index Query]] |
| − | In this part we describe the successful application of the ProB validation tool on an industrial case study. The case study centres 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 AtelierB. AtelierB, 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 around 17 minutes that were manually uncovered in about one man-month. 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. Notably, a new parser and type checker had to be developed. We also touch upon the issue of validating ProB, so that it can be integrated into the SIL4 development chain at Siemens
| |
| | | | |
| | + | == Useful Hints == |
| | | | |
| − | [http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=248 Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge. Automated Property Verification for Large Scale B Models, FM'2009.]
| + | === Version Control === |
| | | | |
| − | === Multi-Level Animation and Validation ===
| + | All sources of the core Rodin platform (and of some plug-ins) are managed under version control in SourceForge. The repository currently used is Subversion and can be accessed using URL [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp]. |
| − | 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.
| |
| | | | |
| − | [http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=256 Stefan Hallerstede, Michael Leuschel, Daniel Plagge. Refinement-Animation for Event-B --- Towards a Method of Validation. ABZ'2010 ]
| + | === Testing === |
| | | | |
| − | See also [http://www.springerlink.com/content/282p2316x7165588/ Stefan Hallerstede, Michael Leuschel. How to Explain Mistakes. TFM'09.]
| + | === Debugging === |
| | | | |
| − | === Test-Case Generation === | + | === Publishing === |
| − | Choreography models describe the communication protocols between services. Testing of service choreographies is an important task for the quality assurance of service-based systems as used e.g. in the context of service-oriented architectures (SOA). The formal modeling of service choreographies enables a model-based integration testing (MBIT) approach. We present MBIT methods for our service choreography modeling approach called Message Choreography Models (MCM). For the model-based testing of service choreographies, MCMs are translated into Event-B models and used as input for our test generator which uses the model checker ProB.
| |
| | | | |
| − | [http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=252 Sebastian Wieczorek, Vitaly Kozyura, Andreas Roth, Michael Leuschel, Jens Bendisposto, Daniel Plagge, Ina Schieferdecker. Applying Model Checking to Generate Model-based Integration Tests from Choreography Models. TESTCOM/FATES 2009.]
| + | A Plug-in developed for the Rodin Platform will normally consist of a collection of eclipse 'plugin' projects and a single eclipse 'feature' project. The feature project contains branding information such as logo's icons and licensing details. It is also used to identify your Plug-in so that users can install it. To build your Plug-in use an eclipse 'site' project. This will build the jar files for your plugin projects and a jar for your feature. See eclipse documentation for more details. |
| | | | |
| | + | Now you need to make your Plug-in available for users to install via the Main Rodin Update site (which comes built-in to the Rodin platform). |
| | | | |
| − | === Proof-Directed Model Checking ===
| + | First upload your jar files onto the Sourceforge uploads area and then create a new release in the FRS (Admin-file releases). Note that you should include a zip of the complete source projects to comply with Sourceforge rules. You must not repeat files that have not changed. Sourceforge does not allow you to upload multiple copies of the same jar file. The Feature jar will take care of unchanged plugin jars and use the existing links. Only new jars should be included in a particular release. |
| − | With the aid of the ProB Plugin, the Rodin Platform provides an integrated environment for editing, proving, animating and model checking Event-B models. This is of considerable benefit to the modeler, as it allows him to switch between the various tools to validate, debug and improve his or her models. The crucial idea of this paper is that the integrated platform also provides benefits to the tool developer, i.e., it allows easy access to information from other tools. Indeed, there has been considerable interest in combining model checking, proving and testing. In previous work we have already shown how a model checker can be used to complement the Event-B proving environment, by acting as a disprover. In this paper we show how the prover can help improve the efficiency of the animator and model checker.
| + | See here for details:- http://alexandria.wiki.sourceforge.net/File+Release+System+-+Offering+Files+for+Download |
| | | | |
| − | [http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=253 Jens Bendisposto, Michael Leuschel. Proof Assisted Model Checking for B. ICFEM 2009.]
| + | Finally, the update site must be updated to redirect the update requests to the files on the FRS. |
| | + | (Currently this is done by Colin Snook on request - see Rodin developers page for contact details). |
| | | | |
| − | === Debugging Tricky Proof Obligations with the ProB Disprover ===
| + | [[Details for Maintaining Main Rodin Update Site]] |
| − | While a large number of proof obligations can be discharged automatically by tools such as the RODIN platform, a considerable number still have to be proven interactively. In this paper, we we describe a disprover plugin for RODIN that utilizes ProB to automatically find counterexamples for a given problematic proof obligation. In case the disprover finds a counterexample, the user can directly investigate the source of teh problem, as pinpointed by the counterexample. We also discuss under which circumstances our plug-in can be used as a prover, i.e., when the absence of a counterexample
| |
| − | actually is a proof of the proof obligation.
| |
| | | | |
| − | [http://www.stups.uni-duesseldorf.de/publications_detail.php?id=219 Olivier Ligot, Jens Bendisposto, Michael Leuschel. Debugging Event-B Models using the ProB Disprover Plug-in. AFADL 2007.]
| + | == Rodin Developer FAQ == |
| | | | |
| − | === Inspection of Alternate Approaches ===
| + | see [[FAQ]]. |
| | | | |
| − | ProB is a model checker for high-level B and Event-B models based on constraint-solving. In this paper we investigate alternate approaches for validating high-level B models using alternative techniques and tools based on using BDDs, SAT-solving and SMT-solving. In particular, we examine whether ProB can be complemented or even supplanted by using one of the tools BDDBDDB, Kodkod or SAL.
| + | [[Category:Developer documentation]] |
| − | | + | [[Category:Rodin Platform]] |
| − | [http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=249 Daniel Plagge, Michael Leuschel, Ilya Lopatkin, Alexander Romanovsk. SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook. AFM'09.] | |
| − | | |
| − | === Validation of ProB ===
| |
| − | | |
| − | Symmetry reduction is a model checking technique that can help alleviate the problem of state space explosion, by preventing redundant state space exploration. In previous work, we have developed three effective approaches to symmetry reduction for B that have been implemented into the ProB model checker, and we have proved the soundness of our state symmetries. However, it is also important to show our techniques are sound with respect to standard model checking, at the algorithmic level. In this paper, we present a retrospective B development that addresses this issue through a series of B refinements. This work also demonstrates the valuable insights into a system that can be gained through formal modelling.
| |
| − | | |
| − | [http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=257 Edd Turner, Michael Butler, Michael Leuschel. A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking. ABZ'2010.] | |
| − | | |
| − | | |
| − | === B-Motion Studio ===
| |
| − | | |
| − | B-Motion Studio provides a way to quickly generate domain specific visualisations for a formal model, enabling domain experts and managers to understand and validate the model. We also believe that our tool will be of use when teaching formal methods, both during lectures as a way to motivate students to write their own formal models.
| |
| − | | |
| − | [http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=258 Lukas Ladenberger, Jens Bendisposto, Michael Leuschel. Visualising Event-B models with B-Motion Studio. FMICS'2009.]
| |
| − | | |
| − | = Planning =
| |
| − | This paragraph shall give a timeline and current status (as of 29 Jan 2010).
| |
| − | | |
| − | === Model-based Testing ===
| |
| − | | |
| − | * Directed Model Checking to achieve coverage (Deploy extension; Flow Graphs)
| |
| − | * Integrate Algorithm into Rodin
| |
| − | * Make Algorithm more generic
| |
| − | * Top-down multi-level animation
| |
| − | * Move from prototype to real product
| |
| − | | |
| − | === B-Motion Studio ===
| |
| − | | |
| − | * Experiment with existing Flash animation and B model of ClearSy
| |
| − | * Improve usability, more widgets
| |
| − | | |
| − | === Validation of ProB ===
| |
| − | | |
| − | * Test coverage analysis for Prolog code
| |
| − | * Validation Document to be delivered to Siemens
| |
| − | | |
| − | === Scalability ===
| |
| − | | |
| − | * More experiments with SAT, SMT, BDD techniques
| |
| − | | |
| − | * Integration of Kodkod into ProB for solving complicated predicates over first order relations and simple sets
| |
| − | | |
| − | === Usability ===
| |
| − | * Feedback errors found by ProB into the PO view (as red icons)
| |
| − | * Improve Disprover, detect when it is a decision procedure
| |
| − | * Further improvments to GUI: 2-D Viewer, better multi-level animation view
| |
