"Model Checking for Probabilistic Timed Automata" - Case Studies

Paper: "Model Checking for Probabilistic Timed Automata"
by Gethin Norman, David Parker and Jeremy Sproston

Included below are the models and properties for the two PRISM PTA case studies featured in the paper.

• Markowitch & Roggeman's Non-Repudiation Protocol
  
  
  • Model (honest version): honest.nm
  • Properties (honest version): honest_eventually.pctl, honest_deadline.pctl
    
    
  • Model (malicious version): malicious.nm
  • Properties (malicious version): malicious_eventually.pctl, malicious_deadline.pctl
  
  
• Task-Graph Scheduling
  
  
  • Model (basic version): scheduler.nm
  • Model (version with random execution times): scheduler_prob2.nm
  • Model (version with a faulty processor): scheduler_failure.nm
  • Properties (all versions): scheduler.pctl
  • PRISM commands (all versions): commands.txt