Course Description (preliminary)

CSI 5174  -  Validation Methods for Distributed Systems

School of Electrical Engineering and Computer Science, University of Ottawa, Fall 2015

Official course description: Review of formal specification and description techniques for distributed and open systems. Verification techniques. Correctness proofs. Verification of general properties of distributed systems. Analysis and relief stragegies. Testing techniques. Test generation strategies. Test architectures.

Professor: Gregor v. Bochmann , phone: 562-5800 ext.: 6205, e-mail: , office: SITE building (room 5082), office hours:   by appointment, please send me an e-mail stating when you would like to meet

Lectures: Wednesdays  at 17:30-20:30 in room LMX 390.


The course gives an introduction to methods for specifying, verifying and testing designs and implementations of distributed systems. The main application areas are telecommunication systems, IP telephony and teleconferencing, Internet applications, Web Services and workflow modeling. Because of their complexity, these systems are difficult to design and implement. The students will learn about the principal methods that can be used for the design of such systems, for the precise descriptions of requirements, for the verification of the logical consistency of these descriptions, and for the testing of the implementations of the system components.

The course gives an introduction to certain formal modelling concepts (labelled transition systems, communicating finite state machines, Petri nets), and certain specification languages and other notations (such as UML State and Activity diagrams, and interaction diagrams) and their use during the development process using automated CASE tools. The course also deals with the comparison of different specifications based on various conformance relations, refinement, abstraction, composition and component replacement.

Leaning objectives

The following list contains some high-level learning objectives for this course. Each objective is preceeded by references to the "graduate attribute criteria" to which they belong (see Section 3.1 of the CEAB Accreditation Criteria and Procedures). In addition, the chapters of the course that concentrate on the objective are indicated at the end.

  1. (2-Analysis; 4-Design; 5-Tools) To design models of system behaviors that satisfy certain given requirements, using different modeling notations such as activity diagrams, labelled transition systems, finite state machines, input-output automata or Petri nets. (Chapters 1, 2, 4, 5, 6)
  2. (2-Analysis; 4-Design; 5-Tools) To design communication protocols for distributed systems that provide a global service that satisfies certain given requirements, using certain methods that are appropriate for the given situation. (Chapters 5, 7)
  3. (2-Analysis; 5-Tools) To verify that a given distributed system functions without flaws and provides a given required global service, possibly using automated tools for this purpose. (Chapters 2, 3, 4, 5, 6)
  4. (2-Analysis; 5-Tools) To develop a test suite that can be used for testing an implementation of a system component for conformance to a given behavior specification and a given fault model. (Chapters 8, 9)

Course activities:

Reading material: Reading material will be provided in the form of course notes and articles from the literature

Evaluation: Final exam (45% - possibly split into mid-term and final exams), exercises (20%), projets (35%, for presentation and final report)

Course content

  1. Introduction: the software development process, behavioral modeling and validation methods (1 week)
  2. Behavior modeling using states and transitions: Labelled transition systems (LTS) (1 week)
  3. Comparing specifications (1 week)
  4. Behavior modeling using Input-Output Automata(IOA) (1 week)
  5. Behavior modeling using communicationg finite state machines (C-FMS) (2 week)
  6. More powerful specification languages and verification tools (1 week)
  7. Deriving protocols for communication services and distributed workflow applications (1 week)
  8. Testing of component-based systems (1 week)
  9. Test architectures for distributed testing (1 week)

Project presentations by students (2 weeks, estimated)

Created: August, 2014, last update: June 22, 2015