By "valid system designs and implemetations", we mean designs and systems that satisfy their requirements. The tools creating such systems can be classified into the following categories:

**Program Proving:**The earliest efforts have been aimed at building program proving tools that check whether a given program satisfies its requirements which may be defined in terms of input and output assertions, invariants, etc. Such tools are based on theorem proving: The axioms related to the semantics of the programming language and the structure of the given program give rise to a large number of propositions, and the theorem proving tool is used to prove that the requirements are implied by these propositions. Theorem proving is an undecidable problem, therefore this approach cannot be completely automated (there exist no algorithm for theorem proving). As a consequence, one has to use human-assisted theorem provers to implement this approach. - It is difficult to perform in most cases.**Model Checking:**For state machines, there exist an algorithm (called Model Checking), that checks whether a given state machine satisfies properties that are defined in terms of temporal logic. Many tools for automatic model checking have been developed. For distributed systems, model checking of global requirements defined in terms of a temporal logic property must be preceeded by reachability analysis in order to obtain a global system model. Therefore most model checking tools include also the reachability analysis function. In the case of on-the-fly analysis, the global system model is not explicitely generated, but it is explored "on the fly" and at the same time the temporal logic requirements are checked.- Model checking for extended state machine models has also been developed, and programs can be interpreted as extended state machines - thus model checking for programs is also possible.

**Synthesis:**While in the above two approaches, the designer has to develop the design for a given requirements definition and can use the tools for checking that his design is valid. With the synthesis approach, a valid design is automatically generated from the given requirements. In general, this problem is also undecidable - therefore there exist no algorithm for doing this in general, but for certain important cases, synthesis algorithm exist, such as the following:**Synthesizing a state machine that satisfies a given temporal logic property**.**Control theory:**For a given behavior of a plant, given input from the environment and given behavior objective for the plant, it is possible to synthesize the behavior of a controller that will retrain the behavior of the plant in such a way that the behavior objective will be satisfied by the plant (if this is possible). Note that some interactions of the plant may not be visible by the controller, and some of the visible interactions may not be controllable (constrainable) by the controller.**Protocol derivation from service specification:**Given a global behavior (service specification) which defines actions for different components in a distributed environment, and assuming reliable message transfer between the different components, one can automatically derive the specification of a protocol to be executed by the different components which assures that the actions of the global behavior are performed in an order that satisfies the global service specification. For details, see next chapter of this course

- This
is an interesting tool for verifying properties of distributed systems. It
uses the
**Promela**language (related to C; with concurrent processes and queue communication) for the definition of the system to be analysed. It allows the specification, in temporal logic, of properties to be verified. This is based on relatively exhaustive state space exploration. Here is a paper on Spin by its author. Here is a tutorial.

- This tool supports extended Petri nets (with tokens containing attributes - colors). See example simple_protocol

- This is a tool developed in the UK which supports communicating finite-state transition machines communicating by rendez-vous (labelled transition systems). It supports the analysis of composed systems and comparison with service properties that are also defined by automata. It is used in a book on designing systems with concurrency for presenting different example systems and their analysis. It is used in the course SEG-2106 at UofO (see tool overview and examples). You may choose the following examples: IOA modeling: IOA-example.lts ; FSM with message passing: Two-SDL-processes - with implied receptions.lts ; nondeterministic accepting automaton (LTS) and minimization: accepting automata minimization.lts ; simplified TCP protocol: CommProtocol.lts and CommProtocol-symmetric.lts

- The described objects may represent temporal states of a dynamic system; therefore the system may be used for describing the possible sequences of states during the execution of a system.
- System properties may be specified by assertions. These assertions can be checked during the analysis for "all" system configurations that can be built according to the specification ("all" within some artificial limit imposed by the designer - in order to avoid the exploration of an infinite number of possibilities). You may down-load the tool.
- Read (and try) for instance the Tutorial - chapter 2 (River Crossing)

- Under "Support" you can find Help pages, an overview, a tutorial text presenting UPPAAL with a detailed example, introductory Powerpoint slides - Also look at the demo examples included in the tool:
**fischer**(a time-based mutual exclusion algorithm) and**train_gate** - You can down-load the tool; note that there is an academic version. Use the command File -> Open System to open some demos that come with the tool. Look at the
*train-gate*, in particular. - Note: The interactions in UPPAAL are inputs or outputs (like in IOA), but the communication semantics for communicating components is by rendezvous (the semantics of UPPAAL is based on LTS with added timers).
- Branching-time temporal logic can be used to defined abstract behavior properties

- The theorem prover, called Z/EVES, from ORA Canada can be obtained without charge (at least this was the case in 2003). It supports Z as the language for writing the system specification and the properties to be proven. From what I have heard about it, it was an interesting system, but it is not available any more from the creators.

- Drissi's tool is described in this paper . The construction algorithm implemented in this tool is described in more details here .

- LSC is a kind of improved version of Message Sequence Charts. This tool
lets the user "play in" sequences of system interactions (inputs and
corresponding expected outputs) and later allows to "play out" the captured
requirements while the user only provides inputs and the tool produces the
required outputs of the system.
*(I have not tried it out)*

- The latest version of the UCM Navigator also supports the generation of MSCs from a given UCM by letting the user select the possible choice at branching points. Currently, however, the generated MSCs can be displayed, but are not compatible for input to other modeling tools, such as the Telelogic SDL tool..

Created: November 6, 2014