Search results

Create the page "Modelling User Interface" on this wiki! See also the search results found.

• Rodin Plug-ins
  === Modelling === * [[CamilleX]] (formerly XEvent-B) with support for text editors and modelling mechanisms such as ''machine inclusion''.
  5 KB (757 words) - 16:19, 13 February 2020
• Modularisation Plug-in Tutorial
  ...just the pressure in the sluice area and control the door locks to allow a user to get safely inside to outside. Such system can be deployed, for example, # the system allows a user to get inside or outside by leveling pressure between room and a destinatio
  8 KB (1,166 words) - 20:58, 10 November 2009
• Undo Redo
  ...e Rodin platform editor, users do not modify a text file but a database of modelling elements. However, the implementation shall reuse any available Eclipse mec ...chanism is based on a history that records all operations performed by the user. The implementation must also provide controls such as a configuration par
  4 KB (599 words) - 15:56, 28 January 2009
• D23 Decomposition
  ...arallel system and the ''shared events'' approach seems more suitable when modelling message-passing distributed systems. Choices, either related to the plug-in core or to the plug-in graphical user interface, have been made with the following constraints in mind:
  6 KB (825 words) - 13:27, 27 January 2010
• UML-B Integration and Improvements
  ...tate machine modelling but also provides visualisation of existing Event-B modelling concepts. UML-B is similar to UML but is a new notation with its own meta-m ...technologies used for Event-B (bespoke data repository) and UML-B (Eclipse Modelling Framework (EMF)). <nowiki>"The EMF project is a modeling framework and code
  5 KB (738 words) - 09:13, 4 March 2009
• D32 UML-B
  :# Functional enhancements to modelling ...onceptual Singleton classes - provides a conceptual grouping of associated modelling elements without generating the lifting mechanisms of a class.
  9 KB (1,382 words) - 11:05, 27 January 2011
