Detaljerad information för diarienr 2003-2983
		Besl. instans: NT Ämnesområde: Datavetenskap Beslutsdat: 2003-11-10 Namn: Claessen, Koen Titel: Fil doktor Kön: Man Univ./Institution: Chalmers tekniska högskola - Institutionen för data-och informationsteknik Projekttitel: Abstraktionssökning med hjälp av ändlig-modellgenerering Project title: Building abstractions using finite model generation Värdhögskola: Chalmers tekniska högskola SCB-klassificering: Datavetenskap Beviljat(SEK): Bidragsform/Finansieringskälla   2004 2005 2006   Projektbidrag/ Vetenskapsrådet, naturvetenskaplig-teknikvetenskaplig forskning   607500 607500 607500 Beskrivning: I dagens datorsystem, spelar kommunikation mellan datorer en allt större roll. Datorer pratar med varandra genom att skicka meddelanden till varandra. De programmen som bestämmer vilka meddelanden som ska skickas till vilken dator på vilken tidpunkt kallas för protokoller. I komplexa nätverk är protokollerna oftast också väldigt komplexa. Det är svårt för människan som designar protokollerna att förstå vad exakt som pågår hela tiden i nätverket, och det är lätt att någonting går fel: ett felaktigt meddelande skickas till fel dator vid fel tillfälle, och helt plötsligt blir alla datorerna förvirrade. För att undvika detta, behövs det metoder som kan visa komplexa protokoller som ovan, där många saker händer samtidigt, på ett mera abstrakt sätt, så att en människa kan förstå systemet, och fokusera på en sak i taget. I forskningsprojektet försöker vi använda ett koncept från matematisk logik, som kallas för logiska ändliga modeller, för att hitta sådana abstrakta sätt att titta på system automatiskt.