Uncertainty Robustifier for Event-B Models

About

Uncertainty Robustifier is a plug-in of Rodin Platform, which is an IDE for the Event-B formal modeling method. This tool takes an Event-B model of a controller system as input, injects given perceptual uncertainty into the perception of plant’s values, and robustifies the controller against the uncertainty.

Details are explained in Kobayashi T., Salay R., Hasuo I., Czarnecki K., Ishikawa F., Katsumata S. (2021) Robustifying Controller Specifications of Cyber-Physical Systems Against Perceptual Uncertainty. In: Dutle A., Moscato M.M., Titolo L., Muñoz C.A., Perez I. (eds) NASA Formal Methods. NFM 2021. Lecture Notes in Computer Science, vol 12673. Springer, Cham. https://doi.org/10.1007/978-3-030-76384-8_13

uncertainty_robustifier_screenshot.png

Installation

  1. Download the archive of Rodin Platform version 3.5 (Linux, Mac OS, Windows) and unpack the archive. Please have a look at the release notes of Rodin platform for the platform-specific requirements.
  2. Select Help -> Install New Software....
  3. Press the Add... button to open the Add Repository menu.
  4. Enter Uncertainty Robustifier in Name and http://research.nii.ac.jp/robustifier/updates/ in Location, then press the Add button.
  5. Tick the checkbox of Uncertainty Robustifier in the list in the middle of the Install window.
  6. Press the Next button and follow the wizard to install.

Usage

  1. Prepare the target Event-B project. (We use A heater example in this document. Please download it and import it in a Rodin workspace.)
  2. Right-click the target machine in Event-B Explorer to open the context menu.
  3. Select Open With -> Uncertainty Handler to show the main interface.
  4. Expand Variables and tick variables that have perceptual uncertainty (e.g., temp).
  5. Expand Events and tick events of the controller’s behavior (e.g., ctrl_stay_safe, ctrl_heat, ctrl_cool).
  6. Press Generate robustified machine button on top.
  7. Fill the Predicate(s) column of the pop-up dialog with definitions of the perceptual uncertainty (e.g., temp_epsilon = (λ t · t ∈ ℤ ∣ t−3 ‥ t+3)) and press OK.
  8. You will find the robustified machine (e.g., heater_0_uncertainty_intolerant_injected) and the definition of perceptual uncertainty (e.g., heater_0_uncertainty_intolerant_uncertainty) in the Event-B Explorer.

Contact

Tsutomu Kobayashi (National Institute of Informatics) <t-kobayashi atmark nii.ac.jp>