Formal Models of Parallel and Distributed Systems (SS 2019)

Section outline

• Select section Formal Models of Parallel and Distributed Systems (SS 2019)

  Formal Models of Parallel and Distributed Systems (SS 2019)

  Collapse all Expand all

  326.0VR/326.076, Time: Monday, 8:30-10:00, Room S2 046. Start: March 25, 2019.

  This course deals with the formal modeling and specifying of concurrent systems such as parallel or multi-threaded programs, distributed hardware and software systems, mobile systems, and the like. We will discuss two major approaches:

  • The state-oriented approach which focuses on the sequence of states that a system has at any time. In essence, the model describes the transitions of the system from one state to another; we are interested to verify whether the resulting state sequence satisfies a specification formula. A representative of this approach is Lamport's Temporal Logic of Actions (TLA) on which the specification language TLA+ is based.
  • The communication-oriented approach which focuses on the sequence of communication operations in which a system may engage at any time. In essence, the model describes the flow of messages among the components of the system; we are interested to verify whether the resulting interaction behavior conforms to that of some specification system. A representative of this approach is Milner's Calculus of Communicating Systems (CCS) for modeling communication and concurrency and its successor, the pi-Calculus, which also models mobility.

  Our discussion will be accompanied by the demonstration of practical software tools supporting these calculi. The participants are expected to elaborate small exercises which will be used for grading (there will be no final exam).

  To take part in the course, you have to enrol in the KUSSS system. Since the exercises will be submitted via Moodle, you also have to login in Moodle and register as a course participant. You will then also receive per email all messages posted in the Announcements forum and may yourself post messages in the Questions and Answers forum.
• Select section The Temporal Logic of Actions (TLA)

  The Temporal Logic of Actions (TLA)

  • Select activity Leslie Lamport: Introduction to TLA

    

    Leslie Lamport: Introduction to TLA File
  • Select activity Logical Models of Systems

    

    Logical Models of Systems File
  • Select activity The Specification Language TLA+ (restricted)

    

    The Specification Language TLA+ (restricted) URL
  • Select activity Leslie Lamport: Specifying Concurrent Systems with TLA+

    

    Leslie Lamport: Specifying Concurrent Systems with TLA+ File
  • Select activity TLA Examples

    

    TLA Examples File
  • Select activity Leslie Lamport: The Temporal Logic of Actions

    

    Leslie Lamport: The Temporal Logic of Actions File
  • Select activity The Temporal Logic of Actions 1

    

    The Temporal Logic of Actions 1 File
  • Select activity The Temporal Logic of Actions 2

    

    The Temporal Logic of Actions 2 File
  • Select activity The TLA+ Home Page

    

    The TLA+ Home Page URL
  • Select activity The TLA+ Toolbox

    

    The TLA+ Toolbox URL
  • Select activity TLA+ Tools

    

    TLA+ Tools URL
  • Select activity Leslie Lamport: Specifying Systems

    

    Leslie Lamport: Specifying Systems URL
  • Select activity Amazon Page

    

    Amazon Page URL
  • Select activity How Amazon Web Services Uses Formal Methods (restricted)

    

    How Amazon Web Services Uses Formal Methods (restricted) URL
• Select section The Calculus of Communicating Systems (CCS)

  The Calculus of Communicating Systems (CCS)

  • Select activity Robin Milner: Communication and Concurrency

    

    Robin Milner: Communication and Concurrency URL
  • Select activity Robin Milner: A Calculus of Communicating Systems

    

    Robin Milner: A Calculus of Communicating Systems File
  • Select activity Luca Aceto et al: Reactive Systems: Modeling, Specification, and Verification

    

    Luca Aceto et al: Reactive Systems: Modeling, Specification, and Verification File
  • Select activity Nondeterminism and Parallelism (restricted)

    

    Nondeterminism and Parallelism (restricted) URL
  • Select activity The Calculus of Communicating Systems

    

    The Calculus of Communicating Systems File
  • Select activity Labelled Transition Systems Analyzer

    

    Labelled Transition Systems Analyzer URL
  • Select activity Jeff Magee & Jeff Kramer: Concurrency: State Models & Java Programs

    

    Jeff Magee & Jeff Kramer: Concurrency: State Models & Java Programs URL
  • Select activity A FSP Model of the Jobshop

    

    A FSP Model of the Jobshop File
  • Select activity FSP Quick Reference

    

    FSP Quick Reference URL
  • Select activity FSP Language Specification (restricted)

    

    FSP Language Specification (restricted) URL
  • Select activity Processes and Threads (restricted)

    

    Processes and Threads (restricted) URL
  • Select activity Concurrent Execution (restricted)

    

    Concurrent Execution (restricted) URL
  • Select activity Logical Properties (restricted)

    

    Logical Properties (restricted) URL
  • Select activity mCRL2

    

    mCRL2 URL
  • Select activity A mCRL2 Model of the Jobshop

    

    A mCRL2 Model of the Jobshop File
• Select section The pi-Calculus

  The pi-Calculus

  • Select activity Robin Milner: The Polyadic pi-Calculus: a Tutorial

    

    Robin Milner: The Polyadic pi-Calculus: a Tutorial File
  • Select activity Robin Milner: Elements of Interaction (restricted)

    

    Robin Milner: Elements of Interaction (restricted) URL
  • Select activity Robin Milner: Communicating and Mobile Systems: The Pi-Calculus

    

    Robin Milner: Communicating and Mobile Systems: The Pi-Calculus URL
  • Select activity The pi-Calculus (Part 1)

    

    The pi-Calculus (Part 1) File
  • Select activity 4 on 1

    

    4 on 1 File
  • Select activity The pi-Calculus (Part 2)

    

    The pi-Calculus (Part 2) File
  • Select activity 4 on 1

    

    4 on 1 File
  • Select activity Structured Global Programming for Communication Behavior

    

    Structured Global Programming for Communication Behavior File
  • Select activity Pi-Calculus for SOA

    

    Pi-Calculus for SOA URL
  • Select activity Stochastic Pi Machine

    

    Stochastic Pi Machine URL
  • Select activity Modeling Biological Systems with the Stochastic pi-Calculus

    

    Modeling Biological Systems with the Stochastic pi-Calculus File
  • Select activity 4 on 1

    

    4 on 1 File
• Select section Software

  Software

  I recommend to download the VirtualBox virtual machine for using the tools presented in this course.
  
• Select section Exercises

  Exercises

  Grading will be based on two exercises.
  

  • Select activity Assignment 1 (May 20)

    

    Assignment 1 (May 20)
  • Select activity Assignment 2 (July 15)

    

    Assignment 2 (July 15)