Lekciju kurss LU datorzinātņu maģistratūras studentiem
2004.gada rudens semestris

Kārlis Čerāns, Dr.dat., asoc.prof.
E-mail: Karlis.Cerans@mii.lu.lv
Internet: http://www.ltn.lv/~karlisc/stud.htm

Kursā tiek aplūkots formālas specifikācijas jēdziens, kā arī virkne klasisku modeļu jeb sistēmu formālu specifikāciju uzdošanai. Tiek aplūkoti pamati programmu moduļu ieejas-izejas darbības specifikācijai, ekvacionālās un modeļbāzētās valodas sistēmu formālai specifikācijai, kā arī valodas paralēlu un reaktīvu sistēmu darbības aprakstam.
    Kurss būs noderīgs studentam, kas interesējas par formālām specifikāciju valodām, kas izmantojamas programmatūras un aparatūras darbības specifikācijā, kā arī studentam,  kas vēlas pilnīgāk apzināties pastāvošo saikni starp matemātiskām teorijām un programmēšanas praksi, vai arī vēlas bagātināt savu programmēšanas un sistēmu izstrādes praksi ar atziņām, kas var tikt smeltas no teorijas.

Plānotais kursa saturs

A. Ievads. Specifikācijas jēdziens, piemēri. Hoara loģika.

A1. Specifikācijas jēdziens. Formālas specifikācijas, to raksturojumi un izmantošana programmatūras dzīves ciklā.
A2. Procedūru interfeisa (ieejas - izejas) specifikācijas loģiskā formā. Daļējā un pilnā korektība.
A3. Atbilstības specifikācijai konstatēšana: Hoara loģika, cikla invarianti, cikla varianti.

B. Ekvacionālās un modeļbāzētās sistēmu specifikāciju valodas

B1. Konstruktīvie datu tipi.
B2. Algebriskās specifikācijas. Valoda ACT ONE. OBJ saimes valodas.
B3. Valoda Larch: ekvacionāli loģiskās specifikācijas.
B4. Modeļbāzētās specifikāciju valodas: B, Z. Ieskats valodu Object Z, VDM-SL konstrukcijās.

C. Paralēlu un reaktīvu sistēmu specifikācija

C1. Paralēlo procesu teorijas pamati. Procesu algebras, valoda CCS.
C2. Valoda LOTOS notikumu temporālā sakārtojuma specifikācijai.
C3. Temporālās loģikas, to varianti. Temporālā loģika TLA. Automāti uz bezgalīgiem vārdiem.

Papildus materiāls:
C4. Petri tīkli sistēmu modelēšanā. Krāsainie Petri tīkli.
C5. Reālā laika automāti. Audio kontroles protokola piemērs.
 

Mājas darbi

Resursi tīmeklī

Literatūra

Vērtēšana:
1) aptuveni 10 mājas darbi (vienkārši uzdevumi, lai nostiprinātu izpratni par aplūkoto formālismu pamata idejām);  (Sk. iepriekšējā gada mājas darbus).
2) uzrakstīts referāts 8-12 lapas, tēma saskaņojama ar pasniedzēju (referāta nolasīšana nav obligāta, bet būs iespējama tiem, kas to vēlēsies);
3) eksāmens (vienkārši teorijas jautājumi un lekcijās un mājas darbos ietvertiem uzdevumiem analoģiski uzdevumi).

Ja noteiktajos termiņos iesniegti izpildīti mājas darbi, kā arī iesniegts maģistratūras līmenim atbilstošs referāts, eksāmenā var saņemt atzīmi vismaz "8" bez teorijas jautājumu atbildēšanas un bez citu uzdevumu risināšanas (mājas darbu uzdevumu risinājumiem šajā brīdī jābūt pareiziem un tos jāspēj paskaidrot / aizstāvēt).