TM8103 - Formal Methods
Lessons are not given in the academic year 2017/2018
The course is taught every second year, next time spring 2019.
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 verification by process algebra, temporal logic, rewriting logic and reasoning on UML constraints. With respect to verification tools, model checkers, theorem provers, SAT and SMT solvers will be discussed.
A. Knowledge: 1) A good understanding of the opportunities, methods and challenges in formal-based modeling, verification and development of functional properties in information and communication technology (ICT) systems. 2) In depth knowledge of the different techniques to specify ICT systems in a modular way and to verify that the models keep certain system properties. 3) Basic knowledge of verification tools like theorem proving and model checking. B. Skills: 1) Manage the terminology and theoretical concepts in the area of formal specification and verification. 2) Be able to specify models of ICT systems based on automata, temporal logic and protocol algebras. 3) Master verification proofs of invariant system properties. 4) Master simple refinement proofs that a more detailed system specification implements a more coarse-grained one. C. General competence: 1) Improved insight into the advantages of a formal-based system design in comparison to non formal programming.
Learning methods and activities
Lectures, self study, colloquiums and assignments.
A submission of a group assignment based on the model checking tool TLC.
The grading rule is pass/fail. The minimum passing grade is 70/100 points (70%).
- Group Work
Further on evaluation
If the course is failed, only the oral exam has to be repeated.
Exam registration requires that class registration is approved in the same semester. Compulsory activities from previous semester may be approved by the department.
Recommended previous knowledge
Experience with state based languages such as SDL, UML and LOTOS.
Required previous knowledge
Knowledge of Finite and Extended State Machines.
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.
- * The location (room) for a written examination is published 3 days before examination date.