FASTEN offers modern tool support for editing SMV models and interacting with NuSMV. Common usage patterns of NuSMV are lifted as first class DSLs which can be freely combined with each other. From high-level models, we generate .smv text files on which NuSMV is run. The results are lifted back in the FASTEN IDE.

  • The core constructs of SMV language

  • Unit tests described as tables

  • Statemachines in graphical notation







  • Modeling architectures using diagrams

  • Verification cases




  • Tabular notation for complex conditions

  • Generalized unit-tests

    • stars denote multiple values

    • hashes denote don't care

  • Component-based design

    • define interfaces and contracts

    • wire interfaces into architectures

    • perform A/G checks