[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...