2D5333 Programverifiering,

Doktorandkurs 4p
som rekommenderas för teknologer på D, F och E,
och för lärare i programmeringskurser.

Bakgrund

Det finns många metoder att producera fungerande program, särskilt när programmen inte är särskilt stora eller när tillförlitlighetskraven inte är extrema. När kraven är absoluta och programmen är stora finns bara en användbar metod: matematiska resonemang uppstyrda av datoriserade och organisatoriska kontrollprocedurer.

Forskning kring programverifiering har varit intensiv under de senaste 30 åren, men resultaten har inte använts i industriell skala förrän på sista tiden, och huvudsakligen i tillämpningsområdet styrning av tekniska system med höga säkerhetskrav. Exempel på sådana system är kärnkraftverk, tågsignalsystem, passagerarflygplan och telekommunikationssystem.

Avsikten med kursen är att ge ett litet antal goda exempel på metoder för stringent analys av program och programsystem som också är tillämpliga på tekniska system i stort, att ge en bild av områdets utveckling sedan von Neumanns och Floyds pionjärinsatser, och att ge praktiska erfarenhet av något eller några akademiskt användbara verktyg.

Förkunskapskrav

Jag förutsätter att du är intresserad av kursens målsättning och har vana vid och intresse av matematiska resonemang, liksom kunskap om programspråk (gärna C), matematisk statistik (liten kurs), logik (liten kurs, ev från tillämpningskurs) datastrukturer och algoritmer (liten kurs).

Målsättning

Efter kursen ska deltagare

Preliminärt innehåll:

  1. Mål och verktyg för matematisk metodik, vanliga misstag och missuppfattningar. Intention, Specifikation och Program - relationer mellan dessa.
  2. Partiell och total korrekthet, avslutning. Intermittent assertions och Hoare-axiomatisering.
  3. Programverifiering kombinerad med konstruktion: Förfining(refinement).
  4. Mekaniserade verifieringssystem: Larch, HOL, ISABELLE , nuprl, mfl. Stödsystem.
  5. Specifikation av dynamiska egenskaper. Exekveringsträd, temporal- och MS-logik.
  6. Utveckling(unfolding), modellkontrollering(model checking) Verifiering av distribuerat system
  7. Program i tekniska system: Reliability/Maintainability problematiken, Markovmodellering. Industriella standarder för tillförlitliga system.

Examination.

Redovisning av läsuppgifter, labbar och hemtal. Närvaro eller muntlig redovisning av teoristoffet.

Uppläggning 1996 (per 4) ... Ingång till Nadas kursweb

Stefan