To: undisclosed recipients
Subject: Formaalmeetodite seminar
Date: Tue, 09 Nov 1999 14:03:59 +0200
From: Tarmo Uustalu

Lp kolleegid.

Seltskond noori Küberneetika Instituudis (Marko K, Juhan E,
allakirjutanu) on leidnud, et peavad end mõnedes formaalmeetodite
teemades harima ning sellepärast otsustanud käivitada

FORMAALMEETODITE MITTEFORMAALSEMINARI,

mille on mõelnud (nüüd sügisel) toimuma neljapäeviti kl 16
Küberneetika Instituudi ruumis B221, kestusega umbes 1.5 tundi. Iga
huviline on käesolevaga teretulnud kaasa lööma.

Eesmärgiks oleks sundimatus õhkkonnas mõõdukas tempos tutvuda
mitmesuguste kontseptsioonide, tehnikate ja töövahenditega
formaalmeetodite alalt, hakatuseks konkreetselt suurte konkurentsete
süsteemide automaatsest verifitseerimisest mudelikontrolli
teel. Võtmesõnadeks peaksid kujunema mh disainide ja omaduste
modelleerimine, olekumasinate klassid, lineaarne ja hargnev ajamudel,
temporaalloogikad ja müü-arvutus, BDDd, automaaditeoreetiline
lähenemine mudelikontrolli ülesandele, globaalne ja lokaalne (lennul)
mudelikontroll, sümboltehnikad ja osalisel järjestusel põhinevad
tehnikad, kompositsioonilisus, algoritmid ja keerukus,
reaalaja-laiendused, olemasolevad tegelikud
mudelikontrollivahendid. Jätkuteemadeks võiksid olla nt automaatse
teoreemitõestamise kasutamine verifitseerimises, tõestajad. Mingeid
erilisi eelteadmisi ei tohiks vaja minna, vähemasti mõte on asjal
selline, aga loomulikult oleks tõhus abi igast initsiatiivist mõni
alateema just ise ette valmistada.

Esimesel kokkusaamisel neljapäeval, 11. novembril räägib allakirjutanu
mõnedest põhimõistetest kõnealuses valdkonnas - realisatsioonid vs
spetsifikatsioonid, olekumasinad vs loogikavalemid, mudelikontroll,
teoreemitõestamine - ühe lihtsa näite toel.

Jooksev info hakkab paiknema webilehel //www.cs.ioc.ee/~tarmo/fmmf/.

Tarmo Uustalu