• Rodin Developer Support
  === Event-B User Interface === ...either [http://handbook.event-b.org/current/html/event_b_perspective.html modelling] in Event-B or [http://handbook.event-b.org/current/html/proving_perspectiv
  8 KB (1,260 words) - 12:45, 30 July 2015
• Tasking Event-B Overview for D32
  ...t of the interface that enables event synchronization. We make use of this interface and add information (see [[#Implementing Events]]) to facilitate code gener ...rce code. There is also a translator that constructs new machines/contexts modelling the implementation, and these should refine/extend the existing elements of
  7 KB (1,009 words) - 10:59, 26 January 2011
• ADVANCE D3.2 Language extension
  ...predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (proof extensions). ...ensions do not compromise the soundness of the existing infrastructure for modelling and proof. In essence, the Theory plug-in provides a systematic platform fo
  4 KB (642 words) - 08:33, 29 June 2012
• UML-B - Statemachine Animation
  ...n all the information in the animated Event-B machine and the normal Pro-B interface should be used in parallel with it. For example, some events may not be rep ...nt-B translator. Once this launch stage has completed, there is no further interface with UML-B during animation.
  7 KB (1,130 words) - 14:39, 28 January 2010
• Tasking Event B Overview
  ...t of the interface that enables event synchronization. We make use of this interface and add information (see [[#Implementing Events]]) to facilitate code gener A Tasking Development is generated programmatically, at the direction of the user; the Tasking Development consists of a number of machines (and perhaps asso
  6 KB (989 words) - 10:43, 10 December 2010
• Rodin Platform 3.0 Release Notes
  === General Interface === ==== Modelling ====
  8 KB (1,195 words) - 16:35, 9 July 2014
• Current Developments
  The efforts in [[Düsseldorf]] ([[User:Fabian|Fabian]]) and [[Newcastle]] ([[User:Alexei|Alexei]]) have been joined to create a single text editor which will ...opment (that is, another module). The plug-in follows an approach where an interface is characterised by a list of operations specifying the services provided b
  12 KB (1,869 words) - 16:35, 18 March 2014
• Development of a Heating Controller System
  ...commended methodological aspects of Event-B, particularly those aspects of modelling concerned with decomposition and code generation. ...put and output parameters. At the top there are two buttons that allow the user to increase/decrease '''Target Temperature'''. The target temperature perio
  7 KB (1,119 words) - 10:06, 12 May 2011
• D32 Mathematical Extensions
  ...predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (prover extensions). ...ies are deployed to the current workspace (i.e., Workspace Scope), and the user can use any defined extensions in any project within the workspace.
  7 KB (1,095 words) - 14:40, 21 December 2010
• Past Developments
  ...a model can be tagged as generated by a tool, in order to prevent the end-user from directly editing them (and their descendants). ...ork includes an EMF representation of Event-B, a synchronising persistence interface for loading and saving models via the Rodin API and facilities to support t
  6 KB (915 words) - 16:57, 27 February 2014
• Tasking Event-B Overview
  ...t of the interface that enables event synchronization. We make use of this interface and add information (see [[#Implementing Events]]) to facilitate code gener ...uce a remote event, without a corresponding local event. This happens when modelling a task that updates a (remote) shared machine, but does not pass any parame
  9 KB (1,528 words) - 08:43, 2 September 2013
• ADVANCE D3.2 General Platform Maintenance
  ...e need to be productive using Event-B and minimize the access to an expert user. It is continuously maintained by the various actors involved in the envir ...video tutorials about the use of the platform.<ref>http://www.youtube.com/user/EventBTv</ref>
  20 KB (3,030 words) - 13:18, 18 July 2012
• ADVANCE D3.3 General Platform Maintenance
  ...nt of external plug-ins by providing easier to use Application Programming Interface (API). Thus, releases 2.7 and 2.8 mainly contain bug fixes and small improv ...a few buttons outside the editing area. This enhancement originated from a user who has contributed a patch for it. The stability of the newer generic Rodi
  16 KB (2,554 words) - 14:05, 8 October 2013
• Google Summer of Code 2009
  ...lling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstracti Reusing formal models in order to reduce the effort of modelling and proving is an important aspect of the Event-B method. The background th
  10 KB (1,629 words) - 12:50, 12 August 2009
• Rodin Platform 2.0 Release Notes
  * General Interface * Modelling
  15 KB (2,008 words) - 15:34, 10 January 2011
• D45 General Platform Maintenance
  ...long predicates (e.g. long goals). Since Rodin 2.2, and its new Proving UI interface, a feature has been added, allowing to search and highlight a string patter ...been provided in such case, taking the form of warnings or errors that any user can understand and review.
  35 KB (5,228 words) - 10:12, 23 April 2012
• D32 Code generation
  ...t of the interface that enables event synchronization. We make use of this interface and add information (see Events<ref name="taskext">http://wiki.event-b.org/ A Tasking Development is generated programmatically, at the direction of the user; the Tasking Development consists of a number of machines (and perhaps asso
  15 KB (2,298 words) - 15:08, 27 January 2011
• Records Extension
  This page is under development. It is intended to be a user oriented manual for using records in Event-B. This page should be read in c The Records Extension introduces a new modelling construct to provide a notion of structured types in Event-B Contexts.
  8 KB (1,347 words) - 13:07, 21 July 2010
• Code Generation Activity
  ...neration for Functional Mock-up Units, for use with the Functional Mock-up Interface (FMI) standard. Tasking Event-B is an extension to Event-B, for defining co ...ar style of C, which is tailored for use with ADVANCE's Functional Mock-up Interface ([http://eprints.soton.ac.uk/365249/1/rms.pdf FMI]) approach. To generate c
  17 KB (2,568 words) - 09:03, 19 October 2015
• D45 Scalability
  ...rience. The whole performance was enhanced by core implementation and user interface refactorings. Improvements made to the proving experience will be detailed This section concerns the actual editors that user work with to view and modify models.
  13 KB (1,991 words) - 20:57, 20 April 2012
• Event Model Decomposition
  ...contain contexts, machines, or both (see [[Event-B Modelling Language|the modelling language]]). The notion of model decomposition covers on the one hand the m ...ied from the non-decomposed machine to a sub-machine, according to the end-user specified distribution (by opposition to ''external'' event).
  43 KB (6,950 words) - 09:48, 27 October 2011
• Rodin Platform 2.3 Release Notes
  * General Interface * Modelling
  11 KB (1,401 words) - 09:39, 8 November 2011
• Statemachine Animation Tutorial
  *UML-B Modelling Environment plug-in ...en actions are made on the diagram elements. In other words it works as an interface between the UML-B and ProB, delivering the existing functionality of ProB t
  13 KB (2,247 words) - 18:16, 13 January 2010
• D45 Code Generation
  ..."Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2012) Formal modelling for Ada implementations: tasking Event-B. In, Ada-Europe 2012: 17th Interna ...de generator on 22-03-2012. The changes were made to the methodology, user interface, and tooling. The first version of the code generator supported translation
  12 KB (1,818 words) - 08:31, 20 April 2012
• Rodin Platform 1.3 Release Notes
  * General Interface * Modelling
  12 KB (1,642 words) - 13:21, 28 July 2010