Formal Models for Parallel and Distributed Systems (SS 2009)

Section outline

• Select section General

  General

  Collapse all Expand all

  Formal Models for Parallel and Distributed Systems (326.076, SS 2009)
  
  Time: Monday, 8:30-10:00, T041.
  Start: March 2, 2009.
  
  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 some of most important developments in this area:
  

  • Lamport's Temporal Logic of Actions (TLA) on which the specification language TLA+ is based,
    
  • Hoare's Communicating Sequential Processes (CSP) which was the origin of many parallel languages,
    
  • Milner's Calculus of Communicating Systems (CCS) for modeling communication and concurrency, and
  • Milner's 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. If you also login in Moodle and register as a course participant, you will receive per email all messages posted in the News forum.
  
  

  • Select activity News forum

    

    News forum
• Select section Topic 1

  Topic 1

  The Temporal Logic of Actions (TLA)
  

  • Leslie Lamport: Introduction to TLA
    
  • Leslie Lamport: Specifying Concurrent Systems with TLA+
    
  • The Temporal Logic of Actions I
  • The Temporal Logic of Actions II
    
  • Leslie Lamport: The Temporal Logic of Actions
  • Leslie Lamport: Specifying Systems (Amazon page).

  TLA+ Tools
  
  
• Select section Topic 2

  Topic 2

  Communicating Sequential Processes (CSP)
  

  • Nondeterminism and Parallelism (protected)
  • C.A.R. Hoare: Communicating Sequential Processes (paper)
  • C.A.R. Hoare: Communicating Sequential Processes (book)

  Formal Systems
  

  Software related to CSP (not used in this course): FDR2 refinement checker, ProBE animator, CSP type checker.
  

  
  
• Select section Topic 3

  Topic 3

  The Calculus of Communicating Systems (CCS)
  

  • The Calculus of Communicating Systems
  • A FSP model of the Jobshop
    
  • Luca Aceto et al: Reactive Systems: Modeling, Specification, and Verification
    
  • Robin Milner: Communication and Concurrency (Amazon page)

  LTSA
  

  • FSP Quick Reference
  • Concurrency: State Models and Java Programs
  • FSP Language Specification (restricted)
  • Processes (restricted)
  • Concurrency (restricted)
    

  mCRL2 (not used in this course)
  

  • The Formal Specification Language mCRL2
  • The mCRL2 Toolset
  • Analysis of a Session-Layer Protocol in mCRL2
• Select section Topic 4

  Topic 4

  The pi-Calculus
  

  • The pi-Calculus (Part 1) (4 on 1)
  • The pi-Calculus (Part 2) (4 on 1)
    
  • Elements of Interaction (protected)
    
  • Robin Milner: The Polyadic pi-Calculus: a Tutorial
  • Robin Milner: Communicating and Mobile Systems: the pi-Calculus (Amazon page)
  • M. Carbone et al: Structured Global Programming for Communication Behaviour
  • From the pi4soa project

  The Stochastic Pi-Machine (SPiM)
  

  • Modeling Biological Systems with the Stochastic Pi-Calculus (4 on 1)
    
• Select section Topic 5

  Topic 5

  Course Software
  

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

  
  
• Select section Topic 6

  Topic 6

  Exercises
  

  3 exercises will be handed out.
  
  

  • Select activity Exercise 1 (April 27)

    

    Exercise 1 (April 27) Assignment
  • Select activity Exercise 2 (June 2)

    

    Exercise 2 (June 2) Assignment
  • Select activity Exercise 3 (July 13)

    

    Exercise 3 (July 13) Assignment