Tallinna Tehnikaülikoolis on erialane kompetents ja professionaalsed õppejõud – tagamaks koolituse kõrget taset, viivad kursuseid läbi oma ala spetsialistid nii TTÜst kui ka mujalt
18.dets, 15:00 ICT-411 "Verifying Hybrid Systems with Modal Kleene Algebra/ Making Linearizability Compositional for Weak Memory"
Tarkvarateaduse instituudi seminaril teisipäeval, 18.12.2018 kell 15:00 esinevad Georg Struth ja Simon Doherty (Sheffieldi Ülikool, Ühendkuningriik) teemadel "Verifying Hybrid Systems with Modal Kleene Algebra/ Making Linearizability Compositional for Weak Memory".
Seminar toimub ruumis ICT-411.
Prof. Georg Struth
Verifying Hybrid Systems with Modal Kleene Algebra
Lühikokkuvõte
Hybrid Systems integrate continuous dynamics and discrete control. Their verification, in domains like the control of chemical plants, finance and traffic systems, the coordination of autonomous vehicles or robots, and the optimisation of mechanical systems or bio systems engineering, is increasingly important. A prominent approach is differential dynamic logic (dL), a modal logic for reasoning about ordinary differential equations and their solutions within hybrid programs. Over the last decade, a domain-specific sequent calculus for dL has been developed together with an intricate explicit substitution calculus. It has been integrated into the KeYmaera X tool, which has proved its worth in numerous case studies.
This talk presents an algebraic reconstruction of dL and the first verification components in an interactive proof assistant inspired by it. It is based on modal Kleene algebra, an extension of Kleene algebra by modal operators in the style of dynamic logic, and integrations of a hybrid store into either the relational or a state transformer semantics of this algebra. This yields a simple semantic variant in which substitutions are replaced by store updates and domains specific inference rules become derivable. At the moment, two approaches to hybrid systems verification are supported: Firstly, solutions to ordinary differential equations can be supplied to the component, and certified along the lines of Picard-Lindelöf's theorem. Verification conditions for the orbits obtained from these solutions, in fact, weakest liberal preconditions, can then be computed and used with the more standard conditions generated by the algebra. Secondly, differential invariants in the style of dL can be supplied and refined within the algebra. Intuitively, these invariants encode the orbit structure of a dynamic system directly as assertions.
Apart from presenting modal Kleene algebra and its extension to hybrid systems, I will comment on the intricacies of formalising the approach within the Isabelle/HOL proof assistant, and outline some future directions for this line of work, time permitting.
This work is joint with Jonathan Julián Huerta y Munive, and partially funded by CONACYT.
Simon Doherty
Making Linearizability Compositional for Weak Memory
Lühikokkuvõte
In the interleaving model of concurrency, where events are totally ordered, linearizability is compositional: the composition of two linearizable objects is guaranteed to be linearizable. However, linearizability is not compositional when events are only partially ordered, as in the weak memory models that describe multicore memory systems. In this talk, we present a generalisation of linearizability for concurrent objects implemented in weak memory models. We abstract from the details of specific memory models by defining our condition using Lamport's execution structures. We apply our condition to the C11 memory model, providing a correctness condition for C11 objects. We describe a proof method for verifying objects implemented in C11 and related models. Our method is an adaptation of simulation-based methods, but in contrast to other such methods, it does not require that the implementation totally orders its events.
