Text

Kvalitetssäkring - Upptäcka fel genom formell verifiering

  • Högskolepoäng 7.5 hp
  • Studieort Ortsoberoende
  • $stringTranslations.StartDate 2021-09-13 - 2022-01-16 (deltid 25%)
  • Utbildningsnivå Avancerad nivå
  • Kurskod DVA468
  • Huvudområde Datavetenskap

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

Lärare

Universitetslektor

Cristina Seceleanu

021-15 17 64

cristina.seceleanu@mdh.se

Kursplan

Du kan läsa i detalj om utbildningen, dess innehåll och litteratur m.m. i kursplanen

Se kursplan

Anmäl dig till kursen

Kvalitetssäkring - Upptäcka fel genom formell verifiering

Till anmälan

Information om anmälan

Efter att du anmält dig behöver du eventuellt komplettera med dokument för att styrka din behörighet. De flesta svenska akademiska meriter hämtas automatiskt. Vänta några dagar efter att du skickat in din anmälan – om dina akademiska meriter fortfarande inte syns på Mina sidor ska du ladda upp dem. Om du har utländska meriter behöver du ladda upp kopia på dem på antagning.se.

Vissa kurser kräver yrkeserfarenhet. Om kursen du söker har krav på yrkeserfarenhet måste 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?

Kursen kräver att du har tidigare akademiska studier. Du som inte har det men har yrkeserfarenhet 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 motsvarar behörighetskraven på 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 kort 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.

Ladda ner mall för CV/Kompetensbeskrivning Word, 27.6 kB, opens in new window.

Ladda ner mall för Tjänstgöringsintyg Word, 25.5 kB, opens in new window.

Om du har frågor om anmälan är du välkommen att kontakta oss genom att mejla till lifelonglearning@mdh.se

Prompt

Kurserna ingår i projektet Prompt där MDH erbjuder kurser på masternivå som ges online utan fysiska träffar och som är flexibla i tid och rum för att de ska vara möjliga att kombinera med yrkeslivet.

Kompetensutveckling med Prompt
Till toppen