Posted on by Achim D. Brucker, licensed under CC BY-ND 4.0.

Specification-based sequence testing is usually associated with various kinds of automaton models. While it is intuitive to model sequential systems (or communicating systems) as automatons, there is an interesting alternative: monads. Monads have been proven to be very successful in functional programming (e.g., Haskell) for representing step-wise computations. Thus, why not use them for sequence testing?

In fact, we developed a Monadic Sequence Testing Framework (MST) that is formalised in Isabelle/HOL (actually, our specification-based testing tool HOL-TestGen) and has been used in several case-studies. MST combines

1. generalised forms of non-deterministic automata with input and output,
2. generalises the concept of Mealy-Machines,
3. generalises the concept of extended finite state machines, and
4. generalises some special form of IO Automata, IO LTS’s, etc.

where the assumptions of this scenario (also called test purposes) are:

• $$\fw{account\_def}$$ that the initial system state $$\sigma_0$$ is a map that contains at least a client $$c_O$$ with an account $$no$$,
• the constraint $$\fw{init}~\sigma_O$$ constrains the tests to those $$\sigma_O$$ where all accounts have a positive balance, and
• $$\fw{test\_purpose}$$ constrains the set of possible input sequences $$S$$ to those that contain only operations of client $$c_0$$ and two of his accounts.

We skip the formal definitions of $$\fw{init}$$ and $$\fw{test\_purpose}$$ due to space reasons.

An example test case, picked from the list of the automatically generated abstract test cases, looks as follows:

\begin{align} \forall x \in \fw{dom} \sigma_0. 0 \le \fw{the}(\sigma_0 x) &\longrightarrow \sigma_0 (c_0, no) = \fw{Some} y\\ &\longrightarrow \fw{int} n' \le y + \fw{int} n\\ &\longrightarrow \sigma_0 \vDash os \leftarrow \fw{mbind_{FailStop}} [\fw{deposit} c_0~no~n, \\ &\fw{withdraw} c_0~no~n', \fw{balance} c_0~no]~PUT;\\ &\fw{unit_{SE}}(os=[\fw{deposit\_ok}, \fw{withdraw\_ok}, \\ &\fw{balance\_ok}(\fw{nat}(y+ \fw{int} n - \fw{int} n'))]) \end{align}

This abstract test case says: for any $$\sigma_0$$ which has only positive values, and a $$y$$ with the balance of the account of client $$c_0$$ on his account $$no$$, and sufficient money on the account such that the deposit and withdraw operations can both be effectuated (mind the precondition of withdraw that the balance must be sufficiently large for the withdraw), a test-sequence deposit-withdraw-balance must lead to the observable result that all three operations succeed and produce the result value $$\fw{nat}(y + \fw{int} n - \fw{int} n'))$$, where $$\fw{nat}$$ and $$\fw{int}$$ are HOL-library coersions between nats and integers. They are a result of our operations in the model that requires at some points natural numbers and at integers on others; this kind of complication is very common in constraints generated from programs or models.

For more information, please have a look on our TAP 2017 paper [1]. Our framework is implemented in HOL-TestGen.

Brucker, A.D., & Wolff, B. (2016). Monadic Sequence Testing and Explicit Test-Refinements TAP 2016: Tests And Proofs DOI: 10.1007/978-3-319-41135-4_2

### References

1. Brucker, A. D. and Wolff, B. “Monadic Sequence Testing and Explicit Test-Refinementstap 2016: Tests and proofs (2016): doi:10.1007/978-3-319-41135-4_2, URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-monadic-sequence-testing-2016

Welcome to the blog of the Software Assurance & Security Research Team at The University of Sheffield. We blog regularly news, tips & tricks, as well as fun facts about software assurance, reliability, security, testing, verification, hacking, and logic.