Have you looked at model-based testing? One way to think of it as property-based testing for stateful system, though that's underselling it a little. It's surprisingly easy to come up models/specs for most stateful systems, including CRUD apps.
The first is that some effect happens asynchronously, potentially interleaved with other operations. Whether a client observes completion by polling or by receiving an event from a message broker is orthogonal to the specification itself - the model looks essentially the same in both cases. The built-in test executor uses polling, but that's an execution strategy, not a specification construct.
If you have a trace containing both requests/responses and observed events, you can use the model to check that the trace conforms to the specification. In practice, it helps if the events can be localized to some interval in the execution (e.g. "this happened after A and before B"); otherwise the checker has to consider many more possible concurrent interleavings.
The conformance testing docs hint at how this can be done, but don't yet show an event-driven example. It's a good enough question that I'll write a dedicated doc page on it.
Property-based testing and model-based testing are closely related. Both ask the developer to state the expected behavior of a system (whether you call it a property, invariant, model, specification, or contract) and then validate that behavior over arbitrary inputs and arbitrary sequences of operations. Property-based testing frameworks also typically provide fuzzing and shrinking.
Where we felt there was a gap was in expressing rich stateful behavior: models involving non-determinism (e.g. a timeout where the write may or may not have committed), concurrency, and eventual asynchronous completion, and then checking that an observed execution trace conforms to that model. Accordant aims to make those kinds of specifications concise and readable.
Once you have such a model, it's possible to integrate it with the fuzzing and shrinking capabilities of existing property-based testing libraries. We'll have documentation on that integration soon.
Every API has a contract - the rules for how it should behave. You can't withdraw more than the balance. You can't delete a resource with active references. You can't re-create what already exists. But usually these rules are never written down in one place. Accordant lets you write the contract directly, as executable code. Not documentation that drifts, but code - if the implementation stops behaving according to the contract, you get immediate failures. Not only can you use the executable spec to validate _arbitrary_ scenarios, you can also use the spec - a first class construct - to mechanically explore the state space of a system and generate interesting test sequences. The docs above have examples.
Also worth calling out that we've used the framework to model a number of complex, distributed real-world systems: those involving async processes, concurrency, retries and crash consistency. These are non-trivial specs (and they pair quite well with techniques like deterministic simulation testing). Great care has been taken to ensure the specs remain readable and concise despite that richness of behavior. For those of you old timers who might be familiar with Spec#/SpecExplorer and NModel, this model-based testing library is a descendant of that line of work.
With the rise in AI-assisted software development, I feel we need richer ways of specifying and validating software and I feel quite excited and bullish about the possibilities here. There's a lot more to say on the topic - follow my twitter feed if interested in more updates ;)
Yes, I understand why you made these design decisions. And I also agree that sticking to JS/TS keeps things simple (for humans, and LLMs). I generally default to the s and s' way of specifying things (in a C# property-based testing framework I'm working on) but looking at how you approached things here gives me another angle to think about.
Bombadil takes a fresh approach to UI testing I haven't seen before: online monitoring through LTL formulas. Unlike model-checking (say by TLC), LTL formulas over here unfold in lock-step with the UI and allow users to express interesting temporal properties during testing.
The other intriguing aspect was how state is modeled (or rather, maybe not explicitly modeled?). A lot of the examples show the state extracted from the DOM and temporal properties indicating what the next (or eventual) state _should be_. If we want to look at the existing state (according to the model/spec) when predicting the next state (similar to how you can use s when specifying s' in TLA+), there seems to be no direct way to do that. It should of course be possible to capture the state at an earlier time in a closure and use it in a thunk at a later point, so it should be possible to work around this but that can be a little awkward, maybe. I'm working on a project in this space (primarily geared towards backend API model-based testing) and the state of the _real_ system isn't globally inspectable unlike a web page so took a different route over there. Having said that, this is a very interesting design choice that's very intriguing (in a good way).
We have used Coyote/P# not just for model checking an abstract design (which no doubt is very useful) but testing real implementations of production services at Microsoft.
Microsoft Azure Storage | Seattle, WA | Onsite or Remote (US only)
Our team in Azure Storage is working on applying automated reasoning and validation techniques to scalably generate hundreds of thousands of tests to check data integrity and durability issues, and scalably validate a combinatorial number of feature interactions to catch regressions and subtle bugs that only happen under rare conditions. As a Software Engineer in this team, not only will you get an opportunity to use tools to specify and check the integrity, correctness and performance guarantees of a large and critical Azure service, you will also get an opportunity to work on building and improving the tools themselves as well as learn about existing state-of-the-art tools in this space. The lessons you will learn will be broadly applicable to any distributed system and will help accelerate your growth as a disciplined and thoughtful distributed systems engineer.
Microsoft's mission is to empower every person and every organization on the planet to achieve more. As employees we come together with a growth mindset, innovate to empower others, and collaborate to realize our shared goals. Each day we build on our values of respect, integrity, and accountability to create a culture of inclusion where everyone can thrive at work and beyond.
The official job posting is not live yet, so please reach out to me directly at [email protected] and include "Automated Reasoning and Validation Position" in the subject.
My team used Coyote to test their distributed service against network race conditions. It requires a little bit of setup to ensure all components that typically run on separate machines can run in a single process, and inter-process communication happens through interfaces that can be stubbed out during testing.
I designed a series of workshops to teach these ideas internally at Microsoft. You can find the source code used in the workshop at https://github.com/microsoft/coyote-workshop - the repo can use better README files but sharing it nonetheless in case the setup helps inspire your own use of Coyote.
TLA+ and Coyote pair quite well actually. Verifying the high level design in TLA+ while checking subtle bugs as you translate that design to an implemention.
Check out Coyote (which is an evolution of P) and allows you to "model check" .NET code to find hard to find race condition-y bugs in your implementation. We have used it very successfully on a number of projects at Microsoft. I should probably do more public talks on it to get the word out. Finding subtle bugs in your implementation using tools like Coyote is easier than most people realize.
Coyote (concurrency exploration tool for .NET programs) can be used to do something "similar". My team often writes tests which set up focused concurrency between different APIs, the tests use Coyote to explore different ways that concurrency can unfold and write a strong set of assertions and invariants that must be true at the end. It's not TLA+ but it's still quite effective, very teachable as developers are already familiar with writing C# tests and helps catch safety and liveness bugs in our actual code base (as opposed to a model of it). It's not the same, by design, and does a decent job at finding concurrency and distributed system bugs.
Visualizations do help a lot when model checkers and concurrency schedule exploration tools like Coyote find bugs. Coyote include the ability to visualize the traces if you express your concurrency using actors (see https://microsoft.github.io/coyote/#concepts/actors/state-ma...)
It also allows you to implement your own "logger" through which you can emit enough information to construct some cool visualizations. I had a lot of fun working on visualizing an implementation of Paxos using Coyote (then P#) (screenshot at https://ibb.co/TTk2hYb)
Loom's style of exploration (and that of aws shuttle mentioned below) can be quite effective. Coyote is the equivalent library in the .NET world (formerly known as P#) and comes with a bunch of exploration "schedulers" (from random exploration to probabilistic and even an experimental reinforcement learning based one). They released an animation rich video today (see https://news.ycombinator.com/item?id=26718273). Worth watching even if you're using Rust as Loom and aws shuttle are conceptually similar.
There has been a bunch of content on Coyote shared before as well but the quality of animations and how they explain how it works under the hood in this introduction was excellent.
The tweet links to a couple of tutorials showing how to test an extremely simple CRUD service using Coyote to find concurrency bugs. Developers write simple unit tests whose concurrency is explored by Coyote to find bugs. You might be surprised to learn how we can write a number of interesting concurrency tests for even the simplest of CRUD services.
I worked on an explanation of Paxos where we start with a simple but incorrect implementation of the protocol. The bug is then fixed and the protocol refined. Which leads to another bug. Interestingly, after fixing 6 or 7 bugs we arrive at the actual working implementation of Paxos. The reader, having walked the path of arriving at the protocol (hopefully) understands the nuances better than just reading the description of the protocol from the get-go.
Concurrency is hard - this was a great investigation into the bug using TLA+ by the author which suggested simplifications to the code in addition to the bug fix.
This reminded me of another reader/writer concurrency bug posted by Tom Cargill in the c2 wiki caused by surprising behavior of Java monitors, which Hillel Wayne showed how to discover and then fix using TLA+ at https://www.hillelwayne.com/post/augmenting-agile/
We were able to reproduce and fix the same bug using Coyote as well, and documented our experience at https://cloudblogs.microsoft.com/opensource/2020/07/14/extre... I was pleasantly surprised at the finding and was definitely heartened by our experiment where we were able to reproduce the bug in actual working C# code without the need of an additional modeling step. While TLA+ is undoubtedly very powerful when it comes to modeling and catching concurrency bugs, I do hope tools like Coyote get wider adoption and are implemented for more languages so bugs in critical infrastructure code can be caught in a scalable and repeatable way while staying within just one language for implementation _and_ testing.
This is a fair call-out. I'll like to share a counter-example where we 'model check' our real-world service written in C# with pretty decent effectiveness. As you rightly call out, the number of execution points around which the model checker explores interleavings in a concurrent situation cannot be too large. If you look at _most_ micro-services, the really interesting points around which interleavings have to be explored are to external storage systems, say, Cosmos DB or Azure Storage etc. This is because most micro-services maintain their state in these external systems and are otherwise stateless. This insight allows us to only explore interleavings around calls to these external services as that's where a ton of concurrency bugs reside and ignore the interleavings at arbitrary points _within_ the services. Leveraging this insight allows us to utilize concurrency testing tools like Coyote on real world code and services with the testing scaling decently with the size of the program.
Source: I've modeled a number of CRUD like and non-CRUD like systems through the Accordant framework (https://github.com/microsoft/accordant)