Text

Quality assurance - Catching bugs by formal verification

  • Credits 7.5  credits
  • Education ordinance 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 this course
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.

Course modules:

* Basic concepts of formal modeling: automata models, formalisation of system properties
* Automated verification of formal models: model-checking, deductive verification
* Application of tools to formal models and code

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

Syftet med kursen är att ge dig en introduktion till metoder och verktyg för system- och programverifiering. Metoderna använder systemmodeller med precis formell semantik och omfattar såväl modellkontroll som deduktiv verifiering.

En uppsättning av enkla exempel såväl som applikationer kommer att användas genom hela kursen för att illustrera metoderna samt deras verktygssupport. Kursens syfte är att förstå de underliggande teorierna för formell verifiering samt att lära sig hur man använder verktygsstöd för att verifiera systemmodeller.

Om kursen

Kursen består av föreläsningar och uppgifter där du lär dig grunderna i formell verifiering, skillnader mellan olika tekniker samt deras möjliga tillämpbarhet i verkliga system.

Kursen omfattar såväl diskreta som tidsberoende system och visar hur olika tekniker kan tillämpas på några prototyper från industrin.

Delkurser:

  • Grundläggande begrepp i formell modellering: automata modeller, formalisering av systemegenskaper
  • Automatiserad verifiering av formella modeller: modellkontroll, deduktiv verifiering
  • Användningen av verktyg för formella modeller och kod

Du kommer att lära dig att

  • Förstå skillnaderna mellan algoritmisk och deduktiv verifiering
  • Formalisera kraven i temporallogik och predikatlogik
  • Modellera funktions- och tidsbeteende hos reaktiva system
  • Tillämpa formella verifieringsverktyg (såsom UPPAAL samt varianter) för att kontrollera egenskaper hos modeller

Relaterade industriella utmaningar som behandlas i kursen

  • Upptäcka potentiella problem/designfel i tidiga designstadier
  • Automatiserat stöd vid val av design (Design space exploration)
  • Öka säkerheten för framtida implementationer

Särskild behörighet

120 hp, varav 80 hp inom teknik eller informatik, inklusive minst 30 hp programmering eller mjukvaruutveckling. Dessutom krävs Engelska A/Engelska 6.

Om du inte uppfyller de formella behörighetskraven kan du få din behörighet bedömd på kunskap och kompetens som du har fått på annat sätt, såsom arbetslivserfarenhet, övriga studier m.m. Läs mer under Information om anmälan.

Undervisningsspråk

Engelska

Occasions for this course

Autumn semester 2021

  • Autumn semester 2021

    Scope

    7.5 credits

    Time

    2021-09-13 - 2022-01-16 (part time 25%)

    Education ordinance

    Second cycle

    Course type

    Independent course

    Application code

    MDH-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

    Applicants with at least 12 month (full-time) documented work-experience from software development have priority. Other applicants are ranked by university credits.

Questions about the course?

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

Senior Lecturer

Cristina Seceleanu

+4621151764

cristina.seceleanu@mdh.se

To top