Outstanding Tooling Issues

From Event-B
Jump to navigationJump to search

TODO list:

  • As a result of the decomposition process, the tool can produce a remote event, without a corresponding local event. A local event, with no guards and skip action, must be added manually to the tasking machine, and composed machine in order to facilitate code generation. This relates to an implementation with a subroutine call, where there are no parameters passed, and no local updates i.e. remote updates only. The addition of the 'dummy' event will be automated in a pre-processing step in the near future. It is not necessary to have a dummy remote event if a remote event does not exist.
  • Flattening of Composition Machines, and Machines at the Implementation level, composed machine refinement.
  • Addition of Addressed Variables