Title: Generative model driven design for agile system design and evolution - a tale of two worlds.

Speaker: Tiziana Margaria, LERO, Ireland

Location: 9:00 - 10:00 on Monday, 3rd September, Iontas Lecture Theatre

Abstract: In order to mainstream the production and evolution of IT at the levels of speed, scale, affordability and collaborative effort needed to truly make IT enter the fabric of every economical and societal endeavour, as is the projected future of our society in the next decade, the ease of learning, understanding, and applying new disruptive technologies must drastically improve. We argue that the needs of the people, the economical sectors, and the large-scale trends can only be met if the IT professions embrace and adopt a new way of producing and consuming IT, based on more formal descriptions, more models, more reasoning and analysis before expensive implementations are incurred, coupled with automatic transformations, generations, and analyses that take advantage of the models and formalized knowledge. We analyse briefly the various dimensions, derive a specification for the new IT and IT platforms, and provide a few examples of how the new thinking can disrupt the status quo but empower a better understanding, a more efficient organization, and a more automatic management of the many cross-dimensional issues that future connected software and systems will depend upon.

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.

Title: Building correct Cyber‐Physical Systems --- can we improve current practice?

Speaker: Susanne Graf, VERIMAG, France

Location: 9:10 - 10:10 on Tuesday, 4th September, Iontas Lecture Theatre

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: Program Correctness under Weak Memory Consistency

Speaker: Viktor Vafeiadis, MPI-SWS

Location: 9:00 - 10:00 on Wednesday, 5th September, Iontas Lecture Theatre

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.

Title: Dynamic Symbolic Execution for Software Analysis

Speaker: Cristian Cadar, Imperial College London

Location: 9:00 - 10:00 on Thursday, 6th September, Iontas Lecture Theatre

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

Location: 9:00 - 10:00 on Friday, 7th September, Iontas Lecture Theatre

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.