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