Hey - it looks like you got bit by the model bug!! Awesome, it’s fun stuff.
I had never heard the term “software model checking” before this. I’m gonna have to read up on some of these references (there are only 120 in this paper). Because I’m most interested in ultimately testing production systems along with connecting them to models, which seems like what this is talking about.
One newer tool that’s really cool in that space is Jepsen. It’s specifically geared towards testing production distributed systems using generative testing / property-based testing, and has found a great number of of bugs in real applications. Whenever you think about property-based testing, you generally assume that it’s used on fast, single-process programs because that’s how you can get the highest number of test cases per second. But you can use it at the integration test level too.
I’m looking into using something along these lines as a way to check that an implementation properly conforms to a model. In that workflow, you kinda get the best of both worlds. You have a model that you can check a lot more deeply, but you can automate the checking of whether or not the implementation correctly implements the model too. Obviously that last step isn’t perfect, because you’re not exploring enough of the state space, but maybe it’s fine in practice.
Compared to more general forms of program verification like interactive theorem proving, model checking provides more limited verification guarantees, but is cheaper due to its higher level of automation. Model checking thus offers an attractive practical trade-off between testing and formal verification.
Hey - it looks like you got bit by the model bug!! Awesome, it’s fun stuff.
I had never heard the term “software model checking” before this. I’m gonna have to read up on some of these references (there are only 120 in this paper). Because I’m most interested in ultimately testing production systems along with connecting them to models, which seems like what this is talking about.
One newer tool that’s really cool in that space is Jepsen. It’s specifically geared towards testing production distributed systems using generative testing / property-based testing, and has found a great number of of bugs in real applications. Whenever you think about property-based testing, you generally assume that it’s used on fast, single-process programs because that’s how you can get the highest number of test cases per second. But you can use it at the integration test level too.
I’m looking into using something along these lines as a way to check that an implementation properly conforms to a model. In that workflow, you kinda get the best of both worlds. You have a model that you can check a lot more deeply, but you can automate the checking of whether or not the implementation correctly implements the model too. Obviously that last step isn’t perfect, because you’re not exploring enough of the state space, but maybe it’s fine in practice.
Follow-up to https://lobste.rs/s/vsb6ue/case_for_models in response to a comment by @amw-zero.