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 formalized in Isabelle/HOL (actually, our specification-based testing tool HOL-TestGen) and has been used in several case-studies. MST combines

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

But how does this work in practice? Let’s take a look on a small toy example: a toy bank that allows for checking the account balance as well as for depositing and withdrawing money. The state of the bank system is modeled as a map from client and account information to the account balance: \[\newcommand{\cmd}[1]{\operatorname{\color{blue}{#1}}} \newcommand{\fw}[1]{\operatorname{#1}} \begin{align} \cmd{type\_synonym} &&\fw{client} &= \fw{string}\\ \cmd{type\_synonym} &&\fw{account\_no} &= \fw{int}\\ \cmd{type\_synonym} &&\fw{data\_base} &= (\fw{client} \times \fw{account\_no}) \rightharpoonup \fw{int} \end{align}\] Our Bank example provides only three input actions for checking the balance, deposit, and withdraw money: \[\begin{align} \cmd{datatype} \fw{in\_c} &= \fw{deposit} \fw{client} \fw{account\_no} \fw{nat}\\ &~| \fw{withdraw} \fw{client} \fw{account\_no} \fw{nat}\\ &~| \fw{balance} \fw{client} \fw{account\_no} \end{align}\] The output symbols are: \[\begin{align} \cmd{datatype} \fw{out\_c} &= \fw{deposit\_ok} | \fw{withdraw\_ok} | \fw{balance\_ok} \fw{nat} \end{align}\]

The traditional way to specify a sequence test scenario in HOL-TestGen looks like this: \[\begin{align} \cmd{test\_spec} &~~\fw{test\_balance}:\\ ~~\cmd{assumes} &~~\fw{account\_def}: (c_0,no) \in \fw{dom} \sigma_0\\ ~~\cmd{and} &~~\fw{accounts\_pos}: \fw{init}~ \sigma_0\\ ~~\cmd{and} &~~\fw{test\_purpose}: \fw{test\_purpose}~ c_0~no~S\\ ~~\cmd{and} &~~\fw{sym\_exec\_spec}: \sigma_0 \vDash (s \leftarrow \fw{mbind_{FailStop}}~S~SYS; \fw{return} (s = x))\\ \cmd{shows} &~~\sigma_0 \vDash (s \leftarrow \fw{mbind_{FailStop}}~S~PUT; \fw{return} (s = x)) \end{align}\] 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.

References