SFMoVeS: Scottish Seminar on Formal Modelling, Verification, and Synthesis

About SFMoVeS

The International Conference on Quantitative Evaluation of Systems (QEST) is the leading forum on quantitative evaluation and verification of computer systems and networks, through stochastic models and measurements. In 2019 QEST takes place in Glasgow! This is a great opportunity to bring together researchers from all SICSA institutions for a one-day pre-conference workshop to address current challenges and relevant questions, to communicate and share their experiences on formal approaches to qualitative or quantitative evaluation of systems. Our aim is to foster a tighter community of researchers from SICSA institutions interested in the formal modelling, verification and synthesis applied to computer systems and networks.

Invited speakers:

• Prof Simon Dobson, School of Computer Science, University of St Andrews
• Prof Alice Miller, School of Computing Science, University of Glasgow
• Prof Guido Sanguinetti, School of Informatics & SynthSys, University of Edinburgh

Call for contributions:
We invite contributions on formal methods applied to modelling, verification and synthesis of complex software systems. Speakers are invited to present research results in any of the themes of interest for the workshop as well as application experiences, tools, and promising preliminary ideas. We are planning this event as a friendly venue for PhD students and RAs to discuss their work in progress and get feedback.
If you would like to give a talk, please send your proposed title and abstract (up to 500 words) by email to Oana Andrei via email by (UPDATED!) 1 September 2019.

Attending:
The lunch and the coffee breaks are free for registered participants. In order to help with catering arrangements, please register on Eventbrite.

Abstracts

• Alice Miller - Collaborative models for autonomous controller synthesis and deployment
  Autonomous vehicles such as unmanned aerial vehicles (UAVs), autonomous underwater vehicles and autonomous ground vehicles have widespread application in both military and commercial contexts. Understandably, there are concerns about safety and reliability of autonomous vehicles, guaranteeing their reliability using testing alone is infeasible. Formal verification offers hope in this direction having been used both for controller synthesis and for verifying the reliability and safety of autonomous controller logic. In this talk I will survey existing work on using discrete-time abstract models for generating controllers for autonomous systems. I will then summarise how we use such an approach to synthesise controllers for an unmanned aerial vehicle (UAV) using abstract models (Markov Decision Processes (MDPs)) and the PRISM model checker. In particular I will focus on the relationship between a concrete (MATLAB) simulation model and abstract MDP models, demonstrating how synthesised strategies for the UAV’s search mode can be deployed on a concrete system. I will also report on recent results implementing a symmetry-based approach to apply our strategies over a larger search area.
  This is joint work with: Douglas Fraser, Ruben Giaquinta, Ruth Hoffmann, Murray Ireland and Gethin Norman
• Prof Guido Sanguinetti - Geometric fluid approximations for general continuous time Markov chains
  Fluid approximations have seen great success in approximating the macro-scale behaviour of Markov systems with a large number of discrete states. However, these methods rely on the continuous-time Markov chain (CTMC) having a particular population structure which suggests a natural continuous state-space endowed with a dynamics for the approximating process. We construct here a general method based on spectral analysis of the transition matrix of the CTMC, without the need for a population structure. Specifically, we use the popular manifold learning method of diffusion maps to analyse the transition matrix as the operator of a hidden continuous process. An embedding of states in a continuous space is recovered, and the space is endowed with a drift vector field inferred via Gaussian process regression. In this manner, we construct an ODE whose solution approximates the evolution of the CTMC mean, mapped onto the continuous space (known as the fluid limit).
  Joint work with Michalis Michaelides and Jane Hillston
