PyModel samples

PyModel is an open-source model-based testing framework in Python.

The samples directory contains a subdirectory for each sample, including a README with more
information about that sample. The samples are:

• abp: models the alternating bit protocol, a simple network
  protocol that retransmits lost or corrupted messages. This model is
  a Finite State Machine (FSM). It shows that an FSM can be
  used as the model (not just as a scenario machine). Just like a
  model program, an FSM can generate traces, generate graphics, and be
  composed with test suites.

• Marquee: a marquee with one line of text scrolling from right to
  left. Demonstrates how the size and structure of the data affect
  the number of states, how a configuration file can augment or
  replace items in the model, and how composition with a scenario
  machine can restrict the behavior of a model.

• populations: models a population whose members can be added or
  removed. It demonstrates state-dependent domains. Since the
  population is a collection of random elements, it would not be
  possible to define a fixed domain in advance.

• PowerSwitch: a very simple model program and an FSM, for an on-off
  power switch and a speed control. Demonstrates several PyModel
  techniques (including composition) on a minimal example.

• safety: models a microwave oven with a safety condition: the
  microwave power can only be on when the oven door is closed. Shows
  how to do safety analysis in PyModel: write invariants (safety
  conditions) that describe safe states, then use exploration to
  search for unsafe states.

• Socket: uses network sockets to demonstrate several PyModel
  techniques for modeling and testing systems that exhibit
  nondeterminism, concurrency, and asynchrony. Includes a stepper
  (test harness) for testing the Python standard library socket
  module. Also includes a simulator that can replace the standard
  socket module with a substitute that can be configured to exhibit
  failures and demonstrate nondeterminism.

• Stack: models a stack. Shows how to model return values as action
  arguments, write and use strategies to guide testing, use
  StateFilter to exclude states from being reached by the model,
  use composition of a model with a test suite to check that the
  traces in the test suite conform to the model, and use observable
  actions to get action arguments from a composed scenario or test
  suite rather than the domains defined in the model.

• StackResult: models a stack, in a different style than the Stack
  sample.

• Timeout: demonstrates the pmt -t (that is, --timeout) option.
  Shows how a simple test suite can be written to exercise a stepper,
  without writing a model program.

• tracemultiplexer: Simulate a program where two threads write to
  the same log file. Exhibit nondeterminism in scheduling threads. Try
  to synchronize so that only one thread at a time can write to the
  log. Detect unsafe states where both threads may write to the log.
  Identify log messages that may have been corrupted by unsynchronized
  writes from both threads.

• WebApplication: contains WebModel, a model for a web
  application, webapp, an actual web application implementation (in
  Python), and Stepper, a stepper that allows the tester pmt to use
  the model to drive the web application. To test, run webapp on
  localhost using the PyModel wsgirunner command. Stepper is a
  web client. It simulates a browser, sending HTTP requests to the
  web application.

For general directions on how to run the samples, see also
samples.txt in the notes directory.

Revised Apr 2013