A cyber-physical system (CPS) is a device controlled by computer algorithms, integrated with users and the internet. However, when it comes to modelling and verification, many such devices pose a significant challenge. This is due to the differing branches of mathematics which are used for modelling the various disciplines that contribute to a typical CPS. Secondly, the complexity inherent in large computer systems can create a challenge for any verification approach.
In response to this issue, a team of researchers from The University of Manchester’s School of Computer Science have developed Hybrid Event-B - a clean extension of the popular Event-B modelling and verification framework for discrete events. The new Hybrid Event-B system was designed to accommodate the additional demands of continuously varying state change in a mathematically compatible way.
To test the efficacy of the new system, the team carried out a case study based on the control of a set of aircraft landing gear. The set-up comprised many interdependent components, thus providing an excellent vehicle for exercising the multi-machine and coordination capabilities of the Hybrid Event-B modelling formalism. The implementation of the system in the nominal regime was achieved via a series of formal Hybrid Event-B refinements, and is connected to a development that tolerates various failure modes, via formal retrenchments, in a structured way.
It is anticipated that the Hybrid Event-B modelling system will have many useful applications in the near future - particularly in industries that extensively utilise complex multi-machine setups (i.e. aerospace, engineering, manufacturing, etc.).