Course - Formal Methods - TM8103
TM8103 - Formal Methods
About
Examination arrangement
Examination arrangement: Oral examination
Grade: Letters
Evaluation | Weighting | Duration | Grade deviation | Examination aids |
---|---|---|---|---|
Oral examination | 100/100 |
Course content
The course is taught every second year, next time spring 2011. Topics are: Focus is on theory for specification, validation and verification of network and network based service functionality specified by communicating state machines, protocol algebraic formulas, and temporal logic descriptions. The theory covers validation by model checking in non-reduced state space, and verification by process algebra, temporal logic, rewriting logic and reasoning on UML constraints.
Learning outcome
To be able to validate the correctness properties of a functional model and also to verify the consistency between models related to the various phases of the functionality life cycle, e.g. the consistency between required properties and functional design, or the consistency between functional design and implementation design.
Learning methods and activities
Lectures, self study, colloquiums and assignments.
A submission of a group assignment based on the model checking tool TLC.
Compulsory assignments
- Group Work
Recommended previous knowledge
Experience with state based languages such as SDL, UML and LOTOS.
Required previous knowledge
Knowledge of Finite and Extended State Machines.
Course materials
1) General papers:
E. Brinksma: What is the Method of Formal Methods, FORTE 91, Sydney November 1991.
B. Pehrson: Protocol Verification for OSI, Computer Systems and ISDN Systems no. 18, 1989-1990.
L. Lamport: The Temporal Logic of Actions, ACM Transactions of Programming Languages and Systems 16, 3 (May 1994) 872-923
P. Herrmann, H. Krumm: A Framework for Modeling Transfer Protocols. In Computer Networks, 34(2000)2, 317-337.
2) The model checkers SPIN and TLC:
G.J. Holzmann: SPIN Model Checker, The: Primer and Reference Manual. ISBN: 0-321-22862-6, Publisher: Addison Wesley Professional, 2004. http://www.aw-bc.com/catalog/academic/product/0,4096,0321228626-PRE,00.html
Y. Yuan, P. Manolios, L. Lamport: Model checking TLA+ Specifications,
CHARME'99, London, Springer 1999.
3) Process Algebra:
R. Milner: Communication and Concurrency,
Prentice Hall 1989, ISBN 0-13-115007-3 PBK.
Credit reductions
Course code | Reduction | From | To |
---|---|---|---|
DIE5938 | 7.5 |
No
Version: 1
Credits:
7.5 SP
Study level: Doctoral degree level
Term no.: 1
Teaching semester: SPRING 2011
Language of instruction: English
-
- Program/system-utvikling
- Telematics
Department with academic responsibility
Department of Information Security and Communication Technology
Examination
Examination arrangement: Oral examination
- Term Status code Evaluation Weighting Examination aids Date Time Examination system Room *
- Autumn ORD Oral examination 100/100
-
Room Building Number of candidates - Spring ORD Oral examination 100/100 2011-05-27
-
Room Building Number of candidates
- * The location (room) for a written examination is published 3 days before examination date. If more than one room is listed, you will find your room at Studentweb.
For more information regarding registration for examination and examination procedures, see "Innsida - Exams"