[_pmf_]

It's used heavily in application code for automotive ECUs. It has code generators that generate output with a really, really, small footprint and zero runtime overhead; due to optimization at very high levels, this is on the level of really good LTO optimization.

Drawbacks: it's very un-agile; you really have to think the system through completely. (The magic being that if you do this, it is very likely correct by design.) It's not really feasible to specify a part of the system now and leave other parts open for later refinement. The other drawback being that no good non-commercial options exist.

[petra]

>> It's not really feasible to specify a part of the system now and leave other parts open for later refinement.

Is there any work or ideas on how to solve that issue?

And so it's also hard to add features later, in next versions ?

[nickpsecurity]

Stuff like these. It overlaps with model-driven development where you work at a higher level in constrained way to knock out many issues. Then, it generates safe code from that which you also check with tests or other tools.

https://en.wikipedia.org/wiki/Stateflow

https://en.wikipedia.org/wiki/Simulink

Recent example from high-assurance security:

https://www.umsec.umn.edu/sites/www.umsec.umn.edu/files/hard...