Thesis: Verification and Controller Synthesis for Probabilistic Systems at Runtime

Case Studies

Thesis: "Verification and Controller Synthesis for Probabilistic Systems at Runtime"
Author: Mateusz Ujma

Included below are all models and properties used to generate experimental results in the thesis. The models are in the format for the PRISM-games tool.

Chapter 5: Incremental Model Construction

• zeroconf: IPv4 Zeroconf Protocol [KNPS06]
  
  
  • Model: zeroconf.prism
  • Parameters:
    • K (number of probes to send)
    Other constants (fixed):
    • N=6 (number of abstract hosts)
    • reset=false (whether or not to clear messages on restart)
  
  
• firewire: IEEE 1394 FireWire Root Contention Protocol [KNS03b]
  
  
  • Model: firewire.prism
  • Parameters:
    • deadline (leader must be elected before the deadline)
  
  
• mer: Mars Exploration Rover [FKP11]
  
  
  • Model: mer.prism
  • Parameters:
    • n (upper bound on the number of cycles)
  
  
• crowds: Crowds Protocol [Shm04]
  
  
  • Model: crowds.prism
  • Parameters:
    • TotalRuns (number of runs of the algorithm)
  
  
• mdsm: Microgrid Demand-Side Management ([CFK+12])
  
  
  • Model: mdsm3304.prism
  • Properties: mdsm3304.props
  • Parameters:
    • N (number of households)
    • D (number of days)
  
  
• android: Android stock monitoring
  
  
  • Model: android_3.prism
  • Properties: android.props
  • Parameters:
    • r (number of retries)
    • s (stock to query)

Chapter 6: Permissive Controller Synthesis

• cloud: Cloud service deployment ([CKJ12])
  
  
  • Model: cloud_steering_vm_5.prism (2 servers, 5 virtual machines)
  • Model: cloud_steering_vm_6.prism (2 servers, 6 virtual machines)
  • Properties: cloud.props
  
  
• android: Android stock monitoring
  
  
  • Model: android_3.prism
  • Properties: android.props
  • Parameters:
    • r (number of retries)
    • s (stock to query)
  
  
• mdsm: Microgrid Demand-Side Management ([CFK+12])
  
  
  • Model: mdsm3304.prism
  • Properties: mdsm3304.props
  • Parameters:
    • N (number of households: 3)
  
  
• investor: Future Markets Investor [MM07]
  
  
  • Model: investor.prism
  • Properties: investor.props
  • Parameters:
    • vmax (maximum share value: 10, 100, 200)
    • vinit (initial share value: fixed at 5)
  
  
• team-form: Team Formation Protocol [CKPS11, GdJ05]
  
  
  • Model: team-form-offline-fc-3.prism
  • Model: team-form-offline-fc-4.prism
  • Properties: team-form.props
  • Parameters:
    • N (number of agents: 3, 4, 5)
  
  
• cdmsn: Collective Decision Making for Sensor Networks [SS11]
  
  
  • Model: cdm3032.prism
  • Properties: cdmsn3032-runtime.props
  • Parameters:
    • N (number of sensors: 3, 4, 5)

Chapter 7: Heuristic-based Controller Synthesis

• zeroconf: IPv4 Zeroconf Protocol [KNPS06]
  
  
  • Model: zeroconf.prism
  • Properties: zeroconf.props
  • Parameters:
    • N (number of abstract hosts)
    • K (number of probes to send)
    Other constants (fixed):
    • reset=false (whether or not to clear messages on restart)
  
  
• wlan: IEEE 802.11 Wireless LAN [KNS02a]
  
  
  • Model: wlan4.prism
  • Model: wlan5.prism
  • Model: wlan6.prism
  • Properties: wlan.props
  • Parameters:
    • BOFF (maximum backoff)
  
  
• firewire: IEEE 1394 FireWire Root Contention Protocol [KNS03b]
  
  
  • Model: firewire.prism
  • Properties: firewire.props
  • Parameters:
    • delay
    • deadline
  
  
• mer: Mars Exploration Rover [FKP11]
  
  
  • Model: mer.prism
  • Properties: mer.props
  • Parameters:
    • n (upper bound on the number of cycles)
  
  
• android: Android stock monitoring
  
  
  • Model: android_3.prism
  • Properties: android_heuristics.props
  • Parameters:
    • r (number of retries)
    • s (stock to query)
  
  
• mdsm: Microgrid Demand-Side Management ([CFK+12])
  
  
  • Model: mdsm6.prism
  • Model: mdsm7.prism
  • Model: mdsm8.prism
  • Properties: mdsm.props