Benchmarks for Mealy Machines (FSMs)

Downloads:

• All mealy benchmarks Δ (7zip, 103MB, Updated Februari 29th 2016)

The archive also contains a README with urls to some sources. All models are complete (or input-enabled), deterministic and minimal (or reduced). The benchmarks are in .dot format, where the from-state of the first transition is always the initial state. If you find any problems, unclarities or have a different format for FSMs, don't hesitate to contact us!

Summary of the benchmarks (the ones indicated TODO are in the archive, but not yet described below):

• Bankcards: Learned models of various bank cards and the e.dentifier2.
• Circuits: Circuits from ACM/SIGDA benchmarks, The Logic Synthesis Workshops.
• ESM: Mealy machine learned from the Engine State Manager (embedded controller software).
• Flattened from register automata or EFSMs with various sizes of domains.
• TLS / SSL implementations (protocols)
• Toy models TODO (small example models from various papers)

Models of bank card protocols

Bank cards (or debit cards) are smart cards used for payment systems. All smart cards follow the ISO/IEC 7816 standard. Here communication is in host-client mode: the terminal sends a command to the card, and the card returns a response, after which the terminal can send another command, etc. Commands and responses are simply sequences of bytes with a fixed format and meaning. Most smart cards issued by banks or credit cards companies adhere to the EMV (Europay-MasterCard-Visa) standard. This standard is defined on top of ISO/IEC 7816.

We have learned models for several client implementations, i.e. real bank cards from different banks. Access to the smart cards was realised via a standard smart card reader. The models might be incorrect, but already showed reproducible bugs in some cases.

See BenchmarkBankcard? for more information.

Learned models of the e.dentifier2

The e.dentifier2 is a hand-held smart card reader with a small display, a numeric keyboard, and OK and Cancel buttons. It is used for Internet banking in combination with a bank card and a PIN code. The e.dentifier2 appear to be based on EMV-CAP, a proprietary standard by MasterCard, which in turn is based on the EMV standard implemented in most bank cards.

Circuits

The logic synthesis workshops (LGSynth89, LGSynth91 and LGSynth93) provide 59 behavioural models for circuit synthesis. More background information can be found on the Benchmark Archives at CBL. These models can be seen as Mealy machines, (in several ways). The models are given as kiss2 files which consist of a list of transitions. As an example we consider a transition "01-- s1 s2 0-". Here "01--" is the input bit vector, "s1", "s2" are the source, target states resp. and "0-" is the output bit vector. A dash "-" means "don't care". In this example all the bit vectors "0100", "0101", "0110" and "0111" will trigger the transition. For the output we can interpret the meaning of don't care bits in (at least) two ways:

• Don't cares are observable. This means that "0-", "00" and "01" are three distinct values. This does not correspond to the physical behaviour of circuits.
• Don't cares keep the output bit unchanged. In this semantics an initial output bit vector is assumed (all zeroes) and "0-" will either output "00" or "01" depending on the state of the output bit vector.

In both cases, the models are deterministic, possibly partial Mealy machines. We consider two ways of completing the models:

• Self-loops. Whenever a transition is missing, remain in the same state and output "--" of correct length.
• Sink-state. Whenever a transition is missing, go to a sink (or crash) state with output "--" of correct length.

In both cases we will obtain a deterministic, complete Mealy machine. We provide all 4 semantics (2*2 combinations of above). If two or more semantics give bisimilar results, we only use one of them in the benchmark suite.

These models are used as benchmarks in papers by Hierons and Turker (TODO: provide references). They choose a semantics with observable don't cares and self-loops (with a distinct null output instead of a don't care output).

TODO: create a table with the list.

Model of the ESM controller

The Mealy machine "ESM Controller" is based on the RRRT-model as described in the [SMVJ15] paper. It is flattened to be a Mealy machine. In addition, an equivalent model was learned. The table below also lists different runs of the learning algorithm used in [SMVJ15] and contain all the hypotheses. This gives a nice sequence of machines, growing in size (Learning runs contain in total 207 models).

Moreover, two incorrect hypotheses are provided where we attempted to learn an extended model. Due to resource constraints we were never able to learn the proper models for this extension. These benchmarks are by far the biggest (finite) Mealy machines of real-world software we currently have.

See BenchmarkESMcontroller? for more information.

Mealy machines created by flattening basic register automata

On can obtain a Mealy machine (FSM) by taking a register automata (or EFSM), by restricting the data domain to a fixed finite set.

Alternating Bit Protocol

Biometric Passport

Boundary Retransmission Protocol

On the register automata page of this benchmark there are also mutants listed. You can find Mealy machine versions of these in the archive file containing all benchmarks at the top.

Simple login procedure

Palindrom repdigit checker

Farmer wolf goat cabbage river crossing puzzle

Session Initiation Protocol

When converting these models to Mealy machines, the result was not a completely specified machine. Self loops with a new output were added in order to complete the machine.

Models of implementations of the TLS protocol

See BenchmarkTLS for more information.