Section outline

  • Formal Methods for Distributed Systems
    (Blocked Course, University of Debrecen, September 18-20, 2007)
    http://www.risc.uni-linz.ac.at/people/schreine/courses/ws2007/formdist

    Wolfgang Schreiner
    Research Institute for Symbolic Computation (RISC)
    Johannes Kepler University, Linz, Austria

    The goal of this blocked course is to describe languages and supporting tools for specifying and reasoning about distributed systems, i.e., hardware and software systems involving concurrency and communication. In detail, we will discuss:
    • Modeling and Reasoning about Concurrency
      • Tool: The Model Checker Spin
    • The Temporal Logic of Actions (TLA)
      • Tool: The Model Checker TLC