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.
Embedded Files
F A S T E N - a Formal Specification Environment
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
Page updated
Google Sites
Report abuse