Search results

From Event-B
Jump to navigationJump to search

Create the page "Event-B Language)" on this wiki! See also the search results found.

Page title matches

  • Event-B Language
    == Book: Modeling in Event-B: System and Software Engineering by Jean-Raymond Abrial == The Event-B introduced in Abrial's book in some ways differs from the Event-B implemented by Rodin.
    3 KB (351 words) - 11:30, 23 January 2014
  • Event-B Mathematical Language
    ...s a brief summary of documents describing Event-B's logic aka mathematical language. [http://handbook.event-b.org/current/html/mathematical_notation.html Rodin Handbook (Mathematical No
    1 KB (203 words) - 11:28, 23 January 2014
  • Event-B Modelling Language
    This page gives a brief summary of documents describing Event-B's modeling notation. [http://handbook.event-b.org/current/html/modeling_notation.html Rodin Handbook (Modeling Notation)]
    410 bytes (54 words) - 08:45, 27 October 2011
  • Language of an Event-B Component
    ...0, Event-B components can use extended version of the Event-B mathematical language. This change was implemented then, but there were some places where strange ...e to parse them back to a tree in memory. Conversely, the serialization of Event-B formulas need to know how to transform the tree in memory into a character
    4 KB (692 words) - 15:06, 20 November 2013
  • Changes to the Mathematical Language of Event-B
    ....0.0. See [[Event-B_Mathematical_Language]] for a full description of the language. [[Category:Event-B]]
    3 KB (469 words) - 12:38, 17 April 2009

