Model-checking III

2 Dezembro 2016, 16:30 • Antónia Lopes

• Specification of properties
  • Linear Temporal Logic
  • Specification in SPIN

Model Checking

25 Novembro 2016, 18:30 • Antónia Lopes

Exercises about model-checking with Spin from Problem Set 6.

Model-checking II

25 Novembro 2016, 16:30 • Antónia Lopes

• Modelling concurrent systems with Promela
  • Shared memory
  • Synchronous communication
  • Asynchronous communication with reliable and lossy channels
  • Semaphores 

Model Checking

18 Novembro 2016, 18:30 • Antónia Lopes

Exercises about Model-checking and Spin from Problem Set 6. 

Model Checking I

18 Novembro 2016, 16:30 • Antónia Lopes

• Introduction
• Reactive vs Transformational Systems
• Modelling
  • Transition Systems
  • Interleaving model
  • Linear and branching semantic