Title:  Formal Analysis and Verification 

Code:  FAV 

Ac.Year:  2007/2008 

Sem:  Winter 

Curriculums:  

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/sem  Lectures  Seminar Exercises  Laboratory Exercises  Computer Exercises  Other 

Hours:  26  0  0  0  26 

 Exams  Tests  Exercises  Laboratories  Other 

Points:  60  0  0  0  40 



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:  

 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 safetycritical 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 computeraided
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 computeraided 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
safetycritical systems. Students know capabilities and the basic
ways of using computeraided 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: 


 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.
 State spaces, state space paths, abstractions of states and
transitions. Interleaving and true concurrency. Linear and branching
time. Safety, liveness, and fairness.
 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.
 Temporal logics. LTL, CTL, CTL*, mucalculus. The relation of temporal logics and automata. Indexed temporal logics.
 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.
 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.
 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.
 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.
 Computeraided tools supporting formal analysis and
verification using state spaces. Spin, Slam, Java
PathFinder, Zing, SMV,
etc. (according to the state of the art).
 An overview of successful applications of formal analysis
and verification in the area of embedded systems, protocol engineering,
control systems, workflow, etc.
 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.
 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).
 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 429528. SpringerVerlag,
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 429528. SpringerVerlag,
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 computeraided 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.  
