Visioconference
26 February 2021 - 10h00
Local Reasoning for Reconfigurable Distributed Systems
by Emma AHRENS from Verimag, Mohytos
Abstract: This work investigates the use of separation logic for reasoning about dynamically reconfigurable behavior, interaction, priority (DR-BIP) systems and allows the verification of reconfiguration programs on certain distributed systems. Separation logic extends Hoare logic to enable the verification of programs on resources. It makes use of local reasoning and provides a frame rule. Static BIP systems represent component-based systems, where a fixed number of components encapsulate behavior specified as transition systems and interact via a fixed set of multiparty interactions (synchronizations) that are executed atomically and non-deterministically. The extension to DR-BIP systems additionally allows dynamic reconfiguration, through addition and/or removal of interactions and components during runtime.
lien visio :
https://veri-bbb.imag.fr/b/rad-ofn-9t8-rqc (password: 031456)