• Yasmin Rafiq - Continual Runtime Formal Verification of QoS Properties with Confidence Intervals
  In my PhD thesis I introduced new techniques for learning the parameters and structures of discrete-time Markov chains, a class of models that is widely used to establish key reliability, performance and other QoS properties of real-world systems. The new learning techniques use as input run-time observations of systems events associated with cost/rewards and transitions between the states of a model. When the model structure is known, they continually update its state transition probabilities and cost/rewards in line with the observed variations in the behaviour of the system. In scenarios when the model structure is unknown, a Markov chain is synthesised from sequences of such observations. The two categories of learning techniques underpin the operation of a new toolset for the engineering of self-adaptive service-based systems, which was developed as part of my research. My thesis introduces this software engineering toolset, and demonstrates its effectiveness in a case study that involves the development of a prototype telehealth service-based system capable of continual self-verification.
  Furthermore, we extend the applicability of quantitative verification to the common scenario when the probabilities of transition between some or all states of the Markov models analysed by the technique are unknown, but observations of these transitions are available. To this end, we introduce a theoretical framework and a toolchain that establish confidence intervals for the QoS properties of a software system modelled as a Makov Chain with uncertain transition probabilities. Our experiments show that disregarding these uncertainties may significantly affect the accuracy of the verification results, leading to wrong decisions and low-quality software systems.
• Simon Dobson - Understanding sensing from a more formal perspective
  What do sensors actually sense? This seems like a straightforward question, but it turns out to be rather more subtle than it first appears. And the answer matters, because we are increasingly making use of sensor observations for mission-critical applications and the formation of public policy. If we can't robustly determine what it is we are actually sensing -- with what confidence, and with what consequences in the case of partial system failure -- then we are clearly running severe risks in our decision-making.
  This sounds like a case for formal methods! ... but the methods we know and love aren't necessarily well-targeted at the sorts of questions that sensor systems pose. In this talk I will describe some current work to identify approaches that might (or might not) be more suitable.
• Clemens Kupke - Coalgebra Learning
  Coalgebra provides a versatile framework to represent various types of transition systems such as DFAs, labelled transition systems (LTSs) and probabilistic and weighted variants of LTSs. In the first part of my talk I will sketch key elements of this coalgebraic framework. After that I will explain how automata learning - a popular technique for inferring minimal automata through membership and equivalence queries - can be generalised to the level of coalgebras. Our approach relies on the use of logical formulas as tests and allows to learn, e.g., labelled transition systems, using Hennessy-Milner logic.
  Based on joint work with Simone Barlocco and Jurriaan Rot.
• Jan de Muijnck-Hughes - Well-Typed Models are Correct Models
  Modern Systems-on-a-Chip (SoC) are constructed by composition of IP (Intellectual Property) Cores with the communication between these IP Cores being governed by well described interaction protocols. However, there is a disconnect between the machine readable specification of these protocols and the verification of their implementation in known hardware description languages. Although tools can be written to address such separation of concerns, the tooling is often hand written and used to check hardware designs a posteriori. Further, it is important when connecting components together that only one signal can flow along a channel.
  Dependent type-systems present a rich and expressive setting that supports the precises specifi- cation of our programs properties to be stated and verified directly in the language’s type-system. Such type-systems also support reasoning about a programs substructural properties in the style of substructural typing. We can use these concepts to express model invarients directly within our model’s types and provide correctness-by-construction guarantees that our models adhere to external specifications, and are thus well-formed, at design-time using type checking.
  In this talk I will present my ongoing work as part of the Border Patrol project to construct a modelling languague for designing Systems-on-a-Chip. Our framework, Cordial, is designed to enrich existing Hardware Description Languages, and development environments, with static design-time mechanisms that reason about the (sub)structural properties of SoC Designs using Dependent, Session, and Quantitative Typing. Cordial’s type-system provides guarantees that the interfaces on an IP Core will be well-typed if they adhere to an external specification, and that we can guarantee that components are connected in a safe way by tracking the number of times a port is used within a design and comparing the interconnections ports. With Cordial mismatches between SoC specification and implementation become impossible thereby reducing errors, increasing designer productivity and enhancing safety and security of SoC designs.
  This is joint work with Wim Vanderbauwhede.