Doktorat

Speaker(s)

Artur Zawłocki

Affiliation

Uniwersytet Warszawski

Date

Dec. 7, 2009, 10:15 a.m.

Room

room 4790

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

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.

---