• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site
For visually-impairedFor visually-impairedUser profile (HSE staff only)Search
Advanced search
Menu
HSE University
User profile (HSE staff only)Search
Advanced search

Course Syllabus

Master 2019/2020

Formal Methods in Software Engineering

Category 'Best Course for New Knowledge and Skills'
Type: Compulsory course (System and Software Engineering)
Area of studies: Software Engineering
Delivered by: School of Software Engineering
Where: Faculty of Computer Science
When: 1 year, 1-4 module
Mode of studies: offline
Instructors: Irina A. Lomazova, Roman Nesterov
Master’s programme: Software and Systems Engineering
Language: English
ECTS credits: 10
Contact hours: 128

Course Syllabus

Full Syllabus

Abstract

In computer science and software engineering, formal methods are a particular kind of mathematically based techniques for the specification, development and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the fact that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design. Formal methods are best described as the application of a fairly broad variety of theoretical computer science fundamentals, in particular logic calculi, formal languages, automata theory, and program semantics, but also type systems and algebraic data types to problems in software and hardware specification and verification. Formal methods can:  be a foundation for describing complex systems.  be a foundation for reasoning about systems.  provide support for program development. In contrast to other system design approaches, formal methods use mathematical proof as a complement to system testing in order to ensure correct behavior. As systems become more complicated, and safety becomes a more important issue, the formal approach to system design offers another level of insurance. Formal methods differ from other design methods by the use of formal verification schemes, the basic principles of the system must be proven correct before they are accepted. Traditional system design uses extensive testing to verify behavior, but testing is capable of only finite conclusions. E. Dijkstra and others have demonstrated that tests can help to find fails and bugs, but cannot guarantee their absence. In contrast, once a theorem is proven true it remains true. It is very important to note that formal verification does not obviate the need for testing. Formal verification cannot fix bad assumptions in the design, but it can help identify errors in reasoning which would otherwise be left unverified. In several cases, engineers have reported finding flaws in systems once they reviewed their designs formally.
Learning Objectives

Learning Objectives

  • The purpose of this course is to learn how to specify behavior of systems and to experience the design of a system where you can prove that the behavior is correct.
Expected Learning Outcomes

Expected Learning Outcomes

  • To model various classes of distributed systems within appropriate formalisms
  • To model various classes of distributed systems within appropriate formalisms;
  • To interpret and apply the formal languages of the formalisms for modeling distributed systems
  • To apply specific techniques for the analysis and verification of distributed systems;
  • To formulate and prove properties of distributed systems within studied formalisms
Course Contents

Course Contents

  • Formal methods as a basis for software reliability
  • Floyd method for verification of sequential programs. Hoare axiomatic semantics for sequential and parallel programs.
  • Finite state machines (FSMs): basic definitions, operational semantics. Categories of FSMs. Extended FSMs. Modeling concurrent systems with communicating FSMs.
  • Petri nets: basic notions, definitions and classification. Modeling distributed systems with Petri nets.
  • Petri nets analysis. Checking structural and behavioral properties.
  • High-level Petri nets. Colored Petri nets and CPNTools.
  • Modeling distributed and concurrent system with process algebras. Structured operational semantics and its formalization (SOS). Algebra CCS: syntax, semantics, modeling technique.
  • The notion and properties of bisimilarity relation.
  • Verifying reactive concurrent systems with CCS. Hennesy-Milner logic and temporal properties. The notion of fixed point and Tarski’s fixed point theorem
  • Transition systems and program graphs. Nondeterminism, parallelism and communication. Peterson algorithm
  • Specifying distributed systems with Promela. Spin model checker.
  • Temporal logics LTL and CTL for specification of behavioral properties of reactive systems.
  • Automata-based approach for verification of LTL formulae.
  • Model checking algorithm for verification of CTL formulae
Assessment Elements

Assessment Elements

  • non-blocking O_accum1
  • non-blocking O_exam1
  • non-blocking O_cuurent2
  • non-blocking O_htask
  • non-blocking O_exam2
    Письменный экзамен с помощью MS Teams / MS Forms - студенты авторизуются по студенческой почте в домене edu.hse.ru Технические требования: web-камера, микрофон, наушники / колонки
Interim Assessment

Interim Assessment

  • Interim assessment (2 module)
    0.5 * O_accum1 + 0.5 * O_exam1
  • Interim assessment (4 module)
    The result grade after the 1st term is calculated by the formula: Оterm 1 = 0,5 ∙ Оaccum1 + 0,5 ∙ Оexam1, where Оaccum1 is the accumulated grade composed of grades for the current work (quick tests, assignments, work in the classroom) during modules 1 and 2; Оexam1 is the grade for the intermediate exam. Rounding is done by “round half up” rule. The final course grade is calculated by the following formulae: Оaccum2 = 0,5 ∙ Оcurrent2 + 0,3 ∙ Оh_task + 0,2 ∙ Оterm1 and Оfinal = 0,6 ∙ Оaccum2 + 0,4 ∙ Оexam2, where Оcurrent2 is the grade for the current work (quick tests, assignments, work in the classroom) during modules 3 and 4; Оh_task is the grade for the home task, Оterm1 is the result grade after the 1st term, and Оexam2 is the grade for the final exam after module 4. Rounding is done by “round half up” rule.
Bibliography

Bibliography

Recommended Core Bibliography

  • Baeten, J. C. M., Reniers, M. A., & Basten, T. G. H. (2010). Process Algebra: Equational Theories of Communicating Processes. Cambridge: Cambridge University Press. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=317653
  • Baier, C., & Katoen, J.-P. (2008). Principles of Model Checking. Cambridge, Mass: The MIT Press. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=226091
  • Fisher, M. (2011). An Introduction to Practical Formal Methods Using Temporal Logic. Chichester, West Sussex, U.K.: Wiley. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=509889
  • Jensen, K., & Kristensen, L. M. (2009). Coloured Petri Nets : Modelling and Validation of Concurrent Systems. Dordrecht: Springer. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=285464

Recommended Additional Bibliography

  • Wan Fokkink, Jan Friso Groote, & Michel Reniers. (2003). Modelling Distributed Systems. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsbas&AN=edsbas.E2E909CB
  • Wil van der Aalst, & Kees van Hee. (2004). Workflow Management: Models, Methods, and Systems. The MIT Press. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsrep&AN=edsrep.b.mtp.titles.0262720469