VERISURE 2014 PROCEEDINGS: PAPERS WITH ABSTRACTS

ABSTRACT. In many safety-critical industries developers and operators are required to construct and present well reasoned arguments that their systems achieve acceptable levels of safety. These arguments (together with supporting evidence) are typically referred to as a “safety case”. Safety arguments historically have been communicated through narrative text, leading often to problems of comprehension and communication. Over the last twenty years there has been increasing interest in using structured argumentation notations such as GSN (Goal Structuring Notation) or CAE (Claims-Argument-Evidence) to communicate the structure of the argument. Whilst such arguments are structured, they remain informal. There is increasing interest in exploring how these informal arguments may be modeled in formal logic, potentially opening up benefits of forms of analysis not possible with informally recorded argument. This position paper discusses a number of considerations in balancing the role of informal and formal logic in modeling assurance case arguments.

ABSTRACT. A key disadvantage of software verification over other quality assurance techniques, such as testing, is its unpredictable cost. A lot of people-hours have to be invested before correctness can be proved, and, in contrast to testing, there is no quantifiable evidence that incremental verification effort results in incremental quality improvements. On the other hand, the process of verifying code can be seen as a sort of audit or code-walk, so there is an intuition that the process itself improves quality, even before a proof can be computed. In this paper we discuss our first attempts to quantify the incremental quality improvements that are achieved during verification using a metric called verification coverage.

ABSTRACT. In Europe, the development of safety-critical rail IT is regulated by the Common Safety Method (CSM 352) and CENELEC standards. The CSM requires the railway undertaking to unambigously specify requirements on equipment. The infrastructure branch of German Railways (DB Netz) has chosen to base the specications of interlockings and related equipment like eld element controllers on SysML statecharts. Although these specications will be more consistent and precise than the text-based ones in use before, this approach faces opposition from manufacturers who find it difficult to justify the correctness of their implementation.

This paper reports on the approach, its motivation and its practical difficulties, and it endeavours to identify its merits and weaknesses.

ABSTRACT. Ensuring the correctness of program compilations is an important step in assuring the correctness of an overall software system. In this work, we describe an effort to verify he SSA (single static assignment) compiler transformation, which turns memory references (i.e., load, store) into corresponding register references (i.e., read, write). It is one of the most important optimizations in modern compilers, and may account for more than half of the optimization speed up. Formally verifying the algorithm behind this transformation is thought to be a difficult task. Verifying the actual code, as implemented in a production compiler, is currently infeasible. We describe an alternative verification strategy, based on generating and checking ``witnesses'' for each instance of the transformation. This approach enormously simplifies the verification task, primarily because it does not require showing that the transformation code is correct.

ABSTRACT. The number of recalls of medical devices with embedded computers due to safety issues in recent years suggests there is a need for new approaches to support the process. There is increasing concern about the impact of systematic use errors. There has been little research focusing on model-based tool support for the assurance and certification of medical devices with respect to systematic use error, however. The CHI+MED project (http://www.chi-med.ac.uk) aims to address this gap. It is concerned with the design of safer medical devices with a specific focus on human-computer interaction. We are developing a range of integrated model-based engineering methods and other formal and semi-formal techniques to support the certification process, both pre- and post-market, including their use in the wider system context. In this position paper we review our approach and the contributions to date.

ABSTRACT. In joint work with several industrial and academic partners throughout Europe, we are working towards the certification of PikeOS -- an industrial separation kernel developed at SYSGO -- according to the highest level of the Common Criteria. We present a new generic model of separation kernels that includes interrupts, control and context switches. For this generic model, noninterference has been proven in the Isabelle/HOL theorem prover from proof obligations on the step function. Noninterference holds for all separation kernels which satisfy these assumptions. In this paper, we discuss this methodology for certification purposes. On the one hand, it is clear that our instantiation of the step function for PikeOS must satisfy the proof obligations. On the other hand, there are many implicit assumptions made in defining the run function, that is, in defining how the step function is applied. Based on work-in-progress, we address the issue of providing evidence that PikeOS indeed satisfies our generic notion of noninterference.

ABSTRACT. This paper reviews the results of our recent research in assurance and verification of embedded software systems. This research was part of an effort in which we prepared evidence, including an abstract formal model and mechanical proofs, of the security of an embedded system implemented in the C language. It then describes the evidence provided for the certification and how this evidence might be presented in an assurance case The paper also describes our more recent research on SecProve, a tool for automatically checking the security of C programs during their development. It concludes by listing some open research problems in system assurance and verification.

ABSTRACT. Nowadays formal methods represent a powerful but in practice not well supported way for verification. One reason among others for this is that such methods are often conceived of being too theoretical, can likely be misunderstood by non-experts, and notations are therefore misapplied.

For example to specify formal specifications, complex logics are state-of-the-art, especially for probabilistic verification properties. It is not only that users are unable to construct correct specifications but they also miss to understand what is meant by the verification results based on the specification.

In this paper we address this problem and endorse the usage of a graphical notation to construct such specification properties, especially probabilistic ones. We present how such a notation may look and emphasize that one single notation is sufficient to solve both lack of comprehensibility of the specification as well as of the verification results. Moreover, we extract some future research directions.

ABSTRACT. Abstract--In this paper we consider two ways of using both formal-logical models based on Model Checking and Markov probabilistic models for semi-automatic verification of robustness to Soft Errors of a target design, and assurance of these properties as well. One of this approach to verification is well-known Probabilistic Model Checking while another is suggested recently a combination of traditional Model Checking with a two–dimensional Markov chain. A comparison of computational complexities of these approaches shows that combination of Model Checking formal verification with analysis of fault-tolerant property could reduce overall design cost, what can increase considerably the formal verification tools effectiveness.