Formella metoder i mjukvaruutveckling

Om utbildningen

Kursens syfte är att lära ut kunskap, teknik och omdöme angående viktiga tekniker inom formella metoder: modellkontroll (model checking) och deduktiv verifikation. Båda stilarna introduceras på tre sätt: konceptuellt, teoretisk och praktiskt, genom användning av ett specifikt verktyg. Kursen bygger på kunskap om första ordningens logik och temporallogik, och visar hur dessa formalismer kan appliceras, och utökas för verifikation av mjukvara. För modellkontroll täcker kursen följande ämnen: \- ett specifikationsspråk för parallella processer, \- verifiering av påståenden, \- synkronisering, \- verifikation av säkerhets- och livenessegenskaper som är skrivna i temporal logik. För deduktiv verifikation täcker kursen följande ämnen: \- ett specifikationsspråk på enhetsnivå för Java-program, \- en logik för verifikation av Java-program, \- verifikation av Java-program, i meningen att implementationen av en enhet uppfyller dess specifikationen.

Behörighet

Godkända kurser om 120 hp i ämnet Datavetenskap, eller motsvarande, särskilt DIT201 Logic in Computer Science, 7,5 hp, och en 7,5 hp kurs i objektorienterad programmering (eller motsvarande) är ett krav. Följande kunskapsnivå i Engelska krävs: Engelska 6/Engelska nivå 2 eller motsvarande från ett erkänt internationellt test, t.ex. TOEFL, IELTS.

Rekommenderade förkunskaper: uh

Alla tillfällen (1)

Liknande utbildningar

• Formella metoder för säkerhetUniversitet/högskola
• Testning, felsökning & verifieringUniversitet/högskola
• Kvalitetssäkring - Upptäcka fel genom formell verifieringUniversitet/högskola
• Datavetenskapens grunderUniversitet/högskola