Model-based Testing Distributed Systems with P Language

State: hard to describe this one. it's an atomic status like "lamp on" or "lamp off."

State Machine: a container for one or more states. The machine has an "active" state and all others are "inactive." The machine may respond to events based on its current active state and this may result in the main state changing.

Event: a message which a state machine

Payload: a piece of data which may be attached to an event.

Call transition: call/return stack like with functions. Allows you to change the main state--while still technically being within the state which was called.

Non-determinism: creating branch points where a random branch is chosen. This can be used to simulate a user choosing one of a number of options.

Fairness: ensuring random choices are picked a regulated number of times; an unfair coin toss can have infinite heads while a fair coin toss has as many heads as tails.

Safety condition: a given bad behavior must never occur.

Liveness condition: a given good behavior must occur.

Temperature measurement: making some states "hot," which increase temperature, which resets on a "cold" state, and treating an excess of temperature as a model failure.

Simulating faults in distrbuted systems by creating "fault injector" machines. They send a "reset" or "halt" event to other machines that respond by resetting or disabling themselves.