FASTEN: a modeling environment for safety critical systems
Assurance modeling using Goal Structuring Notation (GSN), and Claims Argument Evidence (CAE)
automating consistency checks between assurance argument models and system/safety models
analyzing the completeness and confidence of assurance arguments
Model based safety engineering - Fault Trees (FT), Failure Modes and Effects Analysis (FMEA), Hazards and Operability Studies (HAZOP)
integrate safety analyses with system models
Model-based requirements engineering
transition between textual to semi-formal and formal requirements
DSLs and tooling on top of SMV and PROMELA to make formal specification easier to understand and use
mbeddr - a stack of domain specific languages on top of C for the development of embedded systems
recently mbeddr was extended with DSLs to support Model-driven Code Checking (MDCC) using Spin
the MDCC support is experimental and now part of the mbeddr 2018.2.0 release - download
watch the screencast with an overview of mbeddr support for MDCC