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

 

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

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 UPPAAL och TIMES. 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 Paul Pettersson och Wang Yi.

Schema

Mars 23-24, April 20-21, och Juni 5. Sal 6111. Preliminärt schema:

  • Mars 23 2006: Uppsala Universitet, MIC - " Introduction (slides), Untimed Model-Checking (slides), UPPAAL"
    • 10.15-12.00 - Föreläsning
    • 12.00-13.15 - Lunch
    • 13.15-14.00 - Föreläsning
    • 14.15-18.00 - Laboration
  • Mars 24 2006: Uppsala Universitet, MIC - " Timed Automata (slides), Region Construction (slides), UPPAAL's Input Languages (slides) "
    • 09.15-12.00 - Föreläsning
    • 12.00-13.15 - Lunch
    • 13.15-14.00 - Föreläsning
    • 14.15-17.00 - Laboration
  • April 20 2006: Uppsala Universitet, MIC - Region Construction, Symbolic Model-Checking (slides), Case-Study (slides).
    • 10.15-12.00 - Föreläsning
    • 12.00-13.15 - Lunch
    • 13.15-15.00 - Föreläsning
    • 15.15-18.00 - Laboration
  • April 21 2006: 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
    • 12.00-13.15 - Lunch
    • 13.15-14.00 - Föreläsning
    • 14.15-17.00 - Laboration
  • Juni 5 2006: Uppsala Universitet, MIC - Redovisning: projekt och uppsats.
    • 10.15-12.00 - Redovisning Uppsatser
    • 12.00-13.15 - Lunch
    • 13.15-17.00 (eller när vi är klara) - Redovisning Projekt

Delar av eftermiddagarna kommer att ägnas åt laborationer. Ta med egna laptops att uföra laborationerna på. 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 12:e Maj. 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 och betalas av studenterna själva (eller deras universitet eller högskola). Vi har förbokat rum på Hotel Uppsala. Ring 018-480 5005 tala med Jenny eller Mattis, ange bokningskod "ARTES" så blir priset för enkelrum 855 kr inkl moms (första kurstillfället) och 700 kr inkl moms (för andra kurstillfället) med frukost.

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