Journal about testing

Autonomous testing is one of the most powerful approaches for exploring vast state spaces in complex systems. Rather than manually writing test cases for every scenario, autonomous systems can systematically explore millions of states, discovering edge cases that human testers would never think to check.

In this two-part follow-up, we’ll continue the Super Mario Bros. testing series by implementing the autonomous testing approach presented by Antithesis, where they autonomously play and beat the game.

In Part 1, we built an autonomous system that beat all four levels of Super Mario Bros. without any human guidance. We treated the exploration as a mutation-based Genetic Algorithm, and it worked: the system discovered winning paths by exploring, replaying, and mutating input sequences. It found shortcuts, navigated complex enemy patterns, and even uncovered unexpected behaviors like the Level 4 collision bug. However, the exploration only validated one dimension of correctness: Mario’s progress. Our fitness function measured how far Mario advanced (x-position, level completion, and time), but the exploration couldn’t tell us whether the game actually behaved correctly. Did Mario’s velocity follow expected constraints? Were jumps causally justified? Did falling only occur when Mario lacked ground support? We had no way to know. This shows that autonomous testing by itself is not enough. To address this problem, we need a way to actually check state correctness. What we need is to plug in a behavior model!

The classic game Super Mario isn’t just fun to play—it has also become a favorite system for testing and analysis. In a blog post, Antithesis showed how their system that includes a deterministic hypervisor can autonomously play Super Mario and explore its vast state space. This kind of exploration is powerful for surfacing unexpected states, but it leaves one question unanswered: does the game behave correctly in every one of those states?

In this multi-part series, we tackle that challenge. Our approach is to apply a behavior model that captures the game’s intended mechanics—movement, physics, and collision detection—and use it as a framework for systematic testing. With this model, we can go beyond searching for the winning state: we can check that Super Mario behaves as it should in every explored state.

When testing complex stateful systems like Super Mario, behavior models can be your secret weapon. Think of them as property-based testing on steroids. The game world is vast, with countless combinations of player positions, velocities, physics states, and environmental conditions. This complexity makes it impractical to write classical test cases that cover any significant portion of the state space. At best, such tests can only form a sanity suite.

Imagine Mario sprinting through a level, collecting coins, and leaping over pits. Each action he takes depends on a myriad of factors: his speed, the timing of his jumps, his momentum and inertia, and even the layout of the level itself. Writing individual test cases for each scenario—like we showed in Part 1—would be like trying to count every grain of sand on a beach.

Have you ever found yourself fighting your test framework? Wasting hours searching for the right plugin just to run a test conditionally or in a dynamic loop? If so, you’re not alone. The problem might not be your tests, but the dominant “runner mentality” that governs them. For years, the software testing landscape has relied on this model. We diligently write tests as passive objects, only to hand them over to a separate runner that dictates their execution. This approach, popularized by frameworks like Pytest, and many others, certainly has its merits. Runners offer convention over configuration, and features like auto-discovery make it incredibly easy for beginners to get started. They provide a standardized way to execute tests, which is valuable. However, this convenience comes at a cost.

You’re running your tests, and there it is again — a red light, a failing check, you’ve found another bug. You sigh, roll your eyes, and maybe if you are a tester you mutter something about “the devs” or if you are a dev, well there is nobody to blame but yourself. But what if I told you… the bug isn’t the problem?

In fact, that little bug might be your system’s most honest state. And the truth is, it’s not the bug’s fault that you don’t want it — it’s yours!

Inspired by the first BugBash 2025 software reliability conference organized by Antithesis, this post is a lighthearted, and (hopefully) helpful take on why bugs deserve a little more love — or at least, a little less blame.

In software testing, you often hear terms like “condition,” “proposition,” “predicate,” “property,” and “invariant”—but what do they really mean? In this article, we’ll break each of them down by defining them in relation to the states and state transitions that make up state machines. After all, software programs are, at their core, state machines. To aid understanding, we’ll use a well-known puzzle: the Die Hard water jug problem as our reference system. To understand these terms, we will first define what a state is, what a sequence of states is, and how a system can be represented as a mathematical formula. As a bonus, we’ll also define what an assertion means.

Most software systems do not come with formal models. However, formal models are invaluable for constructing comprehensive test suites based on atomic propositions and for verifying the correctness of a system’s behavior using tools like TLA+.

In the previous article, Testing Simple Train Control System Using Its Formal Description, we explored how a formal model can be used to create a behavior model, which, in turn, was leveraged to calculate expected results for tests. However, in real-world applications, the inverse process—deriving a formal model from a behavior model developed during testing—is even more powerful.

In this article, we’ll explore exactly that process: how a testing behavior model can be transformed into a formal model. This approach opens up another dimension in understanding and testing software systems, offering a deeper level of rigor and insight.

In our previous post, Decoding Formal Description of a Simple Train Control System, we examined how to interpret a formal model defined through a Kripke structure for a simple train control system—the Ceiling Speed Monitoring Controller (CSMC). Now, we’re taking the next step by using this model to build a powerful test suite to verify an AI-generated Python implementation of the controller.

With AI tools like ChatGPT increasingly involved in code generation, rigorously testing this code is essential. So, we’ll develop the test suite and see how good the AI-generated code really is—buckle up, and let’s start testing!

