Text

Kvalitetssäkring - Upptäcka fel genom formell verifiering

  • Högskolepoäng 7.5  hp
  • Utbildningsnivå Avancerad nivå
  • Studieort Distans utan obligatoriska träffar
  • Kurskod DVA468
  • Huvudområde Datavetenskap

 

Kursen ger 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. Syftet är att ge förståelse för de underliggande teorierna för formell verifiering samt att lära sig hur man använder verktygsstöd för att verifiera systemmodeller.

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


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. Den omfattar modellering och verifiering av både diskreta och tidsstyrda system, samt verifiering av programkod. Kursen innehåller 4 moduler:

Modul 1: Modellering och verifiering av otidsanpassade system

Modul 2: Modellkontroll av realtidssystem

Modul 3: Logik och deduktiv verifiering av system

Modul 4: Specifikation och verifiering av kod


Du lär dig

  • 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


Behörighet

I faktarutan nedan ser du vilken behörighet som krävs för att läsa kursen. 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.

Tillfällen för denna kurs

Hösttermin 2023

  • Hösttermin 2023

    Omfattning

    7.5 hp

    Tid

    2023-09-11 - 2024-01-14 (deltid 25%)

    Utbildningsnivå

    Avancerad nivå

    Kurstyp

    Fristående kurs

    Anmälningskod

    MDU-24539

    Språk

    Engelska

    Studieort

    Ortsoberoende

    Undervisningsform

    Distans
    Antal obligatoriska träffar inklusive tentamen: 0
    Antal övriga fysiska träffar: 0

    Särskild behörighet

    120 hp, varav 80 hp inom teknik eller informatik, inklusive minst 30 hp programmering eller mjukvaruutveckling. Dessutom krävs Svenska B/Svenska 3 samt Engelska A/Engelska 6. I de fall kursen ges på engelska görs undantag från Svenska B/Svenska 3.

     
     

    Urval

    Antal högskolepoäng

Frågor kring utbildningen?

Hör av dig till kursansvarig om du har frågor kring kursens innehåll.

Information om anmälan

Efter att du anmält dig behöver du eventuellt komplettera med dokument för att styrka din behörighet. Alla kompletteringar laddas upp på antagning.se.

De flesta svenska akademiska meriter hämtas automatiskt. Vänta några dagar efter att du gjort din anmälan – om dina akademiska meriter fortfarande inte syns på Mina sidor på antagning.se laddar du upp kopia på dem. Om du har utländska meriter måste du ladda upp kopia på dem på antagning.se.

Om kursen du söker har krav på yrkeserfarenhet behöver du ladda upp ett tjänstgöringsintyg som är underskrivet av din arbetsgivare. Du hittar mall för tjänstgöringsintyg nedan som du kan använda om du vill.

Inga akademiska meriter?

Många kurser kräver att du har tidigare akademiska studier. Du som inte har det men som har yrkeserfarenhet eller andra studier inom området kan bedömas på så kallad reell kompetens. Det innebär att det görs en bedömning av både formella meriter (betyg, examensbevis) och yrkeserfarenhet. Bedömningen görs för att avgöra om du har kunskaper som gör det möjligt att klara kursen. Om du anser att du har kompetensen som krävs för kursen, ska du fylla i en CV/kompetensbeskrivning, mall finns nedan. Den ska innehålla:

  • Utbildningar
  • Relevant och aktuell arbetslivserfarenhet
  • Kunskaper i engelska
  • Övrigt du vill åberopa

Tänk på att ge en beskrivning av dina arbetsuppgifter, inte bara en titel.

Du behöver också ett underskrivet tjänstgöringsintyg från din arbetsgivare, mall att ladda ner finns nedan.

När du fyllt i dokumenten laddar du upp dem på antagning.se.

Om du har frågor om anmälan eller behörighet är du välkommen att kontakta oss genom att mejla till lifelonglearning@mdu.se