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
- 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
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:
- 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 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.
|