Title:

Formal Analysis and Verification

Code:FAV
Ac.Year:2007/2008
Sem:Winter
Curriculums:
ProgrammeField/
Specialization
YearDuty
IT-MSC-2MGM.-Elective
IT-MSC-2MIN.2ndElective
IT-MSC-2MIS.-Elective
IT-MSC-2MPS2ndElective
Language of Instruction:Czech, English
Public info:http://www.fit.vutbr.cz/study/courses/FAV/public/
Credits:5
Completion:examination (verbal)
Type of
instruction:
Hour/semLecturesSeminar
Exercises
Laboratory
Exercises
Computer
Exercises
Other
Hours:2600026
 ExamsTestsExercisesLaboratoriesOther
Points:6000040
Guarantor:Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Lecturer:Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Faculty:Faculty of Information Technology BUT
Department:Department of Intelligent Systems FIT BUT
Prerequisites: 
Algorithms (IAL), DIFS
Formal Languages and Compilers (IFJ), DIFS
 
Learning objectives:
  The goal of the course is to introduce formal analysis and verification to students as a modern and promising  method of automated evaluation of properties of various kinds of safety-critical systems (such as drivers and other parts of operating systems, control software, workflow, communication protocols, parts of hardware, etc.). The course acquaints students both with the theoretical background of the given area, with computer-aided tools based on them as well as with successful applications of formal analysis and verification in practice (Intel, Nasa, Microsoft, Ericsson, Nokia, ...).
Description:
  Formal analysis and verification as a perspective complement and/or alternative to validating properties of concurrent reactive systems by means of simulation and testing. An introduction to the methods, tools, and capabilities of formal analysis and verification. Selected modelling, query, and specification languages. State spaces and their use for formal analysis and verification. Selected methods of reducing state spaces. An overview of the areas where formal analysis and verification has been successfully applied in praxis. A brief description of several advanced computer-aided tools for formal analysis and verification: Spin, Slam, Java PathFinder, Blast, SMV, etc. (according to the current state of the art). Formal analysis and verification of systems working in real time (Uppaal, Kronos, HyTech, TReX, and similar tools). Automated theorem proving.
Subject specific learning outcomes and competencies:
  Students are acquainted with principles and methods of formal analysis and verification and with their application within the process of designing safety-critical systems. Students know capabilities and the basic ways of using computer-aided tools for formal analysis and verification.
Generic learning outcomes and competencies:
  Acquired knowledge about the significance and possibilities of using formal methods within the development of various kinds of systems and about their growing use in practice.
Syllabus of lectures:
 
  1. The meaning of the terms ``formal analysis and verification''. Capabilities and contribution of formal analysis and verification. The structure of the (automated) process of formal analysis and verification. Theorem proving, using state spaces, the state explosion problem.
  2. State spaces, state space paths, abstractions of states and transitions. Interleaving and true concurrency. Linear and branching time. Safety, liveness, and fairness.
  3. A brief overview of commonly used modelling languages (networks of finite automata, Petri nets, specialized parallel languages, etc.). Specification and query languages. Statistics on the level of state spaces and on the level of modelling languages. Model instrumentation, Büchi automata, testers.
  4. Temporal logics. LTL, CTL, CTL*, mu-calculus. The relation of temporal logics and automata. Indexed temporal logics.
  5. Process algebras. A generalized view on process algebras, their relation to state spaces, operators of hiding and parallel composition. The different process algebraic equivalences and preorders, possibilities of evaluating them.
  6. Computational complexity of formal analysis and verification tasks. Complexity w.r.t. the size of state spaces and w.r.t. the size of models. The relation of time and space requirements of formal analysis and verification methods.
  7. State space reduction. An overview of the various approaches to reducing state spaces, combining state space generating and reducing algorithms with algorithms analyzing the state spaces. Abstracting and transforming models. Compositionality.
  8. State space reduction. Binary decision diagrams and symbolic methods. Bitstate hashing. Reducing state spaces using symmetries in the behaviour of the modelled systems. Partial order reduction methods.
  9. Computer-aided tools supporting formal analysis and verification using state spaces. Spin, Slam, Java PathFinder, Zing, SMV, etc. (according to the state of the art).
  10. An overview of successful applications of formal analysis and verification in the area of embedded systems, protocol engineering, control systems, workflow, etc.
  11. Real time systems. Logical and physical time. Safety, liveness, and feasibility in real time. Modelling and specification languages in the domain of real time, timed automata, real time temporal logics.
  12. Dealing with state spaces of systems working in real time, regions, zones. Automated support for formal analysis and verification of real time systems (Uppaal, Kronos, TReX, ...) and their applications. Hybrid systems (HyTech).
  13. Theorem proving. Principles, automated support (PVS, etc.), applications. Combining theorem proving and methods based on state spaces
Syllabus - others, projects and individual work of students:
 
  • Two home assignments devoted to creating a model of a simple system and validating its behaviour by means of two chosen tools for formal analysis and verification (Spin, Zing, SMV, JPF, INA, Uppaal, TReX, PVS, etc.).
Fundamental literature:
 
  • Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
  • Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
  • Valmari, A.: The State Explosion Problem. In Reisig, W., Rozenberg, G.: Lectures on Petri Nets I: Basic Models, volume 1491 of Lecture Notes in Computer Science, pages 429--528. Springer-Verlag, 1998.
Study literature:
 
  • Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
  • Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
  • Valmari, A.: The State Explosion Problem. In Reisig, W., Rozenberg, G.: Lectures on Petri Nets I: Basic Models, volume 1491 of Lecture Notes in Computer Science, pages 429--528. Springer-Verlag, 1998.
  • Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall, 1991. (freely available on the Internet)
  • Materials presented within the lectures and made accessible via the Internet.
  • Materials freely accessible on the Internet, especially papers and documentation related to the various computer-aided tools for formal analysis and verification.
Progress assessment:
  
  • Two evaluated home assignments - each for 15 points.
  • A final written examination - 70 points.
  • To be allowed to sit for the written examination, a student is to earn at least 15 points during the semester.
  • The passing boundary w.r.t. the ECTS assessment - 50 points.
Exam prerequisites:
  Having at least 50% of the possible point evaluation of the homeworks.
 

Your IPv4 address: 107.20.10.203
Switch to https

DNSSEC [dnssec]