We see the future of medicine as highly automated. Improvement in care-provision will be achieved by both increased clinician efficiency, as well as new computing assisted treatments and diagnoses. In other safety-critical industries, such as avionics and automotive, certification is dependability-driven. In contrast, medical certification is clinical-trial driven, which we argue will become increasingly problematic with increasing medical device and software complexity. By dependability, we mean the dictionary notion: reliable and trustworthy. Thus, failures are either avoided by design, or are accountable to a measured extent. This touches upon the verification (intent) versus validation (outcome) problem. Even though correctness does not imply safety, we do believe from our experiences that, the process of striving for correctness (verification) done right does shed light on safety; on whether the requirements/assumptions were addressed as intended (validation). Medical device trials can lead to adequate assurances of safety, as defined by the local regulatory burden. Nevertheless, the nature of such complex systems means that certain errors may not be detected by trials and so additional efforts to reduce errors is needed. Our intent is, at least for software, to explore the contrast between approaches: correctness-by-construction versus correct-by-trial. Additionally, these levels of safety and effectiveness of systems vary across regulatory domains in different countries. A key challenge is how to achieve a successful interaction between verification tasks using formal methods and system development tasks within engineering teams without prior knowledge of formal techniques. This paper describes a pragmatic process for the application of formal techniques, which is illustrated for three medical devices during pre-clinical development prior to certification. That means, the techniques are not only applied to realistic systems, but are also taken up by development teams themselves (i.e. cannot be entirely formal expert driven). We demonstrate differences in applying formalisms at the start, midpoint and final development stages. In particular, we describe the underlying socio-technical challenges and how we developed mitigation methods for each exemplar case. This paper is not about a general technique for medical automation, as we do not believe this is practical/possible given the varied/dynamic nature of medical problems.

Safety-Critical Java (SCJ) is a version of Java suitable for programming real-time safety-critical systems; it is the result of an international standardisation effort to define a subset of the Real-Time Specification for Java (RTSJ). SCJ programs require the use of specialised virtual machines. We present here the result of our verification of the scheduler of the only SCJ virtual machine up to date with the standard and publicly available, the icecap HVM. We describe our approach for analysis of (SCJ) virtual machines, and illustrate it using the icecap HVM scheduler. Our work is based on a state-rich process algebra that combines Z and CSP, and we take advantage of well established tools.

In this paper we present an attack, which allows fraudulent transactions to be collected from EMV contactless credit and debit cards without the knowledge of the cardholder. The attack exploits a previously unreported vulnerability in EMV protocol, which allows EMV contactless cards to approve unlimited value transactions without the cardholder's PIN when the transaction is carried out in a foreign currency. For example, we have found that Visa credit cards will approve foreign currency transactions for any amount up to ∈999,999.99 without the cardholder's PIN, this side-steps the £20 contactless transaction limit in the UK. This paper outlines our analysis methodology that identified the flaw in the EMV protocol, and presents a scenario in which fraudulent transaction details are transmitted over the Internet to a "rogue merchant" who then uses the transaction data to take money from the victim's account. In reality, the criminals would choose a value between ∈100 and ∈200, which is low enough to be within the victim's balance and not to raise suspicion, but high enough to make each attack worthwhile. The attack is novel in that it could be operated on a large scale with multiple attackers collecting fraudulent transactions for a central rogue merchant which can be located anywhere in the world where EMV payments are accepted.

We present an abstract formalisation of federated cloud workflows using the Z notation. Various properties of interest are observed in the possible deployments symbolically calculated by the Z/EVES theorem prover. These properties are defined using rules restricting valid options in various categories like security, cost, dependability, etc.

Abstract We describe: (1) the internal structures of FDR, the refinement model checker for Hoare’s Communicating Sequential Processes (CSP); and (2) an application-programming interface (API) that allows users to interact more closely with FDR and to have finer-grain control over its behaviour and data structures. This API makes it possible to create optimised CSP code to perform refinement checks that are more space or time efficient, enabling the analysis of more complex and data-intensive specifications. The API can be used either by those constructing CSP models or by tools that automatically generate CSP code. We present examples of using our tool, including handling advanced FDR features such as transparent functions, which compress state spaces before checking. We also show how to transform FDR’s graph format into a graph notation such as JGraph, enabling visualisation of labelled transition systems of CSP specifications.

We present a research roadmap for the second pilot project in the Verified Software Grand Challenge on formally verified POSIX file stores. The work is inspired by the requirements for NASA's forthcoming Mars Rover missions. The roadmap describes an integrated and comprehensive body of work, including current work, as well as further opportunities for collaboration.

The International Grand Challenge in Verified Software is benchmarking current verification technology by conducting a series of experiments, and one such experiment is to build a verified POSIX-compliant flash filestore. An objective of this experiment is to combine different formal methods, and this raises issues about the different logics used. One significant area of difference is in the treatment of undefined expressions, and we show how this difference can be overcome using a unifying theory. This then allows us to use a theorem proverfor Z to verify theorems about a data type specified and refined in VDM.

Abstract We describe our experiences in mechanising the specification, refinement, and proof of the Mondex Electronic Purse using the Z/Eves theorem prover. We took a conservative approach and mechanised the original L a T E X sources without changing their technical content, except to correct errors. We found problems in the original specification and some missing invariants in the refinements. Based on these experiences, we present novel and detailed guidance on how to drive Z/Eves successfully. The work contributes to the Repository for the Verified Software Grand Challenge.

We present results from the second pilot project in the international Verification Grand Challenge: a formally verified specification of a POSIX-compliant file store using the Z/Eves theorem prover. The project's overall objective is to build a verified file store for space-flight missions. Our specification of the file store is based on Morgan & Sufrin's specification of the UNIX filing system; the proof and its mechanisation in Z/Eves are novel. We show how our work contributes towards building a verified software repository: a set of general theories and experiments reusable across different domains.

Parts of the CICS transaction processing system were modelled formally in the 1980s in a collaborative project between IBM Hursley Park and Oxford University Computing Laboratory. Z was used to capture a precise description of the behaviour of various modules as a means of communicating requirements and design intentions. These descriptions were not mechanically verified in any way: proof tools for Z were not considered mature, and no business case was made for effort in this area. We report a recent experiment on using the Z/Eves mechanical theorem prover to construct a machine-checked analysis of one of the CICS modules: the File Control API. This work was carried out as part of the international Grand Challenge in Verified Software, and our results are recorded in the Verified Software Repository. We give a brief description of the other modules, and propose them as challenge problems for the verification community.