ABSTRACT. TBA

ABSTRACT. Why3 is a platform for deductive program verification. It features a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a dedicated IDE where users edit source files and build proofs interactively using a blend of logical transformations and calls to external theorem provers. In this talk, I will illustrate the typical workflow of program verification using Why3's IDE, focusing on the key features of WhyML, auto-active verification, and proof maintenance.

ABSTRACT. Introduction to the 16th Overture workshop

ABSTRACT. Testing of VDM-SL models is currently a tedious and error-prone task due to lack of support for defining tests, executing tests automatically, and validating test results. In VDM++, test-driven development is supported by the VDMUnit framework, which offers many of the features one would expect from a modern testing framework. However, since VDMUnit relies on object-orientation and exception handling, this framework does not work for testing VDM-SL models. In this paper, we discuss the challenges of testing VDM-SL models, and propose a library extension of Overture/VDMUnit that improves this situation. We demonstrate usage of this library extension, and show how it also enables one to reuse tests to validate code-generated VDM-SL models.

ABSTRACT. The Functional Mock-up Interface is a standard for co-simulation, which both defines and describes a set of C interfaces that a simulation unit, a Functional Mock-up Unit (FMU), must adhere to in order to participate in such a co-simulation. To avoid the effort of implementing the low level details of the C interface when developing an FMU, one can use the Overture tool and the language VDM-RT. VDM-RT is a VDM dialect used for modelling real-time and potentially distributed systems. By using the Overture extension, called Overture FMU, the VDM-RT dialect can be used to develop FMUs. This raises the abstraction level of the implementation language and avoids implementation details of the FMIinterface thereby supporting rapid prototyping of FMUs. Furthermore, it enables precise time detection of changes in outputs, as every expression and statement in VDM-RT is associated with a “timing cost”. The Overture FMU has been used in several industrial case studies, and this paper describes how the Overture toolwrapper FMU engages in a co-simulation in terms of architecture, synchronisation and execution. Furthermore, a small example is presented.

ABSTRACT. The executable subset of VDM allows code generators to automatically produce program code. A lot of research have been conducted on automated code generators. Virtual machines are common platforms of executing program code. Those virtual machines demand rigorous implementation and in return give portability among different operating systems and CPUs. This paper introduces a virtual machine called ViennaVM which is formally defined in VDM-SL and still under development. The objective of ViennaVM is to serve as a target platform of code generators from VDM specifications.

ABSTRACT. A major challenge in multi-modelling and co-simulation of cyber-physical systems (CPSs) using distributed control, such as swarms of autonomous UAVs, is the need to model distributed controller-hardware pairs where communication between controllers using complex types is required. Co-simulation standards such as the Functional Mock-up Interface (FMI) primarily support simple scalar types. This makes the protocol easy to adopt for new tools, but is limiting where a richer form of data exchange is required, such as distributed controllers. This paper applies previous work on adding an explicit network VDM model, called an ether, to a multi-model by deploying it to a more complex multi-model, specifically swarm of UAVs.

ABSTRACT. By automation of their critical systems, modern buildings are becoming increasingly intelligent, but also increasingly vulnerable to both cyber and physical attacks. We propose that multi-models can be used not only to assess the security weaknesses of smart buildings, but also to optimise their control to be resilient to malicious use. The proposed approach makes use of the INTO-CPS toolchain to model both building systems and the behaviour of adversaries, and utilises design space exploration to analyse the impact of security on usability. By separation of standard control and security monitoring, the approach is suitable for both the design of new controllers and the improvement of legacy systems. A case study of a fan coil unit demonstrates how a controller can be augmented to be more secure, and how the trade-off between security and usability can be explored to find an optimal design. We propose that the suggested use of multi-models can aid building managers and security engineers to build systems which are both secure and user friendly.

ABSTRACT. In this short talk we present our experience in using VDMSL as tool for understanding a complex requirements specification of our model of the upcoming EMVCo Next Generation Kernel specifications. EMVCo is the consortium including MasterCard, Visa, Amex, etc for worldwide payment systems. It includes the familiar Chip&Pin and contactless protocols, as well as a number of new operational modes, security verification types (including biometric). EMVCo's objective is to ensure the requirements are are safe/correct as possible.

In order to engage them with any findings, a conversation between ourselves and stakeholders within EMVCo sub-groups has been established through formal simulation of specific protocol runs using VDMSL. The results have been productive and substantial: a number of corrections were suggested, and most importantly a large number of hidden assumptions about types, APIs, and other system parts have been carefully documented.

An issue of attempting to apply formal methods to industrial problems is that elegance often needs to be compromised in order to ensure stakeholders notice/accept the formal results: they ought to see what was built as their artefact, rather than a nicer abstraction.

Our aim, which we have achieved, is to influence the specification process prior to public release later in 2018. To date, we have modelled about 75% of the whole EMV kernel, and hope to complete it by the middle of 2018. It comprises 135 modules and 40KLOC in VDMSL, some of which is automatically generated from an XSD/XML data dictionary.

The work unravelled many technical issues in terms of design decisions, identified tool bugs, as well as the limits of Overture as a tool for industrial use at this scale. We hope to discuss these issues and make some useful suggestions.

ABSTRACT. Normally transitions between different VDM dialects go from VDM- SL towards VDM++ or VDM-RT. In this paper we would like to demonstrate that it actually can make sense to move in the opposite direction. We present a case study where a requirement change late in the project deemed the need for distribution and concurrency aspects unnecessary. Consequently, the developed VDM-RT model was transformed to VDM++ and later to VDM-SL. The advan- tage of this transformation is to reduce complexity and prepare the model for a combined commercial and research setting.

ABSTRACT. The cloud is quickly becoming the principle means by which software is delivered into the hands of users. This has not only changed the shipping mechanism, but the whole process by which software is de- veloped. The application of lean manufacturing principles to software engineering, and the growth of continuous integration and delivery, have contributed to the end-to-end automation of the development lifecycle. Gone are the days of quarterly releases of monolithic systems; the cloud- based, software as a service is formed of hundred or even thousands of microservices with new versions available to the end user on a daily basis. If formal methods are to be relevant in the world of cloud computing, we must be able to apply the same principles; enabling easy componentiza- tion of specifications and the integration of the processes around those specifications into the fully mechanized process. In this paper we present tools that enable VDM-SL specifications to be constructed, tested and documented in the same way as their implementation through the use of a VDM Gradle plugin. By taking advantage of existing binary repository systems we will show that known dependency resolution instruments can be used to facilitate the breakdown of specifications and enable the easy re-use of foundational components. We also suggest that the deployment of those components to central repositories could reduce the learning curve of formal methods and concentrate efforts on the innovative. Fur- thermore, we propose a number of additional tools and integrations that we believe could increase the use of VDM-SL in the development of cloud software.

ABSTRACT. The closing session of the Overture workshop will be dedicated to discuss the future of the Overture tool set. It is a follow-up to similar sessions held at the Cyprus and Newcastle Overture workshops. The format of the workshop is a structured brainstorm, inspired by the presentations held earlier in the day.