Formal Verification of Reactive Systems, 7.5 credits

Formal Verification of Reactive Systems, 7.5 credits

All Courses Software Testing

The aim of the course is to introduce the participants into methods and tools for verifying systems that need to react to external stimuli. The methods use system models with precise formal semantics and will span model-checking as well as deductive verification. A set of simple examples as well as real-world applications will be used throughout the course to illustrate the methods and their tool support. The objective of the course is to understand the underpinning theories of formal verification, and learn how to apply tool support in order to verify system models.

Responsible: Mälardalen University (Cristina Seceleanu)

Course modules:

  1. Basic concepts of formal modeling: automata models, formalization of system properties
  2. Automated verification of formal models: model-checking, deductive verification
  3. Application of tools to formal models and code

Learning outcomes: At the end of the course any participant should be able to:

  • Understand the differences between algorithmic and deductive verification
  • Formalize requirements in temporal logic or predicate logic
  • Model functional and timing behavior of reactive systems
  • Apply formal verification tools (such as UPPAAL and variants) to check properties of models

Course content: This course consists of lectures and assignments that will teach the participants the basics of formal verification, differences between techniques, as well as their potential applicability to real-world systems.

The course will cover both discrete as well as timed systems, and will show the application of techniques on some prototype examples from industry.

Related Industrial Challenges Addressed in the Course:

  • Uncover at early design stages potential trouble-spots / errors in design
  • Provide design-space exploration automated support
  • Increase assurance of future implementations

Upcoming instances: September 2017, ’18

More info:

  • Course title in Swedish: Formell verifiering av reaktiva system
  • Course code: DVA457 (at MdH), MDH-24116 (at antagning.se)
  • Course syllabus at Mälardalen University
  • Autumn 2017 instance at Mälardalen University
  • Apply at antagning.se
  • Admission requirements: 120 credits of which at least 80 credits in Computer Science and / or equivalent. In addition, at least 18 months of documented work experience in software development.