Model Checking III
30 Novembro 2022, 16:30 • Antónia Lopes
- Linear Temporal Logic
- Syntax and semantics
- Safety and Liveness properties
- Verification of LTL properties with Spin
- Modelling communicating processes that exchange messages through buffered channels or use rendezvous points in Promela