Lessons about using Contract-based Design (CBD) in FASTEN:

• CBD Lesson 1

  • • modeling interfaces and composite assemblies

• CBD Lesson 2

  • • 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

• CBD Lesson 4

  • • the use of temporal logics patterns for the specification of contracts

    • filtering the counterexample by using regular expressions

    • displaying the counterexample as a MSC