Doktorat

Prelegent(ci)

Artur Zawłocki

Afiliacja

Uniwersytet Warszawski

Termin

7 grudnia 2009 10:15

Pokój

p. 4790

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

Opowiem o formalizmie, mojego autorstwa, do opisu systemów zbudowanych z komponentów, z których każdy porozumiewa się z otoczeniem za pośrednictwem akcji. Podobnie jak np. w CCS i CSP, komunikacja odbywa się przez synchronizację akcji: dwa komponenty można połączyć przez sparowanie 'wyjściowych' akcji jednego z nich, z 'wejściowymi' akcjami drugiego. Do specyfikacji komponentów używam logiki temporalnej (wariantu LTL, linear temporal logic) a za wszystkim stoi model formalny oparty o automaty (albo etykietowane systemy tranzycyjne) z pewnymi moimi rozszerzeniami. Postaram się skupić głównie na przykładzie specyfikacji, pomijając w miarę możliwości technikalia.

---