- We will formally define Timed Automata.
- We will give a detailed presentation of the modelling and specification formalism of UPPAAL
- We will see example of a Train Gate covering - We will detail the UPPAAL verification engine.
- We will detail the UPPAAL verification options.
Exercise 1
Essentially we just use uppaal to check if any of those states are reachable.
you can also look at the last part of Session 6 Timed model
Exercise 2
So to get it to work we changed pub to a broadcast channel because it needed to tell the timeout and the machine that it has been shown.
Exercise 3
A)
Go to the link below to figure out what everything means.
Property Classifications
Validation Properties:
- All succeed
Safety Properties:
- Something bad CAN happen. IE they can try to go both at the same time.
- Passes
Liveness Properties:
- It could take infinite time for a train to cross and thats probably bad.
- same as 1
- same as 1
- same as 1
Deadlock:
- it might deadlock and that is bad
B) So whats going on here are 2 issues in the gate. in the code it pretends that we are 1 indexed, when in reality it is 0 indexed. So changing it from a 1 to a zero fixed it.
The other issue is that a transition can get stuck in the stop node (see image) if the stop node isnt urgent or committed. Since theoretically it is allowed to stay forever, ie allowing it to just straight up crash into the other train.
Exercise 4
A)
Essentially we made this prompt and then just brute forced out number to the lowest we possibly could. There is probably a way to find it automatically, but this works.
B)
Same as before just brute force until you get a result that fails and succeeds with a difference of 1.
C)
