Overview

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:

• Lectures and discussions.
• Small exercises to be prepared by the student.
• Student project, applying one of the validation methods covered in the course to a relatively simple example system, and possibly using one of the existing software tools for this purpose. The student writes a report on his work and gives a short presentation of the results at the end of the course.

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

Course content

1. Introduction: the software development process, behavioral modeling and validation methods (1 week)
   • Waterfall and spiral software development processes - Model-Driven Development
   • 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
   • Different types of component interactions - interfaces (procedure call, messaging passing, rendezvous - local or remote)
   • Specification of component requirements including assumptions about the environment
   • Validation methods: verification versus testing
   • 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
     
2. Behavior modeling using states and transitions: Labelled transition systems (LTS) (1 week)
   • Labelled transition systems (LTS) - rendezvous and nondeterminism
   • State spaces defined by variables: guarded commands or first-order logic specifications
   • General system properties and design flaws
   • Safeness and liveness properties: temporal logics
   • Composition of LTS - communication architectures
   • Reachability analysis and detection of design flaws
3. Comparing specifications (1 week)
   • Semantics (meaning) of a model and comparison of specifications
   • Abstraction by projection (hiding interfaces) - state-nondeterminism
   • Temporal logic and model checking
4. Behavior modeling using Input-Output Automata(IOA) (1 week)
   • Introducing input-output into LTS
   • Design method: The dual behavior (see also Gouda's method - later)
   • Other communication paradigms
5. Behavior modeling using communicationg finite state machines (C-FMS) (2 week)
• Communication by asynchronous message passing: reachability analysis (additional problem: cross-over of messages)
• Gouda's protocol design method
• Considering faulty behaviors: message loss, out-of-order delivery, component failures (fail-safe or byzantine)
6. More powerful specification languages and verification tools (1 week)
   • Specification languages: Programming languages, Extended state machine models and Petri nets
   • Techniques for improving the efficiency of reachability analysis
   • Verification tools: Program Proving, Model Checking, Synthesis, and some specific tools
7. Deriving protocols for communication services and distributed workflow applications (1 week)
   • Partial order relations - weak and strong sequencing
   • Describing complex distributed behaviors as a composition of simpler collaborations
   • Finding message passing protocols for complex behaviors involving weak and strong sequencing
8. Testing of component-based systems (1 week)
   • White-box and black-box testing - regression testing - fault models
   • Test suite and fault coverage measures
   • Software testing techniques: considering control flow, data flow, parameter ranges
   • State machine testing techniques: checking output and next-state faults
9. Test architectures for distributed testing (1 week)
   • Typcal architecture of protocol testing
   • Synchronization issues between local and remote testers
   • Test suite development for embedded components
     

Project presentations by students (2 weeks, estimated)

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