A case study on automotive cruise control originally done in (conventional, discrete) Event-B is reexamined in Hybrid Event-B (an extension of Event-B that includes provision for continuously varying behaviour as well as the usual discrete changes of state). A significant case study such as this has various benefits. It can confirm that the Hybrid Event-B design allows appropriately fluent application level modelling (as is needed for serious industrial use). It also permits a critical comparison to be made between purely discrete and genuinely hybrid modelling. The latter enables application requirements to be covered in a more natural way. It also enables some inconvenient modelling metaphors to be eliminated.
展开▼
