ARTES
-------------------------------------------------

 

Formella analysmetoder för realtidssystem (5p) VT'04

En kurs i formel modellering, specifikation, och verifiering av realtidssystem. (Eng.: Formal Modelling and Analysis of Real-Time Systems)

Kursbeskrivning

Kursen introducerar formella språk för modellering av datorsystems beteenden och krav, matematiska metoder för analys, samt effektiva algoritmer och mjukvaruverktyg för analys. Efter kursen skall studenterna kunna validera formella specifikationer av datorsystem (speciellt tidskritiska system) med hjälp av mjukvaruverktyg såsom SPIN och UPPAAL. I kursen ingår momenten:
  • Introduktion till formella metoder
  • Finita automater
  • Büchiautomater
  • Temporallogik: LTL, CTL
  • Tidsautomater
  • Model-checking
  • Modellerings- och programmeringsspråk för realtidsystem
  • UML för realtidssystem
  • Verktyg: UPPAAL och TIMES.
  • Laborationer
  • Projektuppgift

Kursmaterial

  1. Concepts, Algorithms, and Tools for Model Checking, by Joost-Pieter Katoen.
  2. TIMES online help and tutorials.
  3. UPPAAL2k: Small Tutorial, by Alexandre David.

Referenslitteratur

  • Computation Tree Logics (CTL):
    • Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach, Edmund M. Clarke, E. Allen Emerson, A. Prasad Sistla. POPL 1983: 117-126. Also as "Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. Program. Lang. Syst. 8(2): 244-263 (1986)."
  • Linear Temproal Logic (LTL):
    • An Automata-Theoretic Approach to Automatic Program Verification, Moshe Y. Vardi, Pierre Wolper. (Preliminary Report). LICS 1986: 332-344. Also as "Reasoning About Infinite Computations. Inf. Comput. 115(1): 1-37 (1994)"
  • Timed Systems (Timed Automata, TCTL):
    • Automata For Modeling Real-Time Systems. ICALP 1990, pages 322-335. Also as "A Theory of Timed Automata, Rajeev Alur and David L. Dill. Theoretical Computer Science, vol 126, number 2, pages 183-235. 1994".
    • UPPAAL in a Nutshell, by Kim Larsen, Paul Pettersson and Wang Yi. Springer International Journal of Software Tools for Technology Transfer, 1(1-2), December 1997, pages 134-152.
    • Timed Automata - Semantics, Algorithms and Tools, Johan Bengtsson and Wang Yi. Tutorial on timed automata (a book chapter in Rozenberg et al, 2004, LNCS).

Verktyg

Lärare

Kursen ges av Wang Yi och Paul Pettersson.

Schema

  • Mars 9 2004: Uppsala Universitet, MIC - " Introduction (slides), Untimed Model-Checking (slides), UPPAAL"
    • 09.00-12.00 - Föreläsning (hus 2, sal 2245)
    • 12.00-13.15 - Lunch
    • 13.15-14.00 - Föreläsning (hus 2, sal 2245)
    • 14.15-18.00 - Laboration (hus 1, sal 1312)
  • Mars 10 2004: Uppsala Universitet, MIC, hus 2, sal 2245 - " Timed Automata (slides), Region Construction (slides), UPPAAL's Input Languages (slides) "
    • 09.15-12.00 - Föreläsning (hus 2, sal 2245)
    • 12.00-13.15 - Lunch
    • 13.15-14.00 - Föreläsning (hus 2, sal 2245)
    • 14.15-18.00 - Laboration (hus 1, sal 1312)
  • April 28 2004: Uppsala Universitet, MIC - Region Construction, Symbolic Model-Checking (slides), Case-Study (slides).
    • 10.15-12.00 - Föreläsning (hus 2, sal 2347)
    • 12.00-13.15 - Lunch
    • 13.15-15.00 - Föreläsning (hus 2, sal 2347)
    • 15.15-18.00 - Laboration (hus 1, sal 1313)
  • April 29 2004: Uppsala Universitet, MIC - Normalistion, Optimisations of Symoblic Model-Checking, Time-Optimal Reachability (slides), Timed Automata with Tasks, and TIMES.
    • 09.15-12.00 - Föreläsning (hus 6, sal 6002)
    • 12.00-13.15 - Lunch
    • 13.15-14.00 - Föreläsning (hus 6, sal 6002)
    • 14.15-17.00 - Laboration (hus 1, sal 1313)
  • Jun 16 2004: Uppsala Universitet, MIC - Redovisning: projekt och uppsats.
    • 10.15-12.00 - Redovisning (hus 1, sal 1145)
    • 12.00-13.15 - Lunch
    • 13.15-1x.xx - Redovisning (hus 1, sal 1145)

Delar av eftermiddagarna kommer att ägnas åt laborationer. Därtill kommer ett större projekt. För full poäng på kursen skall dessutom ett ämne självstuderas och redovisas muntligt (en presentation på ca 20 minuter) på redovisningstillfället den 16:e Juni. De ämnen som kan självstuderas är:

Uppgifter

Vägbeskrivning och boende

Kuren kommer att hållas på MIC vid Uppsala Universitet. Vägbeskrivning och kartor finns tillgängliga här.

Boende bokas av studenterna själva. Vi har förbokat rum på Hotel Uppsala (för båda perioderna). Ange bokningskod "ARTES" så blir priset för enkelrum 825 kr (inkl moms) med frukost. Information om detta och andra hotell finns i Kurssekretariatets hotelltips.

  ---------------------line----------------------------
  Strategic Research