View: session overviewtalk overview
Verification
09:00 | A Software Exoskeleton to Protect Ethics and Privacy of Users in the Digital World |
15:00 | A Formal Modeling Approach for Portable Low-Level OS Functionality ABSTRACT. The increasing dependability requirements and hardware diversity of the IoT pose a challenge to developers. New approaches for software development that guarantee correct implementations will become indispensable. Specially for RTOSs, automatic porting for all current and future devices will also be required. As part of our framework for embedded RTOS portability, based on formal methods and code generation, we present our approach to formally model low-level operating-system functionality using Event-B. We show the part of our RTOS model where the switch into the kernel and back to a task happens, and prove that the model is correct according to the specification. Hardware details are only introduced in late refinements, which allows us to reuse most of the RTOS model and proofs for several target platforms. As a proof of concept, we refine the generic model to two different architectures and prove safety and liveness properties of the models. |
15:30 | Synthesis of P-stable abstraction PRESENTER: Anna Becchi ABSTRACT. Stability is a fundamental requirement of dynamical systems. Most of the works concentrate on verifying stability for a given stability region. In this paper we tackle the problem of synthesizing P-stable abstractions. Intuitively, the P-stable abstraction of an open dynamical system characterizes the transitions between stability regions in response to external inputs. The stability regions are not given - rather, they are synthesized as the tightest representation with respect to a given set of relevant predicates P. A P-stable abstraction is enriched by timing information derived from the duration of stabilization. We implement a synthesis algorithm in the framework of abstract interpretation, that allows different degrees of approximation. We show the representational power of P-stable abstractions, that provide a high-level account of the behavior of the system with respect to stability, and we experimentally evaluate the effectiveness of a compositional approach, that allows synthesizing P-stable abstractions for significant systems. |
16:00 | Formal Verification of Human-Robot Interaction in Healthcare Scenarios PRESENTER: Livia Lestingi ABSTRACT. We present a model-driven approach for the creation of formally verified scenarios involving human-robot interaction in healthcare settings. The work offers an innovative take on the application of formal methods to human modeling, as it incorporates physiology-related aspects. The model, based on the formalism of Hybrid Automata, includes a stochastic component to capture the variability of human behavior, which makes it suitable for Statistical Model Checking. The toolchain is meant to be accessible to a wide range of professional figures. Therefore, we have laid out a user-friendly representation format for the scenario, from which the full formal model is automatically generated and verified through the Uppaal tool. The outcome is an estimation of the probability of success of the mission, based on which the user can refine the model if the result is not satisfactory. |
16:30 | Formal Verification of COLREG-Based Navigation of Maritime Autonomous Systems ABSTRACT. Along with the actively progressing field of autonomous ground and aerial vehicles, the advent of autonomous vessels has brought up new research and technological problems originating from the specifics of marine navigation. Autonomous ships are expected to navigate safely and avoid collisions following accepted navigation rules. Trustworthy navigation of autonomous ships presumes to apply provably correct navigation algorithms and control strategies. We introduce the notion of maritime game as a special case of Stochastic Priced Timed Game and model the autonomous navigation using UPPAAL STRATEGO. The navigation control strategy is optimised and verified to achieve the goal to safely reach the manoeuvre target points at a minimum cost. The approach is illustrated with the case study inspired by COLREG Rule 15. |