CITI has stopped operations in 2014, to co-launch NOVA LINCS THIS SITE IS NOT BEING UPDATED SINCE 2013
citi banner
Home Page FCT/UNL UNL
  Home  \  Seminars @ CITI  \  Seminar Page Login  
   
banner bottom
File Top
Synthesising Correct Concurrent Runtime Monitors
{ Wed, 5 Feb 2014, 14h00 }

By: Adrian Francalanza  [ show info ]

(This is a joint CITI/CENTRIA seminar) Runtime verification of programs is often carried out by monitors, software entities running along side the program being verified, observing its behaviour and flagging whenever a satisfaction or violation is detected. A fundamental tenet underlying such a setup is the correctness of the monitor itself. In this talk I shall discuss recent work on synthesising correct concurrent monitors for runtime verification. In particular I shall focus on an adaptation of the mu-calculus that allows one to specify safety properties for Erlang programs. I outline issues relating to automated synthesis from formulas in this logic to Erlang monitors that detect formula violations at runtime. I present a formalisation of monitor correctness for this concurrent setting and describe a technique that can be used to prove monitor correctness in stages; this technique is used to prove the correctness of the monitor synthesis presented.


Hosted by: Software Systems

Location: DI seminars room

File Bottom