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
- Concepts,
Algorithms, and Tools for Model Checking,
by Joost-Pieter Katoen.
- TIMES online
help and tutorials.
- 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:
- Modelleringsspråket UML:
- Realtidsprogrammeringsspråk:
- Verktyg:
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.
|