In scientific research on software testing, you often come across papers filled with complex mathematical descriptions. Formal mathematics is commonly used in academia because it offers a precise way to describe how a system should behave in various situations, ensuring all possible cases are accounted for. However, for many testers, the math in these papers can feel overwhelming and difficult to apply to everyday testing work.

Terms like “Kripke structures,” “atomic propositions,” and “equivalence classes” might sound abstract and unfamiliar. However, these concepts aren’t as intimidating as they seem. They’re simply tools that help us think more systematically about a system, allowing us to create test cases that cover all the important behaviors.

Atomic propositions and equivalence classes offer a practical solution for making testing manageable when dealing with large or infinite input domains. While these concepts are widely used in formal verification—such as in Exhaustive Model-Based Equivalence Class Testing by W. Huang and J. Peleska, 2013, from which we’ll borrow the formal definition of equivalence classes—they are extremely useful in everyday testing tasks.

In this two-part post, we explore how atomic propositions and equivalence classes help us select “representative values” when input spaces are large. These representative values group inputs that behave equivalently, enabling thorough system testing without needing to cover every possible input within each group. Given that atomic propositions and equivalence classes are commonly used in formal verification, we also delve into the formal mathematical notation that defines these concepts.

Building on the foundations from Part 1 🛸, where we introduced atomic propositions and equivalence classes as mathematically rigorous techniques, this section will dive into applying these concepts in practice. Here, we’ll explore how to account for internal states, carefully select specific input values, and utilize a combinatorial sketch to cover all equivalence classes effectively.

Ready to dive deeper? Let’s continue our journey into advanced testing strategies!

Combinatorial testing significantly increases the test coverage of software systems, achieving levels of thoroughness that are unattainable with traditional test suites focusing on individual scenarios or limited combinations of user actions. However, combinatorial testing introduces the notorious test oracle problem—how to determine or compute the expected behavior for every possible combination of user actions.

The survey “The Oracle Problem in Software Testing: A Survey” provides an excellent overview of this issue, highlighting that deriving or even knowing the correct outcomes for complex combinations is often not straightforward. A common approach to solve this is by developing a behavior model that can compute expected outcomes for given system behaviors. Yet, many testers have never encountered the oracle problem, as they primarily deal with single combination tests. Fewer still have created or even understand what a behavior model entails.

To demystify behavior models, we will explore the development of such a model for a simple stateful system: a memory function that allows users to write, read, or erase data. We’ll illustrate how to apply combinatorial testing to this function and develop a behavior model from scratch to verify expected results.

Writing combinatorial tests usually requires that the author of the test plans for combinatorial testing upfront. This requires that all the combination variables and their values are identified and combined with the code that creates possible combinations and loops through each one of them. However, it would be nice to simplify the process and enable testers to write combinatorial tests in a manner that is as close as possible to a test that checks just one combination. This is where combinatorial Sketch‘es come in. A combinatorial sketch allows a tester to write combinatorial tests in an intuitive way without worrying about variable identification, calculation of combinations, and any explicit loops.

1
2
3
4
5
6
7
8
9

@TestSketch(Scenario)
@Flags(TE)
def test_add(self):
    values = {0, 1, math.inf, math.nan, 1 / 3, 2**-200, 2**200}
    sign = {1, -1}
    check_add(
        a=either(*values, i="a") * either(*sign, i="sign_of_a"),
        b=either(*values, i="b") * either(*sign, i="sign_of_b")
    )

According to the US National Institute of Standards and Technology’s (NIST) page on Combinatorial Testing, combinatorial testing can reduce costs for software testing, and its applications in software engineering can be significant. This is not surprising, as combinatorial testing is the cornerstone of any type of software testing. In its simplest form, one can think of it as finding the correct combination for a padlock. But instead of looking for a combination that opens the lock, the quality assurance team looks for combinations that lead to a violation of one or more requirements—the bugs. The technique is simple and universal, and in theory, it provides the most sought-out feature in testing, which is complete test coverage.

How do software development processes such as behavior-driven development (BDD), test-driven development (TDD), or even acceptance-test-driven development (ATDD) affect quality assurance team? To answer this question, we need to first note that all these terms end with “development” and not with “quality assurance”. But could we define behavior-driven quality assurance (BDQA), test-driven quality assurance (TDQA), or even acceptance-test-driven quality assurance (ATDQA)? If so, what would be the difference between them? Well, it would depend on the definitions of a behavior, a test, and an acceptance test.

For software systems with any non-trivial number of parameters, exhaustively testing all possible combinations of parameter values is not feasible. For example, if we have 10 parameters (k = 10) that each have 10 possible values (v = 10), the number of all possibilities is $v^k=10^{10} = {10}_{billion}$, thus requiring 10 billion tests for complete coverage.

“Requirements are the starting point of any design”, this is a quote from the presentation given by Nicholas D. Kefalas, who is a senior technical officer at Sikorsky Aircraft/Lockheed Martin. In this article, we’ll explore how you can work with requirements just like with code and look at a simple example of specifying requirements for a Google Calculator web application. While most people will agree with the quote above, somehow it is not applied or scarcely applied to the commercial software development process. We are developing too fast, and it seems like there is no time to think about the functionality that we are developing, much less write it down

Writing tests is not as easy task as it may seem at first glance. In many cases, writing a good test can be as hard as writing good application code. While readability and maintainability are both desirable features in application code, they are not always required. For tests, on the other hand, readability and maintainability are a must.