Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Complete Test Suites for Automata in Monoidal Closed Categories

Bálint Kocsis, Jurriaan Rot

TL;DR

A framework for proving completeness of test suites at the general level of automata in monoidal closed categories is introduced, and a generalization of a classical conformance testing technique, the W-method is provided.

Abstract

Conformance testing of automata is about checking the equivalence of a known specification and a black-box implementation. An important notion in conformance testing is that of a complete test suite, which guarantees that if an implementation satisfying certain conditions passes all tests, then it is equivalent to the specification. We introduce a framework for proving completeness of test suites at the general level of automata in monoidal closed categories. Moreover, we provide a generalization of a classical conformance testing technique, the W-method. We demonstrate the applicability of our results by recovering the W-method for deterministic finite automata, Moore machines, and Mealy machines, and by deriving new instances of complete test suites for weighted automata and deterministic nominal automata.

Complete Test Suites for Automata in Monoidal Closed Categories

TL;DR

A framework for proving completeness of test suites at the general level of automata in monoidal closed categories is introduced, and a generalization of a classical conformance testing technique, the W-method is provided.

Abstract

Conformance testing of automata is about checking the equivalence of a known specification and a black-box implementation. An important notion in conformance testing is that of a complete test suite, which guarantees that if an implementation satisfying certain conditions passes all tests, then it is equivalent to the specification. We introduce a framework for proving completeness of test suites at the general level of automata in monoidal closed categories. Moreover, we provide a generalization of a classical conformance testing technique, the W-method. We demonstrate the applicability of our results by recovering the W-method for deterministic finite automata, Moore machines, and Mealy machines, and by deriving new instances of complete test suites for weighted automata and deterministic nominal automata.

Paper Structure

This paper contains 34 sections, 38 theorems, 35 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Related work.
  3. Outline.
  4. Notation.
  5. Overview
  6. Complete Test Suites.
  7. The W-method.
  8. Generalizing the W-method.
  9. Words, Languages, and Automata
  10. Words
  11. Languages
  12. Automata
  13. Test Suites and the Generalized W-method
  14. Applications
  15. DFAs, Moore Machines, and Mealy Machines
  16. ...and 19 more sections

Key Result

lemma thmcounterlemma

Let $\mathcal{S}$ be a DFA with $n = |\mathcal{S}|$, and let $\mathcal{M} \in \mathcal{U}_{n + k}$ for some $k \in \mathbb{N}$. Suppose that $P \subseteq \Sigma^*$ is a state cover for $\mathcal{S}$ and $W \subseteq \Sigma^*$ is a characterization set for $\mathcal{S}$. Suppose furthermore that $\ma

Figures (4)

  • Figure 1: A DFA $\mathcal{S}$ for a coffee machine
  • Figure 2: A WA $\mathcal{S}$ for computing the decimal value of a binary number
  • Figure 3: An example DNA $\mathcal{S}$ accepting the language $L = \left\{ aa\ |\ a \in \mathbb{A} \right\}$
  • Figure 4: A faulty implementation WA $\mathcal{M}$

Theorems & Definitions (100)

  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • lemma thmcounterlemma
  • lemma thmcounterlemma
  • corollary thmcountercorollary
  • proof
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • ...and 90 more