Behaviour-driven development
[Slides]Abstract
This lesson goes over the basic concepts in Formal Methods, focusing on software specification and verification techniques. Pros and cons ot these techniques are analyzed, hinting at the fundamental decidability and feasibility issues, and providing examples of industrial case studies. A very simple hands-on model checking example on a trivial mutual exclusion protocol is also included.
Additional notes
A specification for the final example/demo is formalized both in Promela, the specification language of the SPIN model checker, and in the specification language of the NuSMV model checker. The Promela specification is available here, whereas the NuSMV specification is available here.