Havelund97
Havelund et al. [1] performed a case study with the UPPAAL tool back in 1997. They modelled an audio/video protocol used by Bang & Olufsen with UPPAAL, the protocol was at the time actually in use, which makes it a real industry case study. The authors state that the version of the protocol they worked with had faults, but that B&O could not identify them. With their model though, they were able to locate the faults.
With only images of the UPPAAL model available, we re-modelled the system as specified.
Additionally, the provided models used variables to model interesting behaviour, instead of states. We therefore had to adapt the model by hand to make it applicable to our tool. We did this for every part of the requirement on its own as to not introduce too many changes into the model at once. Since our changes should not change the model's behaviour, all the changes could be made to a single model, but to enhance readability we discarded this approach.
Below are images of the models. The models shown display the A-Sender and the corresponding Frame Generator, Detector and Observer. Automatons for the B-Sender are included with the UPPAAL-model (except for the Observer).
The model contains an error which the hand-made observer from Havelund et al. can reveal. A fix that they provided in the paper can be found in the Fixed Frame Generator.
The protocol which was modelled works as follows: Senders A and B can send frames over a medium, if both send at the same time, a collision may occur. This has to be detected by the senders, that then fix the collision. The Frame Generator handles building the frames, i.e. each frame has to be ended with a T4 message, which has to be sent in order for the Frame Generator to reach the location last. The Detector automaton handles collisions, while the Sender handles timeouts, i.e. waiting to send a frame when the other sender has been detected to be sending.
Bus
Frame Generator
Fixed Frame Generator
Detector
Sender
Observer
A[] (A_eof == 1 imply A_diff == 0 and B_res == 0) is the original requirement. To handle this query more easily, we broke it down into three requirements: The first and second ones involve the A_diff == 0. In the paper, this variable is modified by the hand-made observer. There are exactly two instances when A_diff:=1: if at the point of the synchronisation of 'A_observe' A_Pf == 1 and A_S1 == 0 or if at that point A_Pn == 1 and A_S2 == 0 holds. A_diff cannot be reset to 0 at any point. So we decided to observe the transitions where A_diff:=1 could occur, the first one in (1.1), the second one in (1.2). Afterwards we looked at the second part of the requirement: A[] (A_eof == 1 imply B_res == 0). This is handled in (2).
We added states in between A_EOFReset and A_start in order to observe these two states, since in between these two states A_eof == 1 holds. These two states will be used for Q and R respectively for the scope.
(1) A[] (A_eof == 1 imply A_diff == 0)
(1.1) (right part of the observer provided in the paper)
Between Frame_Generator_A.start and Frame_Generator_A.EOFReset, if Sender_A.Failure has occurred, then in response Sender_A.Fail_Resolved eventually holds
scope: Between
Q=Frame_Generator_A.start
R=Frame_Generator_A.EOFReset
Pattern: Response
P=Sender_A.Failure
S=Sender_A.Fail_Resolved
(1.2) (left part of the observer provided in the paper)
Between Frame_Generator_A.start and Frame_Generator_A.EOFReset, if Sender_A.Failure has occurred, then in response Sender_A.Resolved eventually holds
scope: Between
Q=Frame_Generator_A.start
R=Frame_Generator_A.EOFReset
Pattern: Response
P=Sender_A.Failure
S=Sender_A.Resolved
(2) A[] (A_eof == 1 imply B_res == 0)
Here we hand-build an observer that checks the variable B_res. If it is set to 1, the observer can change its state (and does so in the verification, since UPPAAL tries to find a counter-example, which means the observer should be in state Failure as much as possible; hence we don't need to enforce the transition in this case).
Between Frame_Generator_A.start and Frame_Generator_A.EOFReset, if obs.Failure has occurred, then in response obs.Resolved eventually holds
scope: Between
Q=Frame_Generator_A.start
R=Frame_Generator_A.EOFReset
Pattern: Response
P=obs.Failure
S=obs.Resolved
(1.1)
Similarly to the observations stated by Havelund et al. our approach, too, found that the property was violated. Creating the observer and annotating the model took 0.827s. 14 states and 16 transitions were added automatically. The verification with UPPAAL took 0.7s and consumed 9.86MB memory.
When we implemented the fix that was provided by Havelund et al. we were able to verify that the property holds. We again created observers and annotated the model automatically, this took 0.662s, again 14 states and 16 transitions were added. The verification with UPPAAL took 6.344s and consumed 91.904MB memory.
(1.2)
Similarly to the observations stated by Havelund et al. our approach, too, found that the property was violated. Creating the observer and annotating the model took 0.722s. 14 states and 16 transitions were added automatically. The verification with UPPAAL took 0.345s and consumed 9.696MB memory.
When we implemented the fix that was provided by Havelund et al. we were able to verify that the property holds. We again created observers and annotated the model automatically, this took 0.733s, again 14 states and 16 transitions were added. The verification with UPPAAL took 5.418s and consumed 91.084MB memory.
(2)
Similarly to the observations stated by Havelund et al. our approach, too, found that the property was violated. Creating the observer and annotating the model took 0.775s. 15 states and 17 transitions were added automatically. The verification with UPPAAL took 0.527s and consumed 10.824MB memory.
When we implemented the fix that was provided by Havelund et al. we were able to verify that the property holds. We again created observers and annotated the model automatically, this took 0.677s, again 15 states and 17 transitions were added. The verification with UPPAAL took 8,761s and consumed 128.552MB memory.
Summary The three approaches we conducted were successful: Each one of them displayed an error, when we conducted the same changes to the fixed model, the results showed that the requirements were fulfilled.
[1]: Havelund, Klaus, et al. "Formal modeling and analysis of an audio/video protocol: An industrial case study using UPPAAL." Proceedings Real-Time Systems Symposium. IEEE, 1997.