Course Notes
CSI 5174 - Validation Methods for Distributed Systems
School of Electrical Engineering and Computer Science, University of Ottawa, Fall 2015
This page is under construction
Note: This page
will evolve as the course proceeds. I will indicate here details about the
reading material which covers the course content and also provide some
references to supplementary readings (not part of the course content, indicated
by << ... >>). In
addition, I may provide some newly written course notes for certain parts of the
course. Most Powerpoint slides are located here, and some articles from the general literature here.
In order to indicate which part of the course notes and the pointers to other material provided are essential for this course, I have tried to annotate all references by the following colored marks (if the mark is at the beginning of a paragraph or at the title of a document, then it applies to the whole paragraph or document, respectively):
- R means the understanding of the document is required
- A means that this represents additional reading material that could be useful for a better understanding of the required subjects
- C means that this may be of interest for a curious reader; the topic is outside the scope of this course
- R (pointers C) means that the pointed document is R, but the pointers within that document point to documents that are C, that is, outside the scope of this course
Prerequisites (please review this if you are not familiar with these concepts)
- Programming (for instance in Java): interfaces, classes, threads,
and how to program algorithms (see for instance in course SEG 2105 and
2106)
- UML: Class diagrams, Activity and sequence diagrams (see for
instance in course SEG 2105) - here is some reading material on software engineering and UML
- Finite state machines and UML state diagrams
(see for instance in course SEG 2106)
- Software engineering: development methods and processes (see for
instance in course SEG 2105 ) - here is some reading material on software engineering and UML
Course
content
1. Introduction: the software development process, behavioral modeling and validation methods (1
week)
- Leaning objectives
- (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)
- Topics
and reading material
- Waterfall and spiral software development processes - Model-Driven Development: Software engineering principles R
- Notations: programming languages, first-order logic, temporal logic, UML (Class, State, Activity diagrams), formal state-transition modeling (LTS, FSM, IOA, Petri nets);
the nature of syntax and semantics - the need for formality: Software engineering principles R - State-Transition modeling R
- Different types of component interactions - interfaces (procedure call, messaging passing, rendezvous - local or remote)
- Specification of component requirements including assumptions about the environment: Developing a system description - an introduction R (course notes for SEG-2106) - Example of domain modeling R - the Access Control System (course notes from SEG-2106)
- Validation methods: verification versus testing
- The architecture of communication protocols (a specific layered system architecture): See slides R. The main points are the following:
- Architecture of one protocol layer (within a layered architecture)
- Service definition: global view including several access points; abstract interface at each access point
- Protocol defined in terms of the behavior of both protocol entities ; coding of messages is an important aspect, order of interactions is also
important (example of connection establishment prior to using the connection
for data transfer)
- "concrete" service access interface is also important (in the form
of an API), e.g. socket interface in C provided under Windows to access the
TCP service
- Consider some standards: what do they define ? - (abstract) service,
protocol, "concrete" interface, message coding or what ?
- Example: Here are some diagrams from an example
protocol: TCP (taken from the book "Data Communications, Computer Networks and
Open Systems" by Fred Halsall, Addison Wesley, 1992)
- The challenges of distributed systems: distributed systems versus component-based designs or parallel systems
- Historical notes about notations for defining requirements, models and implementations and associated tools - experience and future outlook: see notes for SEG-2106 (Section 1) on State machine modeling and object-orientation and Model-based development. See also my recent paper C on the history of protocol engineering (G. v. Bochmann, D. Rayner and C. H. West, Some notes on the history of protocol engineering, Computer Networks journal, 54 (2010), pp. 3197–3209. Slides of talk at IEEE Canada 2011
- Supplementary Material
2. Behavior modeling using states and transitions: Labelled transition systems (LTS)
(1 week)
- Leaning objectives
- (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-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)
- Topics and reading material
- Labelled transition systems (LTS) - rendezvous and nondeterminism (see introduction in Chapter 1)
- General system properties and design flaws, e.g. deadlock, infinite loops (desired or undesired): course notes R.
- Composition of LTS - communication architectures - Reachability analysis and detection of design flaws: course notes R.
- The LTSA tool: see the Hotel example of the SEG-2106 course
- State spaces defined by variables: guarded commands or first-order logic specifications: course notes R.
- Safeness and liveness properties: temporal logics: course notes R.
- Supplementary Material
3. Comparing specifications (1 week)
- Leaning objectives
- (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)
- Topics and reading material
- Semantics (meaning) of a model and comparison of specifications: course notes R.
- Abstraction by projection (hiding interfaces) - state-nondeterminism: course notes R.
- Temporal logic and model checking: course notes R.
4. Behavior modeling using Input-Output Automata (IOA) (1 week)
- Leaning objectives
- (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-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)
- Topics and reading material
5. Behavior modeling using communicationg finite state machines (C-FMS) (2 week)
- Leaning objectives
- (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-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)
- (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)
- Topics and reading material
- Communication by asynchronous messages and queuing disciplines - reachability analysis: course notes R.
- Design methods for distributed systems: course notes R.
- Considering faulty behaviors: message loss, out-of-order delivery, component failures (fail-safe or byzantine) course notes R.
6. More powerful specification languages and verification tools (1 week)
- Leaning objectives
- (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-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)
- Topics and reading material
- Specification languages: Programming languages, Extended state machine models and Petri nets: course notes R.
- Techniques for improving the efficiency of reachability analysis: course notes R.
- Verification tools: Program Proving,
Model Checking, Synthesis, and some specific tools: course notes R.
7. Deriving protocols for communication services and distributed workflow applications
(1 week)
- Leaning objectives
- (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)
- Reading material
8. Testing of component-based systems (1 week)
- Leaning objectives
- (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)
- Reading material
9. Test architectures for distributed testing (1 week)
- Leaning objectives
- (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)
- Reading material
Last updated: June 22, 2015