Model-Based Design and Verification of Distributed Real-Time Systems
ELG 7187C - Course Notes (Winter
2013)
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, collaboration 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, and behavioral modeling
- 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)
- Reading material
- Software engineering principles R
- Developing a system description - an introduction R (course notes for SEG-2106)
- 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)
- Historical notes: 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.)
- Supplementary Material
2. Behavior modeling using states and transitions
- 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)
- Reading material
- Course notes
- Historical notes: See 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.)
- -Supplementary Material
3. Distributed system design
- 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 3, 7)
- Reading material
4. Performance modeling
- Leaning objectives
- (2-Analysis; 4-Design; 5-Tools) To use Markov models or Timed Automata to model the performance characteristics of a given functional behavior specifications, and to derive certain performance properties from these models.
- Reading material
5. Applications: Web Services and workflow modeling
- Leaning objectives
- (1-Knowledge) To understand how remote procedure calls and the conventions of Web Services can be used to build implementations of distributed system designs.
- Reading material
6. Comparing specifications and model checking
- Leaning objectives
- (2-Analysis; 5-Tools) To verify that a given communication protocol functions without flaws and provides a given required global service, possibly using automated tools for this purpose.
- Reading material
7. Deriving protocols for communication services and distributed workflow applications
- 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.
- Reading material
8. Future perspective
Last updated: March 15, 2013