Search results
From Event-B
Jump to navigationJump to searchCreate the page "Event-B Language)" on this wiki! See also the search results found.
- === 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 structur7 KB (1,009 words) - 10:59, 26 January 2011
- ...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 mat4 KB (642 words) - 08:33, 29 June 2012
- === 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 structur6 KB (989 words) - 10:43, 10 December 2010
- * 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
- ...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 systems12 KB (1,818 words) - 08:31, 20 April 2012
- 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
- ...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 plug7 KB (1,095 words) - 14:40, 21 December 2010
- ...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
- 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 th4 KB (596 words) - 13:21, 18 July 2012
- ...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 simp9 KB (1,382 words) - 11:05, 27 January 2011
- [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 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
- ....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
- |Ensure Event-B handbook consistency |Enrich SMT support for Event-B mathematical language4 KB (584 words) - 09:50, 12 September 2013
- * 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
- ...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 and11 KB (1,725 words) - 18:07, 7 December 2009
- ...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 selected12 KB (1,741 words) - 08:25, 14 December 2010
- ...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 the15 KB (2,298 words) - 15:08, 27 January 2011
- ...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-machi4 KB (659 words) - 09:47, 17 May 2012
- * 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 (296 words) - 14:27, 6 November 2014
