Student projects

Introduction

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)

Proposed process for doing the projects:

• 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 difficulties.
• 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 form and format of your report. Please avoid plagiarism (this is a MUST)

CASE tools and related specification languages

Suggested tools

SPIN

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

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)

• 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

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

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 :
   • 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 UCMs)
   • 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 paper 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:
     1. 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).
     2. 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).
     3. Verify that the protocol specification has the properties defined by the service specification (using the Design-CPN tool).

Student presentations

• Schedule of student presentations - to be determined

• Powerpoint slides of past student presentations