I00072 (I00072)
Processen*
< 2006/2007 > 05-02-2007 t/m 01-07-2007 () L
Informatica - Master variant MT (2005) Keuze informatica (6 ec)
omvang
6 ec (168 uur) : 32 uur plenair college, 32 uur groepsgewijs college, 0 uur computerpracticum, 0 uur 'droog' practicum, 0 uur gesprekken met de docent, 0 uur onderling overleg met medestudenten (werkgroepen, projectwerk e.d.), 104 uur zelfstudie
investering
6 ec * 28 u/ec + #std * (1 + 6ec * 0.15 u/student/ec)
inzet tentatief

examinator
afdeling
tijdbesteding

prof. dr. Henk Barendregt
sws
95u.

speciale web-site

 

Een modulaire taal ontwikkelen voor processen.

Leerdoelen

Het specifieren, implementeren en verifieren van relatief eenvoudige processen.

Onderwerpen

1. Basis Proces Algebra. In dit systeem worden "+" (som van processen, keuze) en "." (product van processen, sequentiele compositie) gedefinieerd. Samen met recursie kunnen we zo al veel interessante processen krijgen, zoals de Stack en de Counter. 2. PA, Proces Algebra met interleaving operator "||". Processen kunnen nu parallel werken en hun acties door elkaar heen doen (interleaving). Het proces Bag is nu definieerbaar. 3. ACP, (Algebra of Communicating Processes). Dit is procesalgebra met communicatie. Het vorige systeem wordt nu uitgebreid met een communicatie-mechanisme. Acties zijn niet meer altijd op zichzelf staand, maar kunnen een communicatiepaar vormen. Het toepassingsgebied is nu veel rijker dan in het vorige systeem. Een typische operator is de encapsulatie-operator, en het proces 'deadlock' doet zijn intree. 4. In het vorige systeem ontbreekt nog de mogelijkheid van abstractie van acties ('hiding'). Dit voegen we nu toe, waardoor het mogelijk wordt hierarchisch opgebouwde systemen van processen te beschrijven. Ook wordt nu duidelijk hoe de relatie is tussen implementatie, specificatie, en verificatie van processen. Als typisch voorbeeld behandelen we Milner's Scheduler. 5. Als semantiek van de axioma-systemen voor processen die tot nu toe zijn behandeld, nemen we het model van procesgrafen met 'branching bisimulatie'. 6. We bespreken met de bovenstaande gereedschappen de verificatie van een simpel communicatie-protocol, zoals het 'Alternating Bit Protocol', het 'Sliding Window Protocol', of het Bakery Protocol'. 7. (Optioneel). Aandacht kan worden geschonken aan de speficatietaal mu-CRL, die op bovenstaande procesalgebra is gebaseerd en die wordt gebruikt in vele praktische implementaie/specificatie/verificatie-projecten, ook in industriele contexten. 8. (Optioneel) Aandacht kan worden geschonken aan de pi-calculus, een recent procesalgebra-systeem dat ook mobiliteit van processen als 'feature' kan beschrijven.

Werkvormen

Voor elk van bovenstaande onderdelen zullen we twee weken uittrekken. Het hele college duurt 13 weken. Aanvang 28.02.2005, laatste college 27.06.2005.

Vereiste voorkennis

Talen en berekenbaarheid.

Tentaminering

Tentamen is schriftelijk; een huiswerktentamen behoort tot de mogelijkheden.

Literatuur

Een syllabus wordt verstrekt.


Evaluatie: studentenquêtes ; geen docentevaluatie bekend Rendement: 10 begonnen, echt meegedaan, geslaagd met 1e kans, geslaagd totaal
Q: