Ridha Khedri
Dipl.Eng., M.Sc., Ph.D., P.Eng
Professor, McMaster University
Additional Technical Material (A Case Study of Modular Modeling of Hybrid System Using Event-B)
- An Event-B Specification of a paper hybrid press (Full Rodin Development).
- The whole Event-B models of insulin pump system
- The Controller model composed with the discrete subsystems of Basal, Normal, and Square/Dual orderly
The model of the Belt example in the paper “Modeling of Timing Constraints in Hybrid Systems Using Event-B” can be downloaded in this website.
In the Theory plugin of the Rodin platform, the operators are rewritten, such as summarize are rewritten as sum (x:”Real”, y:”Real”):”Real”. Therefore, complex functions of the systems are not easy to read. To simplify for readers, in this showing example, we write the basic operators of real numbers the same as the operators of Nature numbers in the Rodin platform.