vissza a tantárgylistához   nyomtatható verzió    

    Formal Methods

    A tantárgy neve magyarul / Name of the subject in Hungarian: Formális módszerek

    Last updated: 2018. február 22.

    Budapest University of Technology and Economics
    Faculty of Electrical Engineering and Informatics
    Computer Engineering, MSc program
    Course ID Semester Assessment Credit Tantárgyfélév
    VIMIMA07 1, 2 3/0/0/f 4  
    3. Course coordinator and department Dr. Majzik István,
    Web page of the course https://www.mit.bme.hu/eng/oktatas/targyak/vimima07
    4. Instructors dr. István Majzik, Associate Professor, BME MIT
    6. Pre-requisites
    Kötelező:
    NEM ( TárgyEredmény( "BMEVIMIM100" , "jegy" , _ ) >= 2
    VAGY
    TárgyEredmény("BMEVIMIM100", "FELVETEL", AktualisFelev()) > 0
    VAGY
    TárgyEredmény( "BMEVIMIMA26" , "jegy" , _ ) >= 2
    VAGY
    TárgyEredmény("BMEVIMIMA26", "FELVETEL", AktualisFelev()) > 0)

    A fenti forma a Neptun sajátja, ezen technikai okokból nem változtattunk.

    A kötelező előtanulmányi rend az adott szak honlapján és képzési programjában található.

    7. Objectives, learning outcomes and obtained knowledge
    As the complexity of information systems and the costs of potential failures are increasing, it becomes more and more important to prove that the design of the critical system components is correct. One of the typical solutions for the challenge of provably correct design is the application of formal methods. Mathematically precise formal models allow the precise and unambiguous specification of requirements and construction of designs; formal verification allows the checking of design decisions and proof of design properties; while the verified models allow automated software synthesis. The subject provides an overview of the formal background needed for the elaboration and analysis of the formal models of IT components and systems: the modelling paradigms, the widely used formal modelling languages, and the related verification and validation techniques. The subject demonstrates the application of formal methods in the field of requirement specification, system and software design, model based verification and source code synthesis.
    The participants of the course who pass the requirements will be able to
    - understand and apply various formal methods;
    - construct formal models on the basis of informal descriptions;
    - understand the advantages and disadvantages of various formal verification techniques;
    - and apply tools that support the application of formal methods.

    8. Synopsis
    - Formal modelling and analysis of information systems (introduction to the subject): The role of formal methods during the design and development of IT systems: formal requirement specification, modelling, verification (model checking and proof of correctness). The relation of engineering and formal models, model transformations. Design environments that support the application of formal methods (e.g., SCADE).
    - Basic formal models and their semantics: Kripke-structures, transition systems, timed automata, network of timed automata.
    - Formalization of requirements: Temporal logics: linear time temporal logic (LTL), branching time temporal logics (CTL, CTL*). The comparison of their expressiveness. Practical examples and applications: the Property Specification Language.
    - Formal verification using model checking: Model checking by the tableau method. Symbolic model checking. The representation of the state space using reduced ordered binary decision diagrams. Bounded model checking. Verification of time dependent behaviour. Practical applications: Modelling embedded controllers using timed automata, verification of temporal properties, automated test case generation using model checkers. The UPPAAL model checker.
    - Modelling state-dependent dynamic behaviour: The formal syntax and semantics of statecharts. Design using statecharts, the formal verification of properties. The typical patterns for software synthesis. Practical applications: UML 2 statecharts, software source code generation and monitor synthesis.
    - Modelling and analysis of concurrent systems: The Petri-net formalism. Dynamic properties of Petri-net models (e.g., safety, liveness, boundedness). The verification of dynamic properties by simulation or on the basis of the reachability graph. Structural properties (e.g., conservativeness, consistency, invariants) and their analysis on the basis of the state equation. Property preserving model reduction techniques. Hierarchical Petri-nets. Modelling examples.
    - Modelling data-dependent behaviour: The extension of Petri-nets with data types and data processing. The adaptation of the definitions of dynamic and structural properties. Practical applications: Analysis of the consistency of distributed data processing, protocol verification.
    - Specification and verification of extra-functional properties: The extension of Petri-nets with probabilities and time: Stochastic Petri-nets. Formalization of properties using stochastic temporal logic. Verification of performance and dependability properties.
    - Modelling data processing: The syntax and semantics of data flow networks. Model refinement, checking the consistency of model refinement. The application of data flow networks for modelling and analysis of business processes.
    - Formal verification based on software source code: Model checking C programs. The use of abstraction: static analysis using abstract interpretation, predicate abstraction, counter-example guided abstraction refinement in model checking.
    9. Method of instruction Lectures.
    10. Assessment
    - During the semester: The requirements for passing the subject are 2 successful midterm exams and a successful homework assignment. The homework assignment includes modelling of a small-scale IT system and the verification of its required properties. The homework is assigned on the 4th week of the semester and it has to be submitted and presented from the 10th week of the semester. The final result is calculated from the results of the two midterm exams (35-35%) and the result of the homework (30%).
    - In the examination period: -
    11. Recaps Each midterm exam can be repeated once. The homework assignment can be submitted during the repetition period, but this late submission will result in 20% decrease of the score.
    12. Consultations Consultations regarding the homework are offered by appointment.
    13. References, textbooks and resources
    - Pataricza András (editor): Formális módszerek az informatikában. Második kiadás, TypoTeX Kiadó, 2006. (in Hungarian)
    - G. Behrmann, A. David, K. G. Larsen: A Tutorial on UPPAAL 4.0. http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf
    Recommended:
    - D. Peled: Software Reliability Methods. Springer Verlag, 2001.
    - B. Berard et al.: Systems and Software Verification: Model-Checking Techniques and Tools. Springer Verlag, 2010.
    - E. M. Clarke, O. Grumberg, D. Peled:  Model Checking. MIT Press, 1999.
    - W. Reisig, G. Rozenberg (eds.): Lectures on Petri Nets. Vol I-II, Springer Verlag, 1998.

    14. Required learning hours and assignment
    Contact hours (lectures)42
    Study during the semester12
    Preparation for midterm exams32
    Preparation of homework22
    Study of written material12
    Total120
    15. Syllabus prepared by
    Dr. István Majzik, Associate Professor, BME MIT
    Dr. Tamás Bartha, Associate Professor, BME MIT
    Dr. András Pataricza, Professor, BME MIT