I finally read this! I like the idea, but I was left with questions. Note that I’ve never (beyond a couple of courses at university some 20 years ago) used formal methods, so this is probably partly domain ignorance.
Nothing here is obvious about how to make a “model” that can be validated as a correct model of what we want. I find this is the biggest bar to useful testing other than pure regression testing (which this probably helps with).
Did I correctly understand that the nature of the model is a trivial implementation of some aspect of the system in order to basically do comparative testing?
For 1., this is a great observation, and definitely a common question. Since the model is the source of truth, there’s definitely a risk of building an implementation that matches the model, but your model doesn’t do what you want it to. I talk about this in Misspecification.
A couple thoughts there. First, this is always a potential problem. There’s an example in that post where a set of automated test cases still misses out on catching an edge case. A test suite doesn’t define the complete behavior of an application either (underspecification), and you can also assert on incorrect behavior (misspecification). Whatever you use as the source of truth, there’s nothing (other than you) that can be sure that it’s correct.
The argument for model-based testing is that avoiding misspecification becomes easier because the model is so much smaller and simpler than the implementation. It’s much easier to check properties / invariants on a model, where that might not be feasible at the implementation level. If the model is executable, you can write simple example-based tests on the model as well, but those are still easier than unit testing a full application. Also, certain operations become trivial (like basic CRUD stuff), so they may really be obvious just by looking at them.
For 2., yea I think you’re understanding that right. To get a little philosophical, I think a model is more than that, which I wrote more about in Refinement. I think a model is actually the essence of the behavior that you want to build a lot of times, and boiling an application down to that essence has other benefits than just testing. Imagine the scenario where someone outside of the Engineering department asks you a detailed question about how the logic works for a particular part of the app. Instead of tracing through thousands of lines of client-side networking code, caching layers, database queries, DTOs, etc., you can consult a simple model to answer that question.
So the model actually also serves as a manageable blueprint and overview of your application, and tests can be derived from that.
Thanks, this makes sense. For some reason specifying the model this way doesn’t seem right to me for no reason I can articulate. I certainly don’t have a way that I think would be better either.
That said, maybe this is perfect. You get to have all the same types, and if you’re in a language that can integrate other forms of constraints, you can put those in your model too.
Writing a model like this in the same language as your implementation (or in this case, just in the same language as the client) is definitely a strange approach. I have definitely seen others do it, but what re-sparked my interest in it is that Amazon recently wrote a paper about using this approach for a component inside of S3.
I’d say most people that actually do model-based testing use some kind of state machine language for their model, which has some formal semantics. This suffers from the verification gap though - you have to figure out how to connect your model to the actual implementation. So you definitely lose out on the purity and logical soundness of the model by writing it in TS for example, but it was honestly very convenient and led to a very simple developer workflow.
I finally read this! I like the idea, but I was left with questions. Note that I’ve never (beyond a couple of courses at university some 20 years ago) used formal methods, so this is probably partly domain ignorance.
For 1., this is a great observation, and definitely a common question. Since the model is the source of truth, there’s definitely a risk of building an implementation that matches the model, but your model doesn’t do what you want it to. I talk about this in Misspecification.
A couple thoughts there. First, this is always a potential problem. There’s an example in that post where a set of automated test cases still misses out on catching an edge case. A test suite doesn’t define the complete behavior of an application either (underspecification), and you can also assert on incorrect behavior (misspecification). Whatever you use as the source of truth, there’s nothing (other than you) that can be sure that it’s correct.
The argument for model-based testing is that avoiding misspecification becomes easier because the model is so much smaller and simpler than the implementation. It’s much easier to check properties / invariants on a model, where that might not be feasible at the implementation level. If the model is executable, you can write simple example-based tests on the model as well, but those are still easier than unit testing a full application. Also, certain operations become trivial (like basic CRUD stuff), so they may really be obvious just by looking at them.
For 2., yea I think you’re understanding that right. To get a little philosophical, I think a model is more than that, which I wrote more about in Refinement. I think a model is actually the essence of the behavior that you want to build a lot of times, and boiling an application down to that essence has other benefits than just testing. Imagine the scenario where someone outside of the Engineering department asks you a detailed question about how the logic works for a particular part of the app. Instead of tracing through thousands of lines of client-side networking code, caching layers, database queries, DTOs, etc., you can consult a simple model to answer that question.
So the model actually also serves as a manageable blueprint and overview of your application, and tests can be derived from that.
Thanks, this makes sense. For some reason specifying the model this way doesn’t seem right to me for no reason I can articulate. I certainly don’t have a way that I think would be better either.
That said, maybe this is perfect. You get to have all the same types, and if you’re in a language that can integrate other forms of constraints, you can put those in your model too.
Writing a model like this in the same language as your implementation (or in this case, just in the same language as the client) is definitely a strange approach. I have definitely seen others do it, but what re-sparked my interest in it is that Amazon recently wrote a paper about using this approach for a component inside of S3.
I’d say most people that actually do model-based testing use some kind of state machine language for their model, which has some formal semantics. This suffers from the verification gap though - you have to figure out how to connect your model to the actual implementation. So you definitely lose out on the purity and logical soundness of the model by writing it in TS for example, but it was honestly very convenient and led to a very simple developer workflow.