Formal veri cation has the potential to provide a level of evidence based assurance not possible by more traditional development approaches. For this potential to be ful lled, its integration into existing practices must be achieved. Starting from this premise, the position paper discusses the opportunities created and the challenges faced by the use of formal veri cation in the analysis of critical interactive computing systems. Three main challenges are discussed: the accessibility of the modelling stage; support for expressing relevant properties; the need to provide analysis results that are comprehensible to a broad range of expertise including software, safety and human factors.
Safety and mission critical interactive computing systems require a level of evidence based assurance that traditional user centred approaches alone cannot provide. For this reason user centred approaches must be integrated with hazard analysis and risk assessment approaches to guarantee safety. Such processes are required to comply with regulatory requirements. Current approaches to provide evidence for safety, are typically based on inspection and testing techniques making it hard to guarantee an adequate level of safety assurance at a reasonable cost/e ort level.
Formal veri cation tools promise the scaleable analysis of components of real systems including interactive systems. They enable exhaustive analysis of use centred safety requirements as part of a risk analysis. This position paper discusses extensions to existing tools for formal modelling and analysis that have the potential to enable their use by current development teams who are not expert in formal methods. In doing this, it discusses requirements for formal toolsets that would aid their acceptability by development teams. The requirements are discussed using the IVY toolset as an example. 2
Formal veri cation, applied to interactive computing systems, has seen
considerable development, mostly at the model-based level3 [
Tools such as the IVY workbench have been shown to be applicable to real
systems [
These activities are consistent with recent progress in \lightweight formal
methods" (LFM). According to Zamansky et al.'s review [
The focus of this discussion is the analysis of safety issues associated with user interaction with software devices. The main problem with the use of formal techniques is that there can be a substantial learning curve associated with their use. Software engineers and human factors specialists have not been trained to use them. This lack of expertise is particularly signi cant when it is considered that many safety critical systems are developed by small teams of innovators. This is certainly the case, for example, in medical device development. Medical devices are often safety critical. They are often innovative and developed by small teams attached to hospitals where the drivers for the design have a medical background. They are not software engineers (or programmers) or HCI experts. The problem of safety analysis of these devices presents important challenges. Safety is usually seen (quite reasonably) in terms of clinical trials where the key focus is the clinical advantage of a functional medical device.
While it can be argued that formal veri cation has proved its worth in a
number of practical applications, the challenge now is to make the tools available
to a wider audience. How to make these techniques accessible to the small teams
that develop these safety critical devices. This is the goal of the LFM community.
The concern here is to make the models and analysis tools of formal methods
accessible to a broader community. The experience of using the IVY tool to
support the safety analysis of a neonatal dialysis machine [
Each of these topics will now be addressed. 3.1
Making the modelling stage accessible to developers
The modelling stage must be made more accessible to non-formal methods
experts. Building formal models of interactive systems is not the typical approach
to developing interactive computing systems, which often relies on the
development of prototypes. There is, then, a gap to be lled between the practices of
developers and the models needed for analysis. This must be lled by looking at
what the current practices are, and how whatever design and development
artefacts are used might be fed into the veri cation process (see [
One approach to make this accessible to developers is to establish common patterns for the architectures of components of interactive systems, to provide a framework that can be populated in the case of the particular system. This process produced the model that formed the basis for the controller in the case of the neonatal dialyser. The developers had already produced a spreadsheet that represented the state transition model that formed the basis for analysis. The spreadsheet was also used in the implementation of the controller for the device. The modelling problem then becomes one of choosing the architecture and populating it.
Several existing notations provide starting points for modellers, see for
example [
Supporting the expression of relevant properties for veri cation The process of creating properties for veri cation is particularly challenging and one where the integration with existing practices is both more critical and more likely to create added value. The risk analysis process is often based on a set of informal requirements. Sometimes these requirements are based on previous cases, as risk logs. The risk requirements speci ed in the risk log are designed to mitigate hazards and may have software, hardware or human aspects to them. A safety requirement may demand an operating procedure or it may suggest a formal requirement that must be true of a software component, for example. This latter possibility could lead to formal analysis of the model of the system. The problem for the safety analysis then is to decide which aspects of a requirement can be captured by properties of a formal model and to provide a formal expression of the property.
Support for specifying these requirements is currently provided by the
adoption of property speci cation templates [
A process such as the above will be made easier through some degree of
automation. Tool support is needed to go from risks, described in the logs, to
properties for veri cation that capture the risk being considered (natural
language processing techniques might be useful here [
Providing analysis results in ways that are understandable by, and useful to, developers When veri cation fails, the causes of failure need to be identi ed and investigated. The counter-examples produced by model checkers can be particularly useful here, but need to be presented in an understandable manner.
Several alternatives can, and have been, explored to this end. Tools such as
IVY provide a number of graphical representations to that purpose. These
however assume a technical nature (tabular or activity diagram based representations
of the states of the system in the counter example) that might not necessarily be
the most appropriate for non-experts. At the other end of the spectrum, tools
such as PVSio-web [
A mid-way, more exible approach, is explored in [
Formal veri cation can provide a level of evidence based assurance that more traditional development approaches do not guarantee. In this paper we have discussed opportunities and challenges of its use with interactive computing systems. A common thread between the challenges is that the formal analysis process must be integrated into existing practices, being driven by them and not forcing developers to change their current practices. Areas where broad interdisciplinary comprehension is necessary to achieve this integration have been identi ed and brie y discussed.
This work is nanced by the ERDF - European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundac~ao para a Ci^encia e a Tecnologia, within project POCI-01-0145-FEDER-016826.