Page text matches

  • Event-B Language
    == Book: Modeling in Event-B: System and Software Engineering by Jean-Raymond Abrial == The Event-B introduced in Abrial's book in some ways differs from the Event-B implemented by Rodin.
    3 KB (351 words) - 11:30, 23 January 2014
  • Mathieu/Main Page
    == Event-B and Rodin Documentation Wiki == [[Event-B Language]]
    295 bytes (39 words) - 22:09, 4 July 2008
  • Event-B Mathematical Language
    ...s a brief summary of documents describing Event-B's logic aka mathematical language. [http://handbook.event-b.org/current/html/mathematical_notation.html Rodin Handbook (Mathematical No
    1 KB (203 words) - 11:28, 23 January 2014
  • How Rodin Deviates from Abrial's Book
    ...(some) differences between the version of Event-B described in [http://www.event-b.org/abook.html Abrial's book] and the version implemented by Rodin. One may understand from Chapter 9 that Event-B is based on naive set theory, and therefore has terms like <math>\{X | X \n
    1 KB (188 words) - 11:10, 25 January 2012
  • Constrained Dynamic Lexer
    ...eterizable lexical analyser''' (i.e. lexer) for the [[Event-B Mathematical Language]]. In order to be usable, [[mathematical extensions]] require that the Event-B
    3 KB (440 words) - 09:10, 1 March 2010
  • Language of an Event-B Component
    ...0, Event-B components can use extended version of the Event-B mathematical language. This change was implemented then, but there were some places where strange ...e to parse them back to a tree in memory. Conversely, the serialization of Event-B formulas need to know how to transform the tree in memory into a character
    4 KB (692 words) - 15:06, 20 November 2013
  • Rodin Plug-ins
    * [[Records_Extension|Records]] provide structured types for Event-B. * [[UML-B]] provides a 'UML-like' graphical front end for Event-B.
    5 KB (757 words) - 16:19, 13 February 2020
  • Event-B to SMT-LIB
    The need for translating the Event-B language to the SMT-LIB language was introduced by the [http://decert.gforge.inria.fr/index.html DECERT] pro ...e translation of Event-B language into the veriT extensions of the SMT-LIB language. It comes down to running a direct syntactic translation when the formula d
    5 KB (797 words) - 10:29, 24 October 2011
  • D23 Introduction
    .... The tool documentation is provided within the Event-B wiki ([http://wiki.event-b.org]). * Model animation and testing, to validate Event-B models. More precisely, the ProB or AnimB plug-ins allow a domain expert to
    3 KB (399 words) - 11:20, 27 January 2010
  • ADVANCE D3.3 Language extension
    ...vide the Rodin user with a way to extend the standard Event-B mathematical language by supporting user-defined operators, basic predicates and algebraic types. ...other things, a user-friendly mechanism to extend the Event-B mathematical language as well as the prover. A theory is the dedicated component used to hold mat
    4 KB (648 words) - 14:52, 7 October 2013
  • Rewriting rules for event model decomposition
    ...first necessary to introduce some equivalence and simplification rules on Event-B assignments and predicates. These rules will then help to understand the tr ...an equivalence relation on the Event-B actions, and by restriction on the Event-B assignments. Two actions are considered as being equivalent if the proof ob
    10 KB (1,604 words) - 09:19, 27 October 2011
  • Past Developments
    ==== Mathematical Language V2 ==== [[Changes to the Mathematical Language of Event-B]] and the corresponding [[Mathematical_Language_Evolution_Design|design]] d
    6 KB (915 words) - 16:57, 27 February 2014
  • D23 Flow Plug-in
    ...traint on event ordering must be such that the overall specification is an Event-B refinement of the original model. Importantly, this means that all the desi There are a number of reasons to consider an extension of Event-B with an event ordering mechanism:
    4 KB (609 words) - 11:37, 8 January 2010
  • Tasking Event-B Overview for D32
    === Tasking Event-B for D32 === Tasking Event-B can be viewed as an extension of the existing Event-B language. We use the existing approaches of refinement and decomposition to structur
    7 KB (1,009 words) - 10:59, 26 January 2011
  • ADVANCE D3.2 Language extension
    ...vide the Rodin user with a way to extend the standard Event-B mathematical language by supporting user-defined operators, basic predicates and algebraic types. ...other things, a user-friendly mechanism to extend the Event-B mathematical language as well as the prover. A theory is the dedicated component used to hold mat
    4 KB (642 words) - 08:33, 29 June 2012
  • Tasking Event B Overview
    === Tasking Event-B === Tasking Event-B can be viewed as an extension of the existing Event-B language. We use the existing approaches of refinement and decomposition to structur
    6 KB (989 words) - 10:43, 10 December 2010
  • D23 General Platform Maintenance
    * Mathematical Language V2 (releases 1.0 and upper) : The new version of the mathematical language is supported.
    7 KB (963 words) - 11:30, 27 January 2010
  • D45 Code Generation
    ...ation of code for typical real-time embedded control software from refined Event-B models. Such a feature will be an important factor in ensuring eventual dep ...roject, work has been undertaken to investigate automatic generation, from Event-B models, for these type of systems
    12 KB (1,818 words) - 08:31, 20 April 2012
  • Theory Plug-in
    The Theory plug-in provides capabilities to extend the Event-B language and the proving infrastructure in a familiar fashion to Rodin users. This p ...clude the sequence operator (which was present in classical B mathematical language) and the bag operator.
    7 KB (958 words) - 14:53, 14 June 2021
  • D32 Mathematical Extensions
    ...vide the Rodin user with a way to extend the standard Event-B mathematical language by supporting user-defined operators, basic predicates and algebraic types. ...define their custom reusable types, that are treated underline by Rodin as Event-B constant sets and relations, supported by additional axioms, which the plug
    7 KB (1,095 words) - 14:40, 21 December 2010
  • Development of a flash-based filestore
    ...s system was chosen as a case study for our experiments, carried out using Event-B and the Rodin tool. The experiments were aimed at developing a rigorous mod ...ental Refinement Approach to a Development of a Flash-Based File System in Event-B===
    4 KB (656 words) - 13:06, 18 November 2010
  • ADVANCE D3.2 Improvement of automated proof
    In an Event-B development, more than 60% of the time is spent on proofs. That explains wh ...of a modified model. The translation of Event-B language into the SMT-LIB language is the main issue of this integration. Two approaches were developed for th
    4 KB (596 words) - 13:21, 18 July 2012
  • D32 UML-B
    ...hat provides an alternative to UML-B which is more closely integrated with Event-B. ...provide a means of visualising the animation and model-checking process of Event-B machines modelled in UML-B tool, in particular state-machines, thus to simp
    9 KB (1,382 words) - 11:05, 27 January 2011
  • Rodin Workshop 2009
    [http://wiki.event-b.org/images/Rodin_plug-in_tutorial_2009-07-15.pdf Rodin Plug-in Development * Michael Butler, [http://wiki.event-b.org/images/Intro.pdf Introduction]
    5 KB (766 words) - 09:59, 21 September 2011
  • Tasking Event-B Tutorial
    === Tasking Event-B Tutorial Overview === This tutorial follows on from the abstract development described [http://wiki.event-b.org/index.php/Development_of_a_Heating_Controller_System here].
    11 KB (1,714 words) - 12:41, 2 September 2013
  • Changes to the Mathematical Language of Event-B
    ....0.0. See [[Event-B_Mathematical_Language]] for a full description of the language. [[Category:Event-B]]
    3 KB (469 words) - 12:38, 17 April 2009
  • Tool Development Roadmap
    |Ensure Event-B handbook consistency |Enrich SMT support for Event-B mathematical language
    4 KB (584 words) - 09:50, 12 September 2013
  • Measurement Plug-In
    * provide feedback to the user about the quality of the Event-B model he is building and about potential problems in it or in the way he is ...omings (usability, prover), modelling issues (to be addressed by training, language, tool evolution,...), etc.
    2 KB (308 words) - 16:35, 17 December 2008
  • D23 Code Generation
    ...g, it became clear that having support for generation of code from refined Event-B models would be an important factor in ensuring eventual deployment of the * Enrich Event-B with explicit algorithmic structures for use in later refinement stages and
    11 KB (1,725 words) - 18:07, 7 December 2009
  • Code Generation Tutorial
    ...source code, which uses the common language model. An overview of Tasking Event-B can be found on the [[Tasking_Event-B_Overview]] page. ...tep to implementation, by extending Event-B with the necessary constructs. Event-B machines that are to be implemented (and their seen Contexts) are selected
    12 KB (1,741 words) - 08:25, 14 December 2010
  • D32 Code generation
    ...he commonalities between their flow plug-in <ref name = "flow">http://wiki.event-b.org/index.php/Flows</ref> and the flow control structures used in our appro ...>. It had been recognised that support for generation of code from refined Event-B models would be an important factor in ensuring eventual deployment of the
    15 KB (2,298 words) - 15:08, 27 January 2011
  • State-Machines and Code Generation
    ...ed; that is, nothing over and above the usual mark-up required for Tasking Event-B, such as identifying non-typing/typing invariants, and guards etc. State-ma ...e should be able to apply decomposition techniques to decompose the single Event-B machine with state-machines into a number of machines, with the state-machi
    4 KB (659 words) - 09:47, 17 May 2012
  • D23 UML-B
    ...B relies on an EMF representation of Event-B. The development of a new EMF Event-B plugin-in feature is also described in this section. This feature was initi ...us animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diag
    8 KB (1,224 words) - 15:53, 28 January 2010
  • Old Flow Plug in page
    ...aining of event ordering must be such that the overall specification is an Event-B refinement of the original model. Importantly, this means that all the desi How expressive is the language of flows? There is, effectively, just one construct but it already covers a
    11 KB (1,869 words) - 23:48, 21 January 2011
  • ADVANCE D3.3 Introduction
    * the Event-B wiki,<ref name="EventB_wiki">http://wiki.event-b.org</ref> * the Rodin Handbook.<ref name="Rodin_handbook_Page">http://handbook.event-b.org</ref>
    2 KB (325 words) - 17:32, 29 November 2013
  • Extending the Rodin Pretty Print Page (How to extend Rodin Tutorial)
    ...din_Event-B_Explorer_(How_to_extend_Rodin_Tutorial)|Adding elements to the Event-B explorer]]| Next=[[Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tut ...ariant expressions. There are many pre-defined CSS classes for the Event-B language elements. To review them, go to the file <tt>html/style.css</tt> in the plu
    4 KB (567 words) - 12:27, 25 August 2010
  • Rodin Keyboard User Guide
    The Rodin Keyboard plug-in creates a view (namely "Rodin Keyboard") under Event-B category. # Choose the "Rodin Keyboard" view from the Event-B category.
    14 KB (1,930 words) - 12:58, 21 July 2010
  • Event-B Examples
    This page is for listing available example Event-B/Rodin projects. This material describes an Event-B development of a Vehicle On-Board Controller for trains.
    9 KB (1,283 words) - 13:58, 5 July 2017
  • Code Generation Activity
    ...or defining concurrent systems sharing data, for details see the [[Tasking Event-B Overview]] page. Other code generation approaches that are available for Event-B include:
    17 KB (2,568 words) - 09:03, 19 October 2015
  • Mathematical Language Evolution Design
    ...ocument describes the modifications that occur to the Event-B mathematical language from the developer point of view. The old language will still be recognized, in order to provide backward compatibility.
    14 KB (2,104 words) - 09:40, 11 May 2009
  • D23 Rule-based Prover
    ...tactic. Therefore, a certain level of competence with the Java programming language as well as knowledge of Rodin architecture is necessary. ...Java code, and covers most of the rewrite rules available in [http://wiki.event-b.org/index.php/All_Rewrite_Rules]
    5 KB (796 words) - 11:44, 8 January 2010
  • Introduction (How to extend Rodin Tutorial)
    ...ou have basic knowledge in Event-B, and are familiar with Java programming language.<br> ...odin Event-B Explorer (How to extend Rodin Tutorial) | Extending the Rodin Event-B Explorer]]" of this tutorial.
    5 KB (825 words) - 17:03, 16 October 2010
  • ADVANCE Deliverable D3.3
    ...ts made in the area of the mathematical language and other planned Event-B language extensions * See §4 of [http://wiki.event-b.org/images/Llncsdoc.pdf How to Edit Your Input File] for LLNCS formatting r
    6 KB (830 words) - 13:21, 7 October 2013
  • Transformation patterns
    .../www.eclipse.org/gmt/epsilon/doc/eol/ EOL] (simple object-based imperative language) and easily run them over models within the same project. Editing is done i ...the transformations, and provides a simple library handling user input of Event-B elements such as machines, events, variables etc.
    7 KB (1,011 words) - 13:08, 1 July 2013
  • ADVANCE D3.3 Model Checking
    ...lication/PlaggeLeuschel_Kodkod2012</ref> we described a translation from B/Event-B to Kodkod where we applied the translation to improve We have now applied the technique to check theories of a context in Event-B, check assertions in classical B and to the constraint-based invariant chec
    6 KB (1,016 words) - 10:41, 23 September 2013
  • Modularisation Integration Issues
    ...nchecked machine). Statically checked components are generated to be plain Event-B. ...l) and contexts are used as a lingua franca for plugins extending the core language and also for the plugins analysing and manipulating models. There should be
    3 KB (518 words) - 11:34, 6 September 2010
  • D23 TEXT
    As an Event-B model consists of text, users were requesting a text editor, which would al ...ammar had to be carefully designed to be able to parse the structure of an Event-B model independently of the content of the predicates, expressions and actio
    8 KB (1,257 words) - 15:56, 28 January 2010
  • Rodin 3.0 Plug-in Migration Guide
    of language versions obsolete: references to the <tt>LanguageVersion</tt> language and therefore built by the same factory. If you are in a special
    17 KB (2,614 words) - 16:25, 14 February 2014
  • ADVANCE D3.3 General Platform Maintenance
    ...engthen the way mathematical extensions could be added to the mathematical language to ensure that proofs are always sound. Concerning model editors, we have improved readability in Event-B editor by moving a few buttons outside the editing area. This enhancement o
    16 KB (2,554 words) - 14:05, 8 October 2013
  • ADVANCE D3.2 Introduction
    * the Event-B wiki,<ref name="EventB_wiki">http://wiki.event-b.org</ref> * the Rodin Handbook.<ref name="Rodin_handbook_Page">http://handbook.event-b.org</ref>
    2 KB (371 words) - 16:27, 13 July 2012
  • Tasking Event-B Overview
    === Tasking Event-B === Tasking Event-B can be viewed as an extension of the existing Event-B language. We use the existing approaches of refinement and decomposition to structur
    9 KB (1,528 words) - 08:43, 2 September 2013
  • Camille Editor
    <span style="color:#8B4513">Make sure to install the latest Event-B EMF Framework (version 3.7.0 or greater)!</span> ## If you didn't install the ''Event-B EMF Framework'' yet it will be automatically added. Confirm by clicking ''F
    6 KB (945 words) - 12:22, 27 January 2015
  • Records Extension
    ...elopment. It is intended to be a user oriented manual for using records in Event-B. This page should be read in conjunction with the [[Structured_Types|Struc The Event-B mathematical language currently does not support a syntax for the direct definition of structured
    8 KB (1,347 words) - 13:07, 21 July 2010
  • EMF framework for Event-B
    ...for extending the Event-B modelling language is available here: [[Generic Event-B EMF extensions]]. ...t-B generators. It will eventually replace the generator that only targets Event-B.
    26 KB (3,961 words) - 13:04, 19 May 2020
  • Event-B Statemachines
    ...atemachines Plug-in provides a way of adding state machines directly in to Event-B machines. The statemachines generate additional guards and actions which ar ...d GMF frameworks, Event-B EMF framework, Event-B EMF Extensions framework, Event-B diagrams framework and , for animation, ProB - all of these dependencies wi
    13 KB (2,134 words) - 08:04, 6 October 2015
  • D32 Provers
    ...external provers (PP, newPP, ML). Jann Röder carried out experiments using Event-B models from different domains and observed that his tactic significantly in ...ethodology for reasoning about the soundness of Event-B proof rules within Event-B. The document also allows users to look-up definitions of predefined operat
    11 KB (1,699 words) - 15:25, 27 January 2011
  • ADVANCE D3.2 General Platform Maintenance
    ...t as users wishes and requests were collected along. At the same time, the Event-B models and proof got bigger and bigger, in the same way as the experience o Release Notes<ref name="relNotes">http://wiki.event-b.org/index.php/Rodin_Platform_Releases</ref> and the SourceForge trackers<re
    20 KB (3,030 words) - 13:18, 18 July 2012
  • Current Developments
    For an overview of Tasking Event-B see [[Tasking Event-B Overview]]. ...ork for Event-B|EMF framework for Event-B]] (see that [[#EMF framework for Event-B|section]] for details).
    12 KB (1,869 words) - 16:35, 18 March 2014
  • Structured Types
    The Event-B mathematical language currently does not support a syntax for the direct definition of structured ...'invented' syntax for this (based on VDM syntax but currently not part of Event-B syntax):
    18 KB (2,643 words) - 12:41, 12 August 2009
  • Rodin Keyboard
    ...ho want to declare different "keyboards" corresponding to the mathematical language that they want to use. Moreover, different combinations can be used to ente * Standard keyboard for Event-B.
    9 KB (1,367 words) - 11:59, 23 June 2014
  • Constrained Dynamic Parser
    ...the requirements for a '''generic parser''' for the [[Event-B Mathematical Language]]. In order to be usable, [[mathematical extensions]] require that the Event-B
    27 KB (3,967 words) - 13:21, 15 February 2010
  • Event Model Decomposition
    One of the most important feature of the Event-B approach is the possibility to introduce new events during refinement steps ...ontexts, machines, or both (see [[Event-B Modelling Language|the modelling language]]). The notion of model decomposition covers on the one hand the machine de
    43 KB (6,950 words) - 09:48, 27 October 2011
  • Rodin Platform 1.1 Release Notes
    :A new extensible plug-in for the Event-B Keyboard is included. The former one, namely <tt>org.eventb.eventBKeyboard< # One in the plug-in <tt>org.eventb.keyboard</tt>, for standard Event-B notation translation.
    9 KB (1,298 words) - 10:06, 28 July 2010
  • Rodin Performances
    Taken from Jean-Raymond Abrial's book "Modeling in Event-B" A base string is made of all standard Event-B Mathematical Language symbols, separated from each other with a space character.
    7 KB (787 words) - 08:43, 17 June 2011
  • D23 ProB
    No new programming language has to be learned: the linking is described in B itself. ...in the SAP workpackage it became clear that test-case generation from the Event-B models is required for success.
    17 KB (2,580 words) - 15:55, 28 January 2010
  • Documentation Overhaul DoW
    ...011. The continuous build of the handbook can be found at http://handbook.event-b.org/ '''Deliverable:''' [http://handbook.event-b.org/review-1/html/sect0006.html A Guideline for content creators] and templ
    9 KB (1,421 words) - 12:41, 8 December 2011
  • D45 Prover Enhancement
    In an Event-B development, more than 60% of the time is spent on proofs. It has been a co ...of the ProB kernel. It is available from the ProB plugin after loading an Event-B model.
    21 KB (3,334 words) - 21:20, 20 April 2012
  • Extending the Pretty Print Page
    ...t Page of the [http://handbook.event-b.org/current/html/eventb_editor.html Event-B Editor] provides a rendered view of an edited machine or context, for an qu When contributing to the Event-B Editor, one uses the extension point <tt>org.eventb.ui.editorItems</tt>.
    17 KB (2,385 words) - 09:53, 27 October 2011
  • Rodin Platform 3.0 Release Notes
    Commands available from the Event-B explorer have been refactored and reorganized.<br/> The dependency on the Event-B UI plug-in has been removed by splitting text translation from translation
    8 KB (1,195 words) - 16:35, 9 July 2014
  • Rodin Platform 2.5 Release Notes
    ...This change is fully binary compatible, as stated in §13.4.21 of the Java Language Specification 3.0, as throws declaration are checked only at compile time. ...sion.StandardGroup'' that lists the syntactical groups in the mathematical language. Prefer referencing them instead of their ids as bare strings.
    11 KB (1,478 words) - 17:32, 2 May 2012
  • D45 General Platform Maintenance
    ...Documentation</ref> and the SourceForge<ref name=documentation>http://wiki.event-b.org/index.php/D45_General_Platform_Maintenance#Available_Documentation</ref ...were corresponding to previously identified needs (listed in [http://wiki.event-b.org/index.php/Category:D32_Deliverable D32 - Model Construction tools & Ana
    35 KB (5,228 words) - 10:12, 23 April 2012
  • Rodin Platform 2.7 Release Notes
    ...nts > Rodin). These settings allow you to modify the properties set on the Event-B Keyboard Text Font which is used in many views of the Proving UI. However, ...rp/files/DefaultAuto_ML800 DefaultAuto_ML800], then Window > Preferences > Event-B > Sequent Prover > Auto/Post Tactic > Profiles (tab) > Import..., point to
    10 KB (1,301 words) - 07:11, 29 August 2013
  • D32 Model Animation
    To support validation of Event-B models such as the ones generated by Bosch, this short coming had to be add ..."abz2010">S. Hallerstede, M. Leuschel, D. Plagge, Refinement-Animation for Event-B - Towards a Method of Validation, ASM'2010, LNCS 5977, Springer-Verlag, 201
    16 KB (2,553 words) - 15:12, 27 January 2011
  • Rodin Platform 2.6 Release Notes
    ...nts > Rodin). These settings allow you to modify the properties set on the Event-B Keyboard Text Font which is used in many views of the Proving UI. However, ...rp/files/DefaultAuto_ML800 DefaultAuto_ML800], then Window > Preferences > Event-B > Sequent Prover > Auto/Post Tactic > Profiles (tab) > Import..., point to
    10 KB (1,328 words) - 16:14, 3 August 2012
  • Rodin Proving Perspective
    ...r]]|Next= [[The_Mathematical_Language_(Rodin_User_Manual)|The Mathematical Language]]|Up= [[index_(Rodin_User_Manual)|User_Manual_index]]}} |([http://handbook.event-b.org Nightly Handbook Build])
    27 KB (4,348 words) - 08:56, 26 September 2011
  • The Proving Perspective (Rodin User Manual)
    ...r]]|Next= [[The_Mathematical_Language_(Rodin_User_Manual)|The Mathematical Language]]|Up= [[index_(Rodin_User_Manual)|User_Manual_index]]}} |([http://handbook.event-b.org Nightly Handbook Build])
    27 KB (4,348 words) - 18:45, 28 September 2011
  • Mathematical Extensions
    Currently the operators and basic predicates of the Event-B mathematical language supported by Rodin are fixed. ...oy-eprints.ecs.soton.ac.uk/216 ''Proposals for Mathematical Extensions for Event-B''], 2009.
    19 KB (2,883 words) - 18:20, 17 March 2014
Retrieved from ‘https://wiki.event-b.org/index.php/Special:Search’