TACAS'11 Case Studies
Paper:
"Quantitative Multi-Objective Verification for Probabilistic Systems"
by V. Forejt, M. Kwiatkowska, G. Norman, D. Parker and H. Qu.
Included below are models, properties and scripts used to generate experimental results in the paper.
Models are in standard PRISM format and (where feasible) can be analysed with the default version of PRISM.
Most properties currently require the "prism-multi-fair" extension of PRISM
(which will be made publicly available in due course)
and are provided for information only.
Controller synthesis
-
IBM TravelStar disk-drive controller (original PRISM model from [NPK+05])
Compositional verification
-
Randomised consensus (algorithm from [AH90])
For this case study, since the reward structure is over the actions of all the components of the system,
to employ our compositional techniques we: we divide the reward structure into a number of sub-structures (one over the processes and one for each coin protocol).
and then use the fact that the maximum total reward of the system
with respect to the complete reward structure is less that or equal to the sum of the maximum total
rewards of the sub-structures.
-
Two processes
- Assumptions on coin protocols (standard probabilistic model checking):
- probability coin protocol returns same value for all processes: model and property
- Assumptions on processes (assumes probabilistic property of coin protocols):
- probability coin protocol of the second round is invoked: model and property
- probability coin protocol of the third round is invoked: model and property
- Guarantees on process (assumes properties of coin protocols):
- maximum expected reward for processes (3 rounds): model and property
- maximum expected reward for processes (4 rounds): model and property
- maximum expected reward for processes (5 rounds): model and property
- Guarantees on coin protocols (assumes properties of processes):
- maximum expected reward for coin protocol of round 1: model and property
- maximum expected reward for coin protocol of round 2: model and property
- maximum expected reward for coin protocol of round 3: model and property
- Non-compositional model checking: model (3 rounds, 4 rounds and 5 rounds) and property
-
Three processes
- Assumptions on coin protocols (standard probabilistic model checking):
- probability coin protocol returns same value for all processes: model and property
- Assumptions on processes (assumes probabilistic property of coin protocols):
- probability coin protocol of the second round is invoked: model and property
- Guarantees on process (assumes properties of coin protocols):
- maximum expected reward for processes (3 rounds): model and property
- maximum expected reward for processes (4 rounds): model and property
- Guarantees on coin protocols (assumes properties of processes):
- maximum expected reward for coin protocol of round 1: model and property
- maximum expected reward for coin protocol of round 2: model and property
- Non-compositional model checking: model (3 rounds, 4 rounds) and property
-
Zeroconf network configuration protocol (protocol from [CAG02])
- Assumptions on host (standard probabilistic model checking):
- safety assumptions on the host (encoded with automata): model and property
- actions send1 and send2 performed only finitely many time: model and property
- Assumptions on environment (assumes properties on host):
- actions rec0 and rec1 performed only finitely many time: model and property
- Guarantees on the host (assumes properties on environment):
- Non-compositional model checking: model and property