Course - Formal Methods 2 - TM8108
Formal Methods 2
About
About the course
Course content
The course is taught every second year, next time spring 2012.
The course expands on methods and theory from Formal Methods. In particular, approaches for temporal logic-based correctness-preserving design of software will be discussed.
Learning outcome
A. Knowledge:
1) A good understanding of the opportunities, methods and challenges in formal modeling, verification and development of functional properties in information and communication technology (ICT) systems based on the Temporal Logic of Actions (TLA) and compositional TLA (cTLA).
2) In depth knowledge of the techniques to specify ICT systems in temporal logic and of refinement verification that a more detailed system specification implements a more coarse-grained one.
3) Basic knowledge of verification tools like TLC.
B. Skills:
1) Manage the terminology and theoretical concepts in the area of temporal logic.
2) Be able to specify models of ICT system in cTLA.
3) Master TLA verification proofs of invariant system properties and refinement proofs.
C. General competence:
1) Improved insight into the advantages of temporal logic-based system design in comparison to other formal modeling techniques.
Learning methods and activities
Guided self studies.
Recommended previous knowledge
PhD course Formal Methods - TM 8103
Course materials
P. Herrmann, H. Krumm, A Framework for Modeling Transfer Protocols,
Computer Networks, 34, 2, 2000, 317-337.
Further excerpts from text books and publications are decided at the start of course.
Subject areas
- Telematics
Contact information
Course coordinator
Department with academic responsibility
Department of Information Security and Communication Technology