Interesting - and I agree about the tools. But what type tools can visualize states or requirements that we haven't yet considered? And is it possible that Spark achieves this by preventing unknown states, but it does so at an unacceptable cost. Where is the middle ground?
I'm not an expert on writing safety-critical software or Spark. Let me just start off by saying that.
I don't know if there is any way to use tools to visualize states or requirements that haven't yet been considered. It's easy to imagine two software systems interacting in completely unexpected ways that would be impossible to cover with a tool that only knew about its own system.
Here's a video of two automatic garbage cans triggering each other with hilarious results:
I think that's what makes Dr Leveson's work so interesting. She's basically side-stepping the issue of trying to enumerate all possible states and examining each one. Instead we just have to figure out the states we don't want our system to have and prevent them from occurring regardless of how these states might arise.
For example, we don't care about the details but we just want to be absolutely sure that a ballistic missile launch drill can't accidentally launch a real nuclear weapon.
I don't think Spark can help with this problem directly. The formal modeling languages will be able to help you detect ambiguity or conflicts in your requirements and that might lead you to discover faulty or missing requirements, but, again, I'm not an expert in this area.
We're a place where coders share, stay up-to-date and grow their careers.
We strive for transparency and don't collect excess data.