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

Monadic Sequence Testing?!

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.


A. D. Brucker and B. Wolff, “Monadic sequence testing and explicit test-refinements,” in TAP 2016: Tests and proofs, B. K. Aichernig and C. A. Furia, Eds. Heidelberg: Springer-Verlag, 2016. doi: 10.1007/978-3-319-41135-4_2.

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

You can also follow us on Twitter: @logicalhacking.




academia ai android apidesign appsec bitcoin blockchain bpmn browser browserextensions browsersecurity bug certification chrome composition cordova dast devops devsecops dom dsbd efsm epsrc event extensions fixeffort floss formaldocument formalmethods funding hol-ocl hol-testgen humanfactor hybridapps iast industry internetofthings iot isabelle/hol isabelledof isadof latex logic maintance malicous mbst mobile mobile apps modelinference modeling monads monitoring msc ocl ontology opensource owasp patches pet phd phdlife phishing policy protocols publishing reliability research safelinks safety sap sast sdlc secdevops secureprogramming security securityengineering securitytesting semantics servicecomposition skills smartcontract smartthings softwareeinginering softwaresecurity softwaresupplychain solidity staff&positions statemachine studentproject tcb test&proof testing tips&tricks tools transport tuos uk uoe upgrade usability verification vulnerabilities vulnerableapplication webinar websecurity


blog whole site