How to engineer and test mission critical software?

TL;DR: My goal is to create some framework with which I could discover/test all possible internal states of my application so that I would approach with confidence for example engineering software for medical devices, airplanes etc…

Let me first explain some context…

I was watching interesting video on example mapping technique used in agile practices. The video is about how to explore the domain space with examples which are creating a map for the problem domain space. In more concrete words they tried to get to model a solution for user story: “booking a train ticket”. After user story was presented, they layout rules or constraints for the solution space. After that they layout some basic examples in which they created interesting cases (examples) in which entities of the domain space can get into… From brainstorming session, they discover problem space that was not known before and created questions like “what should system do if this particular state can occur”.

Every programming solution that we programmers create is essentially to create a behavior for a list of use cases. Many times we don’t cover all the states in which our solution can get into or we miss unknown use cases that are creating illegal states and this is why further interactions are creating errors (unwanted behavior) of our system.

So I want to incorporate discrete event simulation testing in my standard toolbox that would analyze my system under scope with a mission to explore the problem space and to discover that unwanted behavior. Many times happened before when I didn’t have full knowledge about the domain space I was learning about that domain space with producing those errors, so using some discrete event testing simulation will be a great benefit to my software engineering practice along with DDD and TDD.

I’m a big fan of TDD but it often happens that you don’t cover all the cases because of limited domain knowledge…

So I’m thinking to incorporate some form of white box testing framework in which I would tell what are internal and external input/output constraints for various input arguments, databases calls, external services calls etc…) and the testing framework should discover unexpected behavior (bugs etc…) instead of me creating all those e2e tests that could be covered by the testing framework. And this could be a great addition alongside TDD…

My question is how NASA, for example, test their rocket system software? They must incorporate some form of discrete event simulations on their software so that they are confident that they have explored all the states in which system can enter?