Přístupnostní navigace
E-application
Search Search Close
Course detail
FIT-FAVAcad. year: 2009/2010
Formal analysis and verification as a modern complement and/or alternative to validating properties of systems by means of simulation or testing. Model checking - formal verification based on a systematic state space exploration. Selected modelling, query, and specification languages. Various approaches to state space reductions. Methods of automated abstraction of systems being examined, especially predicate abstraction. Automated theorem proving, decision procedures, modern methods of SAT and SMT solving and their aplications in formal analysis and verification. Static analysis based on looking for error patterns, data flow analysis, and abstract interpretation. A brief description of several advanced computer-aided tools for formal analysis and verification: SMV, Spin, Slam, Blast, Java PathFinder, ARMC, FindBugs, 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).
Language of instruction
Number of ECTS credits
Mode of study
Guarantor
Department
Learning outcomes of the course unit
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.
Prerequisites
Co-requisites
Planned learning activities and teaching methods
Assesment methods and criteria linked to learning outcomes
Having at least 50% of the possible point evaluation of the homeworks.
Course curriculum
Work placements
Aims
Specification of controlled education, way of implementation and compensation for absences
Recommended optional programme components
Prerequisites and corequisites
Basic literature
Recommended reading
Classification of course in study plans
branch MBI , 0 year of study, winter semester, electivebranch MBS , 0 year of study, winter semester, compulsory-optionalbranch MGM , 0 year of study, winter semester, electivebranch MGM , 0 year of study, winter semester, electivebranch MIN , 0 year of study, winter semester, compulsory-optionalbranch MIN , 2 year of study, winter semester, electivebranch MIS , 0 year of study, winter semester, compulsory-optionalbranch MIS , 0 year of study, winter semester, electivebranch MMI , 0 year of study, winter semester, electivebranch MMM , 1 year of study, winter semester, compulsorybranch MPS , 2 year of study, winter semester, electivebranch MPV , 0 year of study, winter semester, electivebranch MSK , 2 year of study, winter semester, compulsory-optional
Lecture
Teacher / Lecturer
Syllabus
Project