Modelling with UML-B State-machine Diagrams - Aircraft Engines

Problem

An aircraft has one or more engines. Each engine has 3 possible electrical power sources: An engine alternator which is only available when the engine is running, an airframe APU which must be used during starting, an airframe battery which is only sufficient to power electronic systems and to start the APU. Engine start/run sequence: When the engine is not running it is either stood or being started. To start the engine, it is motored by an electrical starter motor until ‘lightoff’ is achieved. If lightoff is not achieved, the engine must be purged to remove unburnt fuel before it is returned to the stood state. If lightoff is achieved, the engine reaches ground idle and can be accelerated to flight idle. The engine must be returned to ground idle before it is shut off. To avoid damaging the alternator, power should be switched back to battery before shutting off the engine. Model this system using UML-B state-machines . Use hierarchically nested state-machines where appropriate. Where possible, add invariants to states to test the guards are correct and sufficient. Animate the state-machines using Pro-B and run the model checker to detect any invariant violations

Solution

Example of UML-B State-machines - Aircraft Engines

Tips

A Class can be linked to a corresponding ClassType by setting the 'Instances' property of the Class to the ClassType.

The key combo for the 'dot' operator used in predicates and actions of a class is ,. (i.e. comma+stop)