Kvalitetssäkring - Upptäcka fel genom formell verifiering

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.

Det här är en kurs på avancerad nivå för dig som har tidigare högskolepoäng och är yrkesverksam. Den är utvecklad för att passa dig som arbetar och vill kunna kombinera studier och arbete.

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. En uppsättning av enkla exempel såväl som applikationer kommer att användas 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 för att lära dig hur du använder verktygsstöd för att verifiera systemmodeller.

Kursen innehåller 4 moduler:

1. Modellering och verifiering av otidsanpassade system
2. Modellkontroll av realtidssystem
3. Logik och deduktiv verifiering av system
4. Specifikation och verifiering av kod

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

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".

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.

Ladda ner mallen CV/Kompetensbeskrivning

Ladda ner mallen Tjänstgöringsintyg

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