Title: Building correct Cyber‐Physical Systems --- can we improve current practice?
Speaker: Susanne Graf, VERIMAG, France
Abstract: Modern cyberphysical systems are of increasing complexity, composed of an increasing number of components and subsystems of heterogenous nature, of different criticity levels and where different non-functional aspects -- such as timing, energy, dependability and more and more also security -- are as important as functionality. Current approaches use different models and corresponding tools for different viewpoints and guarantee overall correctness by means of strong assumptions. A more flexible contract-based approach would allow to relax some of these strong assumptions without abandoning the current modelling approach and the current tools.
About Susanne: Susanne Graf received her PhD in Computer Science in 1984 from Grenoble Polytechnical Institute (INPG). Currently she is a "Directeur de Research" at CNRS in the Verimag laboratory of Univ. Grenoble Alpes. Her research interests include theories, algorithms and tools for modeling and verification and their application to the design and certification of embedded and real-time as well as mixed-criticality systems. Presently she is focussing on knowledge and contract-based methods to achieve scalability. One of her main contributions is in the domain of abstraction where together with Hassen Saidi she has proposed a method called predicate abstraction. She has been the Chair of ETAPS 2002 in Grenoble, she has been the PC chair of TACAS 2000, SPIN 2004, ATVA 2006 and FORTE 2015. She is on the editorial board of Springer's STTT journal and has been in a large number of Program Committees.
Title: Generative model driven design for agile system design and evolution - a tale of two worlds.
Speaker: Tiziana Margaria, LERO, Ireland
Abstract: To be added.
About Tiziana: Tiziana Margaria is Chair of Software Systems and Head of Department at the Dept. of Computer Science and Information Systems at the University of Limerick (Ireland). She is also a Principal Investigator of Lero, The Irish Software Research Center, where she is heads the Committee on International Relations Development, and Principal Investigator of Confirm, the new SFI Research Centre on Smart Manufacturing. In Lero, she heads research projects on Scientific Workflow and model-driven HW/SW Cybersecurity. In Confirm, she will co-lead the Hub on Cyberphysical Systems, and use her expertise in advanced model driven, generative, and service-oriented design in the industrial automation context.
She has broad experience in the use of formal methods for high assurance systems, in particular concerning functional verification, reliability, and compliance of complex heterogeneous systems. She is (co-) author of over 200 refereed papers in international journals and conferences, and she served on more than 100 Program Committees, over 20 times as chair.
She is the ideator and General Chair of ISoLA, the series of biannual International Symposia on Leveraging Applications of Formal Methods, Verification and Validation (since 2004), co-founder of STTT, the International Journal on Software Tools for Technology Transfer (Springer, 1997), and most recently Founding editor of the Transactions on Foundations for Mastering Change (Springer, 2016).
She is Fellow of the Irish Computer Society and Fellow of SDPS, the Society for the Design and Process Science. She is currently Vicepresident of the European Association of Software Science and Technology (EASST), and current Chair of FMICS (the ERCIM Working Group on Formal Methods for Industrial Critical Systems). In EuSEM (European Society for Emergency Medicine) she is Member of the Research Committee Special Interest Group on Technology and Processes of Care in the Emergency Care (SIG-TPCEC). She holds 2 USPTO patents, one of which with NASA.
Dr. Grant Olney Passmore.
- Co-Founder and Co-CEO, Aesthetic Integration, London
- Life Member, Clare Hall, University of Cambridge
- Honorary Associate, LABORES - Laboratoire de Recherche Scientifique, Paris
Title: Formal Verification of Financial Algorithms with Imandra
Abstract: Many deep issues plaguing today's financial markets are symptoms of a fundamental problem: The complexity of algorithms underlying modern finance has significantly outpaced the power of traditional tools used to design and regulate them. At Aesthetic Integration, we've pioneered the use of formal verification for analysing the safety and fairness of financial algorithms. With a focus on financial infrastructure (e.g., the matching logics of exchanges and dark pools), we'll describe the landscape, and illustrate our Imandra formal verification system on a number of real-world examples. We'll sketch many open problems and future directions along the way.
P.S. Imandra is available for use in the cloud and is by no means limited to financial algorithms (for example, Imandra is now being used for the design and regulation of autonomous vehicle controllers and RobotOS nodes!). Bring your laptop if you want to experiment with Imandra and the systems we'll discuss during the talk.
Title: Dynamic Symbolic Execution for Software Analysis
Abstract: Symbolic execution is a program analysis technique that can automatically explore and analyse paths through a program. While symbolic execution was initially introduced in the seventies, it has only received significant attention during the last decade, due to tremendous advances in constraint solving technology and effective blending of symbolic and concrete execution into what is often called dynamic symbolic execution. Dynamic symbolic execution is now a key ingredient in many computer science areas, such as software engineering, computer security, and software systems, to name just a few.
In this talk, I will discuss recent advances and ongoing challenges in the area of dynamic symbolic execution, drawing upon our experience developing several symbolic execution tools for many different problems, such as high-coverage test input generation, bug and security vulnerability detection, patch testing and bounded verification, among many others.
Title: Integrating formal methods for modelling and simulation of swarm robotics
Speaker: Ana Cavalcanti, University of York
Abstract: There are many challenging aspects involved in ensuring safety of mobile and autonomous robots. One aspect that has been neglected is software engineering. The state-of-practice uses costly iterations of trial and error, often with hardware and environment in the loop, after an ad hoc use of simulations. It is clear that the modern outlook of the robotic applications is not matched by the outdated practices of design and verification when it comes to controller software.
We present two new domain-specific languages for robotics: RoboChart and RoboSim. They support a model-based approach for early formal validation and sound generation of simulations. In robotics, simulation is the favoured technique for analysis. In our work, simulation is complemented by analysis based on model checking, using CSP, tock-CSP, and the refinement model checker FDR, and theorem proving, using Isabelle/UTP. Our ultimate goal is to support reasoning and code generation using a variety of techniques, but relying on theorem proving to deal with data-rich and large systems, especially with models for swarm applications.
RoboChart is a UML-like notation that includes timed and probabilistic primitives for modelling of controllers. We link it to RoboSim, another graphical notation defined as a gateway between RoboChart models and customised simulations developed for traditional robotics simulators. RoboChart enforces design patterns appropriate to deal with robotic applications and now includes also notation to model collections of robots as present in swarms.
Our approach is predicated on a few principles. First, we adopt notations akin to those in current use by practitioners, namely, notations based on state machines, to ensure usability. Second, we enforce specific architectural patterns relevant for the area, and define precise languages that can be used for automatic generation of mathematical models. Third, our goal is to hide the formalisms from practitioners entirely. Via specialisation and automation, we seek both scalability and usability. Finally, we investigate the integrated use of a variety of techniques together to tackle the different needs of verification and development.
Title: Program Correctness under Weak Memory Consistency
Speaker: Viktor Vafeiadis, MPI-SWS
Abstract: It is fairly common knowledge that shared-memory concurrent programs running on modern multicore processors do not adhere to the interleaving concurrency model, but rather exhibit weakly consistent behaviours, such as store and load buffering. Formally, the semantics of shared-memory concurrent programs is determined by a weak memory model, defined either by the programming language (e.g., in the case of C/C++11 or Java) or by the hardware architecture (e.g., for assembly and legacy C code).
These weak memory models pose two major challenges for software verification. First, many standard proof techniques that were developed for interleaving concurrency, such as the Owicki-Gries method, are unsound in the context of weak memory consistency. Second, it is not even clear how to specify the correctness of concurrent libraries when there is no globally agreed notion of time and state. To overcome these challenges, we therefore have to develop new techniques for specifying and verifying weakly consistent concurrent programs. The invited talk will present some first steps in this direction.