in the course ELG 7187C - Topics in Computers: Model-Based Design and Verification of Distributed Real-Time Systemss
The projects apply certain concepts,
methods and tools discussed in the course to small example systems. The
evaluation will be based on the following three components:
The purpose of these projects is to get familiar with a given
specification language and associated tools (by using it to write a small
example specification), to get familiar with certain methods which can be used
to derive a more detailed system design or to verify that a given system design has no flaws and has the properties that are
desired for the particular example system in question.
- Project definition: This short document should include the following
topics: - the purpose of the project, the foreseen results, etc. - the
different steps which lead to the final results - description of preliminary
work already done at the time of writing (for example readings, draft of specification
prepared, initial experimentation with the tools, etc.) - any difficulties
- Oral presentation of the project and the preliminary results obtained (at
the date of the presentation). This presentation is planned for the last two
weeks of classes and should last around 30 minutes.
- Final report: This report should provide a summary of the work performed
and should explain the obtained results. It is also important to explain any
unexpected situations that have been encountered, such as errors detected in
the specifications, difficulties encountered in relation with the use of
tools. You are also encouraged to provide critical remarks concerning the
obtained results or any other useful comments. (Expected size: 10 to 20 pages)
Proposed process for doing the projects:
note: You are welcome to come for more meetings with the professor to
discuss the progress of your readings and experimentation, and to discuss any
questions you may have concerning the form of the system specification you are
developing or the orientation of your work. You may contact him after the class,
by phone or by e-mail.
- First three weeks of course: selection of topic (example system, problem
to be solved, and tool support). A special session for tool demonstrations is
also planned at the end of the second course chapter.
- For early February, after some initial work
on the project (if you encounter any problems with the
project, please talk to me): submission of the Project Definition (see
above) and subsequent discussion with professor.
- Every two weeks: Meeting with professor and discussion of progress and
- During the last two weeks of the term: Presentation of final or
preliminary results to the class (see above).
- At the end of the term: Final report (see above).
Here are some comments on the
and format of your report. Please avoid plagiarism (this is a MUST)
CASE tools and related specification languages
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.
CPN - a tool for modeling with Colored Petri Nets (see also Petri Nets World)
- This tool supports extended Petri nets (with tokens containing attributes - colors). See example simple_protocol
LTSA - Labelled Transition System Analyser (see overview of LTSA)
Alloy - a tool based on first-order logic
using an object-oriented syntax - for describing and analysing the structure and the behavior of systems
- 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)
UPPAAL - a tool for modeling extended state machine models possibly including hard real-time constraints (Timed Automata) - have look at the demos that come with the tool.
- 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
Other specification methods and tools
UML State Machines - see here
First-order logic - theorem prover for Z (not suggested for a project)
- 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.
IOAutomata (for applications of the controller derivation algorithm - not covered in this course in 2013)
- Drissi's tool is described in this
paper . The construction algorithm implemented in this tool is described
in more details here .
Requirements capture tool for Live Sequence Charts (LSC)
- 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)
Deriving MSCs (or UML sequence diagrams) from User Case Maps
- 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..
Here are some comments on possible projects
(first written Sept. 2002, revised 2007, 2013
- Consider one of the tools and its related specification method for very simple example first. Look at the examples given in the tutorial information. Then decide whether it is appropriate for the project you intend to do (what kind of system do you want to describe ? - what kind of verification do you intend to do ?)
- If you want to work with Colored Petri nets :
- Experiment with work flow examples (see
papers from the group
of Wil van de Aalst)c
- Design a train shuttle system (see
Case Study - from
Dagstuhl seminar - and
its view with
- Derive a protocol for a given service
specification and verify that the protocol provides the desired service. A method for deriving the specification of communication protocol
entities that realize a given service specification written in the form of a
Petri net is described in a
by Yamaguchi et al. ( Protocol synthesis and re-synthesis with optimal allocation of resources based on extended Petri nets ( H. Yamaguchi, K. El-Fakih, G. v. Bochmann and T. Higashino ), Distributed Computing, Vol. 16, 1 (March 2003), pp. 21-36.). The principles of this method can be easily applied
to service specifications written in the form of Colored Petri nets. The
project consists of the following:
- Write the service specification of the software engineering process
given in Figure 12 of the paper by Yamaguchi (or a similar behavior) in
the form of a Colored Petri net, using the CPN
tool (see above).
- Derive by hand a corresponding protocol specification, using the
method mentioned above, and write this specification in the form of a
Colored Petri net (using the Design-CPN tool).
- Verify that the protocol specification has the properties defined by
the service specification (using the Design-CPN tool).
Schedule of student presentations - to be determined
Last update: January 11, 2013