Student projects

in the course ELG 7187C  -  Topics in Computers: Model-Based Design and Verification of Distributed Real-Time Systemss

 (Winter 2013)

Introduction

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:
  1. 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 encountered
  2. 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.
  3. 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)
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.

Proposed process for doing the projects:

Important 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.

Here are some comments on the form and format of your report. Please avoid plagiarism (this is a MUST)

CASE tools and related specification languages

Suggested tools

SPIN

CPN - a tool for modeling with Colored Petri Nets (see also Petri Nets World)

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

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.

Other specification methods and tools

UML State Machines -  see here

First-order logic - theorem prover for Z (not suggested for a project)

IOAutomata (for applications of the controller derivation algorithm - not covered in this course in 2013)

Requirements capture tool for Live Sequence Charts (LSC)

Deriving MSCs (or UML sequence diagrams) from User Case Maps

Here are some comments on possible projects

(first written Sept. 2002, revised 2007, 2013

  1. 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 ?)
  2. If you want to work with Colored Petri nets :

Student presentations


Last update: January 11, 2013