Model Checking III

17 Novembro 2021, 16:30 • Antónia Lopes

Model Checking

• Linear Temporal Logic
  • Syntax and semantics
  • Safety and Liveness properties
  • Verification of LTL properties with Spin
• Channels in Promela
• Modelling communicating processes that exchange messages through buffered channels or use rendezvous points