Lindahl98
Lindahl et al. [1] performed a case study with the UPPAAL tool back in 1998. They modelled a gear controller with an interface and a gear controller and its environment, consisting of an engine, clutch and gearbox. A formal description of the system can be found in their paper.
With only images of the UPPAAL model available, we re-modelled the system as specified. The Interface automaton that was given only represents the gear change from gear 1 to gear 2. The other automatons' initial states suggest that the process would start with a gear 0. To start with gear 1, we adjusted the system: Since the Interface wants to change gear from first to second gear, it is safe to assume that the car is already driving forwards. This results in the engine delivering torque through the gearbox. Therefore we conclude that the Engine should start initially in state Torque. When the gear is set to 1, the gearbox should not start in Neutral, but instead in state Idle. With the resulting model we could perform various simulations of the specified behaviour. Furthermore we added a gear change from gear 2 back to gear 1 in order to create a loop.
Clutch
Engine
Gearbox
Gear Control
Interface
In the paper, a total of 14 requirements were specified that the authors state were validated with UPPAAL.
Our approach can only handle information encoded in states, i.e., a specific state should hold at a specific point in the execution. However, properties (1)-(2), (7)-(10) and (14) specify an implication which cannot be expressed with the pattern catalogue which is the foundation of our approach. Furthermore, the possibility expressed in (13) cannot be specified with a pattern of the catalogue. Therefore, we concluded that our approach is only applicable to properties (3)-(6).
(3)
The specified requirement was: Clutch.ErrorClose ->[<=200] GearControl.CCloseError We used the Response pattern with the globally scope with P being Clutch.ErrorClose, S being GearControl.CCloseError and since this requirement specifies a time bound, t1=0 and t2=200.
The states Clutch.ErrorClose_ENTER and GearControl.CCloseError_ENTER were added and the transitions altered as described here.
The property is satisfied, verification took 0.005s. 5 states and transitions were added automatically in 0.630s.
(4)
The specified requirement was: Clutch.ErrorOpen ->[<=200] GearControl.COpenError We used the Response pattern with the globally scope with P being Clutch.ErrorOpen, S being GearControl.CCOpenError and since this requirement specifies a time bound, t1=0 and t2=200.
The states Clutch.ErrorOpen_ENTER and GearControl.COpenError_ENTER were added and the transitions altered as described above.
The property is satisfied, verification took 0.002s. 5 states and transitions were added automatically in 0.783s.
(5)
The specified requirement was: Gearbox.ErrorIdle ->[<=350] GearControl.GSetError We used the Response pattern with the globally scope with P being Gearbox.ErrorIdle, S being GearControl.GSetError and since this requirement specifies a time bound, t1=0 and t2=350.
The states Gearbox.ErrorIdle_ENTER and GearControl.GSetError_ENTER were added and the transitions altered as described above.
The property is satisfied, verification took 0.004s. 5 states and transitions were added automatically in 0.731s.
(6)
The specified requirement was: Gearbox.ErrorNeu ->[<=200] GearControl.GNeuError We used the Response pattern with the globally scope with P being Gearbox.ErrorNeu, S being GearControl.GNeuError and since this requirement specifies a time bound, t1=0 and t2=200.
The states Gearbox.ErrorNeu_ENTER and GearControl.GNeuError_ENTER were added and the transitions altered as described above.
The property is satisfied, verification took 0.003s. 5 states and transitions were added automatically in 0.705s.
[1]: LINDAHL, Magnus; PETTERSSON, Paul; YI, Wang. Formal design and analysis of a gear controller: An industrial case study using uppaal. In: LNCS, Proc. of the 4th International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. 1998. S. 281-297.
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.43.1194&rep=rep1&type=pdf