Lessons about using Contract-based Design (CBD) in FASTEN:
modeling interfaces and composite assemblies
definition of pre/post-conditions written in Linear-Time Temporal Logics (LTL),
checking of the consistency between the system and its sub-systems using NuSMV, and
understanding why a verification failed by simulating the counterexample
CBD Lesson 3 (Part 1, Part 2, Part 3)
creating designs as SMV modules and checking refinement of the interface
multi-level decomposition of architecture
the use of temporal logics patterns for the specification of contracts
filtering the counterexample by using regular expressions
displaying the counterexample as a MSC