Text

Quality assurance - Catching bugs by formal verification

  • Credits 7.5  credits
  • Education level Second cycle
  • Study location Distance with no obligatory meetings
  • Course code DVA468
  • Main area Computer Science

 

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.

About the course

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

The course will cover modeling and verification of both discrete and timed systems, as well as verification of program code. The course includes four modules:

Module 1: Modeling and Verification of Untimed Systems

Module 2: Model checking Real-time Systems

Module 3: Logics and Deductive Verification of Systems

Module 4: Specification and Verification of Code

You will learn to

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 systems
  • apply verification tools (such as UPPAAL and Dafne) to check properties of models and code, respectively.

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

Requirements

Below you find the entry requirements for the course. If you do not fulfill the requirements, you can get your eligibility evaluated based on knowledge acquired in other ways, such as work experience, other studies etcetera. Read more in Application information below.

Occasions for this course

Autumn semester 2024

  • Autumn semester 2024

    Scope

    7.5 credits

    Time

    2024-09-16 - 2025-01-19 (part time 25%)

    Education level

    Second cycle

    Course type

    Freestanding course

    Application code

    MDU-24539

    Language

    English

    Study location

    Independent of location

    Teaching form

    Distance learning
    Number of mandatory occasions including examination: 0
    Number of other physical occasions: 0

    Course syllabus & literature

    See course plan and literature list (DVA468)

    Specific requirements

    120 credits, of which 80 credits in engineering or informatics, including at least 30 credits in computer science or software development. In addition, Swedish course B/Swedish course 3 and English course A/English course 6 are required. For courses given entirely in English, exemption is made from the requirement in Swedish course B/Swedish course 3.
     
     
     

    Selection

    University credits

Questions about the course?

If you have any questions about the course, please contact the Course Coordinator.

Application information

You’ll find the entry requirements in the course description. After submitting your application, the next step is to submit documentation to demonstrate your eligibility for the course. Most academic credentials from Sweden are retrieved automatically. Wait a few days after submitting your application - if you still can’t see your academic credentials om My pages, please upload them.

If you have studied in another country, you must provide transcripts of your academic studies and of your English proficiency. Exactly what you need to submit and how, depends on several factors. You can read more on universityadmissions.se or antagning.se.

If the course requires work experience, you need to provide an employer’s certificate. You can download a template for employer’s certificate below.

No academic qualifications?

Many courses requires that you have previous academies studies, but we can validate work experience to determine whether you have the qualifications for the course.

If you don’t have the formal qualifications required, please send in a certificate of employment (current or previous) and a CV/Description of competence that describes your educational and professional background. Please include a short description of your work experience, not only the work title.

Use the CV/ Description of competence template below and fill in the information requested.

You can also use our template for Employers certificate if you like.

Download a template for CV/Description of competence Word, 45.5 kB, opens in new window.

Download a template for Employers certificate Word, 38 kB, opens in new window.

If you have any questions regarding eligibility or application please send an e-mail to lifelonglearning@mdu.se