New Opportunities for Integrated Formal Methods
Mario Gleirscher Simon Foster Jim Woodcock






Department of Computer Science, University of York, United Kingdom

  Deramore Lane, Heslington, York YO10 5GH

[1]Partly funded by the Deutsche
  Forschungsgemeinschaft (DFG, German Research Foundation) under the
  Grant no. 381212925.
   2019. This is the author's version of the work. It is posted here for
  your personal use. Not for redistribution. The definitive version was published
  in ACM Computing Surveys, <https://doi.org/10.1145/3357231>.
 

New Opportunities for Integrated Formal Methods^1
    Jim Woodcock
    December 30, 2023
=================================================


  Formal methods have provided approaches for investigating software
  engineering fundamentals and also have high potential to improve
  current practices in dependability assurance.  In this article, we
  summarise known strengths and weaknesses of formal methods.  From
  the perspective of the assurance of RAS, we highlight new
  opportunities for integrated formal methods and identify threats to
  the adoption of such methods.  Based on these opportunities and
  threats, we develop an agenda for fundamental and empirical research
  on integrated formal methods and for successful transfer of
  validated research to RAS assurance.  Furthermore, we outline
  our expectations on useful outcomes of such an agenda.


 

3





§ INTRODUCTION



A plethora of difficulties in software practice and momentous software
faults have been continuously delivering reasons to believe that a
significantly more rigorous discipline of software engineering is
needed <cit.>.
Researchers such as <cit.> have collected plenty of
anecdotal evidence on software-related risks substantiating this
belief.

In DSE, researchers have turned this
belief into one of their working hypotheses and contributed
formalisms, techniques, and tools to increase the rigour in
engineering workflows <cit.>.  Examples
of activities where formalisms have been brought to bear include
requirements
engineering <cit.>,
architecture design and verification, test-driven development, program
synthesis, and testing, to name a few.  FM have
been an active research area for decades, serving as powerful tools
for theoretical researchers.  As a paradigm to be adopted by
practitioners they have also been investigated by applied
  researchers.  Applications of FM have shown their strengths
but also their weaknesses <cit.>.

Based on observations contradicting the mentioned difficulties,
<cit.> came to ask “How did software get so
reliable without proof?”  He, and later
<cit.>,
suggested that continuously improved design of programming languages
and compilers, defensive programming, inspection, and testing must
have effectively prevented many dangerous practices.
 coined the
“Hoare paradox” stating that although proof was seldom used,
software had shown to be surprisingly fit for purpose.  However, faced
with software of increasing complexity (RAS),
 pondered how long
's question will remain valid.

Indeed, recently we can observe a plethora of difficulties with
RAS <cit.>.  Such
systems are set to be more broadly deployed in society, thereby
increasing their level of safety criticality <cit.> and
requiring a stringent regulatory regime.  A successful method for
regulatory acceptance is provided by structured assurance cases, which
provide comprehensible and indefeasible safety arguments supported by
evidence <cit.>.  However, such
assurance cases—whether or not compliant with standards like
IEC 61508[For: Functional Safety of
  Electrical/Electronic/Programmable Electronic Safety-related
  Systems.] and DO-178C[For: Software Considerations in
  Airborne Systems and Equipment Certification.]—can be laborious to
create, complicated to maintain and evolve, and must be rigorously
checked by the evaluation process to ensure that all obligations are
met and confidence in the arguments is
achieved <cit.>. Nevertheless, these are
problems that FM are designed to overcome.

In spite of the weaknesses of current FM, and encouraged by
their strengths, we believe that their coordinated use within
established processes can reduce critical deficits observable in
dependable systems engineering.  <cit.> state that
“there is currently no general framework integrating formal methods
for robotic systems”.  The authors highlight the use of what are
called iFM[We reuse the term from the homonymous
  conference
  series <cit.>.]  in
the construction of assurance cases and the production of evidence as
a key opportunity to meet current RAS challenges.  Particularly,
computer-assisted assurance techniques <cit.>, supported
by evidence provided by iFM, can greatly increase confidence in
the sufficiency of assurance cases, and also aid in their maintenance
and evolution through automation.  Moreover, the use of modern
FM-based tools to support holistic simulation, prototyping,
and verification activities, at each stage of system, hardware, and
software development, can lead to systems that are demonstrably safe,
secure, and trustworthy.



 §.§ Contribution



We investigate the potentials for the wider adoption of
  integrated formal methods in dependable systems engineering, taking
RAS as a recent opportunity to foster research in such methods
and to support their successful transfer and application in practice.

We analyse the strengths, weaknesses, opportunities, and
  threats of using formal methods in the assurance of dependable
systems such as RAS.  For this analysis, we summarise experience
reports on formal method transfer and application.

Assuming that
[(a)]

  * integration enhances FM and 

  * the assurance of RAS is a branch of DSE,

<Ref> shows how we derive an
agenda for fundamental and applied iFM research.

From the strengths, we see in recent research, and from the
opportunities in current RAS assurance, we argue why this
domain is a key opportunity for iFM.  Particularly, we indicate
how such methods can meet typical assurance challenges that RAS
are increasingly facing.

From the weaknesses, we observe in recent research, and from the
threats FM research transfer is exposed to, we derive
directions of foundational and empirical research to be taken to
transfer iFM into the assurance of robots, autonomous systems,
and other applications, and to use these methods to their maximum
benefit.



Our analysis


  * elaborates on the analysis and conclusions of
  <cit.>,

  * extends their suggestions with regard to formal method
  experimentation and empirical evidence of effectiveness focusing on
  collaboration between formal method researchers and practitioners,
  and

  * develops a research and research transfer road map, placing
  emphasis on RAS.




 §.§ Overview



We provide some background including
terminology (<Ref>) and related
work (<Ref>) in the following.  Then, we carry
through an analysis of strengths, weaknesses (<Ref>),
opportunities (<Ref>), and
threats (<Ref>) of iFM for RAS assurance.
Based on this analysis, we formulate our
hypotheses (<Ref>), pose research questions based on
these hypotheses, derive a research agenda, and specify some outcomes
we expect from this agenda (<Ref>).



§ BACKGROUND



This section introduces the core terminology used throughout this
article, and provides a discussion of other surveys of the FM state
of the art and a summary of similar positions and agendas.



 §.§ Terminology



For the sake of clarity among readers of different provenance, we restrict
the meaning of some terms we use in the following and introduce
convenient abbreviations.

We view robots and autonomous systems as both dependable
systems and highly automated machines capable of achieving a variety
of complex tasks in support of humans.  We can consider such systems
by looking at four layers: the plant or process composed of the
operational environment and the machine; the machine itself; the
machine's controller, and the software embedded into this controller.
Based on these layers, we treat “embedded system” and “embedded
software” as synonyms.  Machine, controller, and software can all be
distributed.

By dependable systems engineering, we refer to error-avoidance
and error-detection activities in control system and embedded software
development (according to the V-model).
<cit.> devised a comprehensive
terminology and an overview of the assessment and handling of a
variety of faults, errors, and failures.  For critical systems, such
activities are expected to be explicit (traceable, documented),
to employ best practices (design patterns), and to be driven by
reasonably qualified personnel (well-trained and experienced
engineers or programmers).

The need for dependability often arises from the embedding of
software into a cyber-physical context (an electronic execution
platform, a physical process to be controlled, and other systems or
human users to interact with).  DA, or
assurance for short, encompasses the usually cross-disciplinary task
of providing evidence for an assurance case (safety, security,
reliability) for a system in a specific operational
context <cit.>.

By formal methods, we refer to the use of formal (mathematically precise and unambiguous) modelling languages to
describe system elements, such as software, hardware, and
the environment, and the subjection of models written in these
languages to analysis <cit.>, the results of which are
targeted at assurance <cit.>.
FM always require the use of both formal syntax and
formal semantics (the mapping of syntax into a
mathematical structure).  Semantics that allows the verification of
refinement or conformance across different FM is said to be
unifying <cit.>.  iFM allow the
coordinated application of several potentially heterogeneous FM,
supported by interrelated layers of formal
semantics <cit.>.

FM stand in contrast to informal methods, which employ
artefacts without a formal syntax or semantics, such as natural
language descriptions and requirements. In the gap between informal
methods and FM there is also a variety of semi-formal
  methods, including languages like the UML and the SysML,
whose syntax and semantics have frequently been subject of
formalisation in
research <cit.>.

FM-based tools assist in the modelling and reasoning based
on a FM.  MBD and MDE served many opportunities for
FM-based tools to be applied in dependable systems
practice <cit.>.[The SCADE Design
  Verifier (<http://www.esterel-technologies.com>) and the seL4
  microkernel (<http://sel4.systems>) represent good although less
  recent examples.]

We speak of applied or practical FM to signify successful
applications of FM in a practical context, to develop
embedded control software deployed in a commercial product marketed by
an industrial company.  We consider the use of FM in research
projects still as FM research.  Empirical FM
  research investigates practical FM, using surveys, case
studies, or controlled field
experiments <cit.>.  We speak of
FM transfer if FM research is transferred into
practice with the aim to effectively apply and practice FM.  We
consider FM transfer, as discussed below, as crucial for
empirical FM research and progress of iFM research.



 §.§ Related Work



Many researchers have suggested that FM will, in one way or another,
play a key role in mastering the difficulties discussed below and in
achieving the desired guarantees (dependability, security,
performance) of future critical
systems <cit.>.

Expecting an increased use of FM to solve practical challenges in the
mid 1990s, <cit.> suggested FM
integration, tool development, and continuous specialist training to
foster successful FM transfer to practice.

In 2000, <cit.> observed a growing number of FM
success stories in requirements engineering.  Evaluating several FM
paradigms, he outlined weaknesses (isolation of languages, poor
guidance) to be compensated and challenges to be met towards effective
FM use, particularly their integration into multi-paradigm
specification languages.

Aiming at the improvement of software dependability,
<cit.> made several key
observations of recent dependability practice (lack of evidence
for method effectiveness) leading to a general proposal with broad
implications: rigorous dependability cases with explicit claims, the
support of reuse and evolution, and the selective use of FM.
Additionally, these authors provide a number of recommendations to
tool vendors and organisations in education and research.

Also in the mid 2000s, <cit.>
spotted a decline of internet software dependability in the context of
an increased level of concurrency in such systems.  Their observation
was backed by an earlier comparative software/hardware dependability
discussion by <cit.>.
 highlighted
achievements in FM automation enabling an increased use of lightweight
FM in “software engineers' usual development environments”.
Furthermore, they stressed the ability to use several FM in a combined
manner to verify distributed (embedded) systems, avoid errors and,
hence, stop the decline of software dependability.

<cit.> issued a manifesto for a
“Verified Software Initiative”.  Based on a consensus of strengths,
weaknesses, opportunities, and threats in the software engineering
community, they proposed a long-term international “research program
towards the construction of error-free software systems”.  This
initiative aims to achieve its agenda through
[(1)]

  * new theoretical insights into software development,

  * creation of novel automated FM tools, and

  * a collection of experiments and benchmarks.

In particular, the initiative is driven by a number of “grand
challenges” <cit.>—difficult practical verification
problems that can guide future research.  The experiments have broad
scope, and include a smart cash card <cit.> (the Mondex
card), a secure entry system[Tokeneer Project Website:
  <https://www.adacore.com/tokeneer>.] (Tokeneer), and a cardiac
pacemaker.[Pacemaker Formal Methods Challenge:
  <http://www.cas.mcmaster.ca/sqrl/pacemaker.htm>.]

Outlining an agenda for FM transfer,
<cit.>
raised the need for improved benchmarks, metrics, and infrastructure
for experimental evaluation, the need for revised teaching and
training curricula <cit.>,
and the need for research communities interested in engaging with
practitioners and working on ways to scale FM up to large systems and
to increase the usability of FM.  The authors specified several
applications with great opportunities for FM transfer.

  

Applied researchers and practitioners interviewed by
<cit.> convey an optimistic picture
of FM adoption in practice, highlighting the potentials to improve IT
security, particularly in cyber-physical systems.
<cit.> share the view that FM are the
most promising approach towards acceptably dependable and secure
systems.  The challenges they list for the security domain are similar
to the challenges we perceive in RAS assurance: FM integration, sound
abstraction techniques, compositional guarantees, and evidence for
sustainable transfer.

With their survey of FM for RAS verification,
<cit.> identified
difficulties of applying FM in the robotics domain and summarised
research results and their limitations.  They conclude
[(i)]

  * that formalisation remains the most critical and most difficult task,

  * that the surveyed approaches do not provide “sufficient
  evidence for public trust and certification”, and

  * that iFM would be highly desirable if the current lack of
  translations between the most relevant of the surveyed
  techniques (model checking) could be overcome.

We complement their observations with a further analysis of the lack
of unification of FM and of the missing empirical evidence for the
effectiveness of FM and iFM.  Additionally, we provide a research
road map.



§ STRENGTHS AND WEAKNESSES OF FORMAL METHODS FOR ASSURANCE




Following the guidelines for SWOT analysis
by <cit.>, we provide an overview of
strengths and weaknesses of FM, regarding


  * reputation, proof culture, education, training, and use (<Ref>),

  * transfer efforts (<Ref>),

  * evidence of effectiveness (<Ref>),

  * expressivity (<Ref>), and

  * integration and coordination (<Ref>).




 §.§ Reputation, Proof Culture, Education, Training, and Use



In the guest editor's introduction of the “50
Years of Software Engineering” IEEE Software special theme
issue <cit.>, the question

  “Are formal methods essential, or even useful, or are they just an
  intellectual exercise that gets in the way of building real-world
  systems?”

invited us to deliberate on
this topic and summarise its highlights.  Applied researchers have
raised the issue of limited effectiveness and productivity of
FM, particularly in large practical systems with changing
requirements <cit.>.
FM are known to be difficult to apply in practice,
and bad communication between theorists and practitioners
sustains the issue that FM are taught but rarely
applied <cit.>.
In contrast, they are considered to have significant potential to cope
with the toughest recent engineering problems: certifiable RAS
assurance <cit.>.

Studying the sociology of proof,
<cit.> identified three
sources of knowledge about a system's dependability: induction (from observation), authority (expert opinion), and
deduction (inference from models) which is possibly the most powerful.
Since the beginning of software engineering there has been a debate on
the style of deductive reasoning about programs and on the usefulness
of FM.
<cit.> argued that proof is a social
process.  Long and difficult to read computer-produced verification
evidence cannot be subject to such a process and is not genuine proof.
<cit.> countered, albeit not as
a supporter of mechanisation, to change from a personal trust-based culture
of proof to the formalisation of proof steps.
<cit.> doubted that verification
based on a model of the program can yield any knowledge about the
dependability of an implementation of that program.
According to <cit.>, it is not the
degree of formalisation making a proof convincing but the way the
argument is organised.
 tried to
arbitrate this debate between rigorous proof in ordinary mathematics
and formal mechanised proof.  He suggested that proof assistants have
the potential to use formal
methods <cit.> to the maximum benefit.
<cit.> concluded from a
discussion with Tony Hoare that formalist and empiricist perspectives,
while still causing controversies between research and practice,
complement each other in a fruitful way.

Nevertheless, FM have shown to be well-suited to
substantially improve modelling precision, requirements clarity,
  and verification confidence.  FM applications in requirements
engineering such as the “Software Cost Reduction”
tool set <cit.> even carry the
hypothesis of FM cost-effectiveness in its name.
By the 1990s, FM researchers had already started to examine FM
usefulness with the aim to respond to critical observations of
practitioners <cit.>.  Some of these efforts
culminated in empirical studies
<cit.> suggesting
high error detection effectiveness, though with some
controversy also caused by employed research designs
<cit.>.

<cit.> observe
that the combination of formal[ “Formal” refers to
    the formality of the procedure but does not imply the use of
    formal semantics or mathematical techniques.]  inspection, static
analysis, and formal testing has been the best approach to defect
prevention with up to 99% of accumulated defect removal
  efficiency.  FM can be seen as a rigorous and systematic form
of this approach, though less often applied.  In
<Ref>, we make a brief excursion to the
relationship between FM and formal inspection and try to roughly
estimate the population size of FM users.

From two larger surveys, one in the early 1990s
<cit.> and another one in the late
2000s <cit.>, we obtain a more
comprehensive picture of the typical advantages of FM use and barriers
to FM adoption as seen by practitioners and practical FM researchers.
In two recent surveys
<cit.>,
we made two, not necessarily surprising but empirically supported,
observations underpinning the main findings of the former studies:
many practitioners view FM as promising instruments with
high potential, and would use these instruments to their maximum
benefit, whether directly or through FM-based tools.  However,
the beneficial use of FM is still hindered by severe
obstacles (FM are considered hard to learn, difficult to
integrate in existing processes, too expensive, prone to invalid
abstractions, difficult to maintain).


  FM can improve RAS modelling, the specification of
  RAS requirements, and the automation of RAS verification,
  fostering the early detection of systematic errors in RAS
  designs.
  Many assurance practitioners perceive FM usefulness as
  positive.


  FM have shown to be difficult to learn and apply.  Many
  assurance practitioners perceive the ease of use of FM as
  negative.  Moreover, research has been ineffectively communicated in
  FM teaching and training.




 §.§ Transfer Efforts
 


FM can be effective in two ways, ab-initio (before
implementation) and post-facto (after implementation).
The ab-initio use of FMs aims at reducing late error costs through,
formal prototyping, step-wise refinement, formal test-driven
development, crafting module assertions prior to programming, or
formal contract-based development.  Once an initial
formalisation (invariants) is available, it is argued for
families of similar systems that, from the second or third FM
application onward, the benefit of having the formalisation
outperforms the cumulative effort to maintain the formalisation up to
an order of
magnitude <cit.>.
This argument also addresses agile settings inasmuch as iterations or
increments refer to similar systems.
The post-facto use of FM can occur through knowledge extraction
from existing artefacts and using automated tools such as, formal
or model-based post-facto testing tools or post-facto use of code
assertion checkers <cit.>.  Overall, the second way of
utilising FM is known to be more compatible with everyday
software practice.

Achievements collected by <cit.>,
<cit.>, and <cit.> show that many
researchers have been working towards successful
  FM transfer.  Moreover, researchers experienced in particular
FM draw positive conclusions from FM applications,
especially in scaling FM through adequate tool support for
continuous reasoning in agile software
development <cit.>.  Other researchers report
about progress in theorem proving of system software of industrial
size <cit.> and about
FM-based tools for practical
use <cit.>.
MBD and MDE have a history of wrapping FM into software
tools to make access to formalisms easier and to help automating
tedious tasks via DSL and visual
notations.

Static (program) analysis is another branch where
FM-based tools have been successfully 
practised <cit.>.
However, few static analysis tools are based on FM and many
of these tools are exposed to reduced effectiveness because of
high false-positive rates, particularly if settings are not
perfectly adjusted to the corresponding
project <cit.>.

Furthermore, the concolic testing technique <cit.>, a
post-facto FM, has seen multiple successes in
industry <cit.>. It exercises all possible
execution paths of a program through systematic permutation of a
sequence of branch conditions inferred by an instrumented concrete
execution. It uses these symbolic execution paths and SMT solving to
obtain a series of inputs that exercise the full range of program
paths. It does not depend on a predefined model of the program, but
effectively infers one based on the branch conditions. It can
therefore readily be used on existing program developments, and has
notably been used by Samsung for verification of their flash storage
platform software <cit.>. Indeed, it is a belief of the
authors of this latter work that post-facto methods provide greater
opportunities for adoption of FM in industry.

Recently, there have been several developments in the use of FM
to assure safety requirements related to HCI, and a growing body
of
literature <cit.>,
particularly relating to certification of commercial medical
devices <cit.>.  There,
FM have been shown to be successful in facilitating
regulatory acceptance, with the FDA agency in the United
States. <cit.> formalised the FDA
regulatory safety requirements for the user interface of a
patient-controlled infusion pump, and used the PVS proof assistant to
verify it.  <cit.>, similarly, formally modelled
an infusion pump interface, using the Z notation, and then used the
resulting specification as an oracle to generate test cases.
<cit.> performed risk analysis for a new
neonatal dialysis machine, formalised safety requirements, and use
these requirements to analyse and verify the source code.  The
consensus of these authors is that FM can greatly reduce the
defects in safety critical HCI prior to deployment.  The
techniques are increasingly practically applicable through greater
automation.  Moreover, it is likely that these results have potential
applications in other domains, such as RAS, provided they can be
transferred and scale to this greater complexity.


  There exist many transfer re-entry points from a range of insightful
  FM case studies in industrial and academic labs.  FM were
  demonstrated to be a useful basis for many static analysis and
  MDE tools.


  The number of practical (comparative) case studies using (ab-initio)
  FM or iFM, particularly on RAS, is still too low
  to draw useful and firm conclusions on FM effectiveness.




 §.§ Evidence of Effectiveness



Whether used as ab-initio or post-facto tools, strong evidence
for the efficacy of FM in practice is still
  scarce <cit.> and
more anecdotal
<cit.>,
rarely drawn from comparative studies
<cit.>,
often primarily conducted in research labs
<cit.>, or not recent enough to
reflect latest achievements in verification tool
research <cit.>.  We
observe that a large fraction of empirical evidence for FM
effectiveness can be classified as level 6 or 7 according to
<cit.>, too weak to draw
effective conclusions.

<cit.> as well as
<cit.>, two
researchers from the software engineering measurement community,
support this observation.
 state that “there is
very little empirical data on several topics that need to be well
understood if proofs of correctness are to become useful tools for
professional software development as opposed to academic
experiments”.  Moreover, the controversies about proof culture
summarised in <Ref> contain little data to
resolve practitioners' doubts.  

<cit.> observed this lack of evidence of FM
effectiveness in assurance argumentation.  More generally,
<cit.> noticed insufficiently evaluated safety research.
About 86% of works lack guidance to reproduce results, hence forming
a barrier to the advancement of safety practice.  Although their study
is limited to one conference series, it indicates deficiencies in the
evaluation of DA research.
Overall, it is important to understand that the mentioned lack of
evidence and successful transfer produces great opportunities for
further empirical and theoretical FM research.


  For (comparative) studies of FM effectiveness, there are
  several research designs and benchmark examples available from the
  scientific literature.  In <Ref>, we assess
  the effort and feasibility of corresponding qualitative and
  quantitative studies.


  FM have been suffering from fragile effectiveness and
  productivity in dependability engineering in general.
  There is a lack of convincing evidence of FM effectiveness,
  particularly, of ab-initio FM.  RAS engineering and
  assurance are likely to be affected by these weaknesses.




 §.§ Expressivity



An often quoted weakness of MBD, particularly when applied to
RAS, is the “reality gap” <cit.> that
can exist between a naively constructed model and its corresponding
real-world artefact.  According to <cit.>, over-reliance
on simulation to test behaviour using naive and insufficiently
validated models can lead to effort being applied to solving problems
that do not exist in the real world. Worse, programs for robotic
controllers developed in a model-based setting may fail when executed
on real-world hardware, because “it is very hard to simulate the
actual dynamics of the real-world” <cit.>. This problem is
not only true of simulation, but any form of model-based analysis,
including reasoning in FM
<cit.>.

The fundamental problem here is that it is impossible to model the
behaviour of any physical entity precisely <cit.>, unless we
replicate the original. Moreover, as models become more detailed,
their utility decreases and they can become just as difficult to
comprehend and analyse as their real-world counterparts, an
observation highlighted by the famous paradox of
<cit.>. Nevertheless, as statistician George Box said
“all models are wrong but some are useful” <cit.>: we must
evaluate a model not upon how “correct” it is, or how much detail it
contains, but on how informative it is.  According
to <cit.>, the antidote is not to abandon the use of models,
but to recognise their inherent limitations and strengths, and apply
them intelligently to reasoning about a specific problem.  This means
selecting appropriate modelling paradigms that enable specification of
behaviour at a sufficiently detailed level of abstraction, and using
the resulting models to guide the engineering process.


  FM allow and foster the use of specific abstractions to
  specifically inform engineers of RAS properties critical for
  their assurance.


  The effectiveness of formal models is fragile and can be
  significantly reduced because of uncontrollable gaps
  between models and their implementations.




 §.§ Integration and Coordination



Modelling notations usually employ a particular paradigm to abstract
the behaviour of the real-world.  For example, the state-based
paradigm, employed by FM like Z <cit.>,
B <cit.>, and refinement
calculus <cit.>, considers how the internal
state of a system evolves, whilst the event-driven paradigm, employed
in process calculi like CSP <cit.>,
CCS <cit.>, and
π-calculus <cit.>, considers how behaviour
may be influenced by external interactions. Consequently, individual
formal methods are usually limited to considering only certain aspects
or views of a system's
behaviour <cit.>,
which can limit their effectiveness when used in isolation.  Many
researchers have therefore sought to overcome this weakness by FM
integration <cit.>.

The 1990s saw a large number of works on semantic unification and
method
integration <cit.>.
Theoretical foundations were provided by
, in his seminal work on
semantic unification using the “programs-as-predicates”
approach <cit.> and
comparative semantics <cit.>.  At the same time, refinement
calculi were developed <cit.> that would
underlie the work on linking heterogeneous notations through
abstraction.  Also, <cit.> explored the
integration of state- and event-based modelling using weakest
preconditions, and several other works on this topic
followed <cit.>.
 proposed a unified theory of
programming <cit.> that links together the
three semantic styles: denotational, operational, and algebraic. These
developments culminated in
's
UTP <cit.>, a general
framework for integration of semantically heterogeneous notations by
application of 's
approach <cit.> to the formalisation of a catalogue
of computational paradigms, with links between them formalised using
Galois connections.  This framework enables a definitive solution to
the integration of states and events, along with other computational
paradigms, in the Circus language
family <cit.>.

Another result of these developments was a number of seminal works on
FM integration <cit.>.
, inspired by work on
systematic method integration <cit.>,
defined a generic “meta-method” that aimed at integration of several
formal and semi-formal methods using notational translations with a
common predicative semantic foundation, which builds on
's work <cit.>. Meanwhile,
<cit.>, building on their
previous work <cit.>, likewise proposed the creation
of hybrid FM with a multi-paradigm approach.  Moreover,
<cit.> proposed that FM
should be integrated into the V-Model of 
development <cit.> with common semantic
foundations to link the various artefacts across development
steps.

These diverse efforts eventually led to the founding of the iFM
conference series in
1999 <cit.>, with the
aim of developing theoretical foundations for “combining behavioural
and state-based formalisms”.  For the second iteration of the iFM
conference <cit.>, the scope
broadened to consider all the different aspects of FM
integration, including semantic integration, traceability, tool
integration, and refinement. A few years later, a conference series
was also established for UTP <cit.>, with the aim
of continuing to develop unifying semantics for diverse notations
within the UTP framework.

However, there is as yet no agreed and general methodology for
integrating FM that could be applied to
RAS <cit.>.  Overall, integration is of particular
pertinence to RAS, since such systems are multi-layered and
possess a high degree of semantic heterogeneity.  As
 found, they “can be variously categorised
as embedded, cyber-physical, real-time, hybrid, adaptive and even
autonomous systems, with a typical robotic system being likely to
contain all of these aspects”.  When we consider RAS, we must
consider advanced computational paradigms like real-time, hybrid
computation with differential equations, probability, and rigid body
dynamics. This implies the use of several different modelling
languages and paradigms to describe the different aspects, and
therefore a variety of analysis techniques to assure properties of the
overall system.  Assurance of autonomous systems will certainly
therefore require iFM <cit.>.
<Ref> on page fig:refinedapproach
summarises this relationship.


  iFM raise the potential of integration and coordination of
  several FM to consistently reason about RAS properties
  implemented by a combination of various technologies such as
  software, electronic hardware, and mechanical hardware.


  There is currently no agreed framework for the integration of
  FM that would effectively address the needs in the RAS
  domain or similar domains.




§ OPPORTUNITIES FOR INTEGRATED FORMAL METHODS




This section continues with the environmental part of our
SWOT analysis.  Several key opportunities for the transfer of
iFM arise from ongoing assurance challenges, particularly in
RAS assurance and from looking at what other disciplines do to
cope with similar challenges.  In the following, we describe
opportunities stemming from


  * the desire for early removal of severe
  errors (<Ref>),

  * the desire to learn from accidents and their root
  causes (<Ref>),

  * the desire of assurance to form a mature
  discipline (<Ref>), and

  * the desire for adequate and dependable
  norms (<Ref>).




 §.§ The Desire for Early Removal of Severe Errors



Summarising major challenges in automotive systems engineering in
2006, <cit.> indicated
that modelling languages used in practice were often not formalised
and the desired benefits could not be achieved from semi-formal
  languages.  Moreover, software engineering was not well
  integrated with core control and mechanical engineering processes.
Domain engineers would produce software/hardware sub-systems and
mechanical sub-assemblies in undesirable isolation.
 referred to a lack
of iFM for overall architecture verification.

Has the situation changed since then?
In model-centric development in embedded software practice (based
on UML or SysML), drawbacks can be significant if methods
and tools are not well integrated or trained personnel are
missing <cit.>.  Likely,
's criticism remains
in contemporary automatic vehicle engineering and assurance practice.
In fact, he has a recent, clearly negative, but not pessimistic answer
to this question <cit.>.  Moreover,
this view is shared by the Autonomy Assurance International
Programme's discussion of assurance barriers,[See
  <https://www.york.ac.uk/assuring-autonomy/body-of-knowledge/>.]
current challenges in RAS assurance.  These barriers (validation, verification, risk acceptance, simulation, human-robot
interaction) could be addressed by formal engineering models and
calculations based on such models to be used as evidence in assurance
cases.


Model-based assurance <cit.> uses system models
to structure assurance cases and represents another opportunity for
formal methods in (through-life) assurance. Assurance arguments that
are purely informal can be difficult to evaluate, and may be subject
to argumentation
fallacies <cit.>.  Consequently,
there have been a number of efforts to formalise and mechanise
assurance cases, both at the argumentation
level <cit.> and the evidence
level <cit.>.  More recently, in MDE, the
SACM[See
  <https://www.omg.org/spec/SACM/About-SACM/>.] is a standardised
meta-model that supports both structured argumentation and integration
of evidence from diverse system models <cit.>. SACM
unifies several existing argumentation notations, and also
provides support for artefact traceability and terminology.  It could,
in the future, serve as a crucial component for iFM in assurance.

Leading voices from applied software engineering research periodically
mention the role of FM as a key technology to master upcoming
challenges in assuring critical software
systems <cit.>.
A round table about the adoption of FM in IT
security <cit.>
positively evaluated their overall suitability, the combination of FM
with testing, and the achievements in FM automation.  The panellists
noticed limitations of FM in short-time-to-market projects and in
detecting unknown vulnerabilities as well as shortcomings in FM
training and adoption in practice.

However, even for mission-critical systems, high costs from late
defect removal and long defect repair
cycles <cit.>, as well as dangerous
and fatal[the fatal accident involving a Tesla advanced
  driving assistance system,
  <https://www.theguardian.com/technology/2018/jun/07/tesla-fatal-crash-silicon-valley-autopilot-mode-report>.]
incidents indicate that assurance in some areas is still driven by
practices failing to assist engineers in overcoming their challenges.
Moreover, , an observer
of a multitude of computing risks, stated that “the needs for better
safety, reliability, security, privacy, and system integrity that I
highlighted 24 years ago in my book, Computer-Related Risks, are still
with us in one form or another
today” <cit.>.

artificial intelligence software—particularly ML
components—has been developed at a high pace and used in many
non-critical applications.  Recently, ML components are increasingly
deployed in critical domains.  For verification and error removal,
such software has to be transparent and explainable.  Preferring
verifiable algorithms to heuristics,
<cit.> recalled the corresponding
engineering principle: “We cannot trust a device unless we know how
it works”.  One way to follow this principle and establish
transparency is to reverse engineer (to decode) the functionality
of an ML component even if this is not possible in
general <cit.>.
FM can help extract knowledge and reverse engineer abstractions
of ML systems to explain their behaviour.  We might then ask to
which extent the reverse engineered and verified functionality serves
as a substitute for the original ML component.

These anecdotes make it reasonable to question current assurance
practice.  Seen through the eyes of assurance, they suggest
that we might again be facing a dependable software engineering
crisis similar to the one from the late
1960s <cit.>.


  We as method researchers could learn from this crisis and improve
  the way that FM can be effectively coordinated to support
  early error removal in practical engineering processes.  We as
  practitioners could learn from this crisis and improve the way that
  we correctly engineer and certify highly automated systems such as
  RAS.




 §.§ The Desire to Learn From Accidents and Their Root
  Causes



In the title of <Ref>, the word “severe”
refers to the negative consequences potentially caused by
errors we want to remove using iFM.  The more severe the potential
consequences of an error, the more critical is its early removal.  The
usefulness of iFM thus positively correlates with their support in
the removal of critical errors.  However, the estimation of severity
often also requires the careful study of past field
incidents <cit.>.

We speak of field incidents to refer to significant operational
events in the field (the environment a technical system is
operated) which are undesired because of their safety risks and their
severe harmful consequences.  Field incidents range from minor
incidents to major accidents.  It is important to separate the
observed effect, the field incident, from its causes or, more
precisely, from the causal chains of events leading to the
observed effect.
Hence, this analysis depends on the considered system
perimeter <cit.>.
Depending on the possibilities of observation and the depth
pursued in a RCA, a conclusion on a possible cause can result in
any combination of, overall system failure, human error, adverse
environmental condition, design fault, hardware fault, software fault,
or specification error.[Specification errors are also called
  development failures <cit.> and
  can be seen as flaws in the process of requirements validation.]

There are many databases about field incidents: some are comprehensive
and include RCA, others are less detailed, and some are confidential,
depending on the regulations in the corresponding application domain
or industry sector.  Based on such databases, accident research,
insurance, and consumer institutions occasionally provide brief root
cause statistics along with accident
statistics.
[See <cit.>
  for a list of accident databases from such institutions.]

Accident statistics allow certain predictions of the safety of systems
and their operation, whether risk has been and will be acceptably
low.  Such statistics are also used in estimations of the amount of
field testing necessary[according to “As Low As
  Reasonably Practicable” or “So Far As Is Reasonably Practicable”.
  See <http://www.hse.gov.uk/risk/theory/alarpcheck.htm>:
  “Something is reasonably practicable unless its costs are grossly
  disproportionate to the benefits.”] 
to sufficiently reduce risk <cit.>.

it is well-acknowledged that inadequately designed and
implemented user interfaces are a significant contributory factor in
computer-related
accidents <cit.>.
But how and how fast have we arrived at this conclusion and how can we
prevent future such incidents?
Without proper empirical investigation of accident causes, such
statistics are of little use in decisions on measures for
  accident prevention <cit.>,
particularly on improvements of engineering processes, methods (iFM), and technologies (iFM tools) used to build these
systems.  For this, we require more in-depth, possibly formal,
RCA and statistics that relate error removal by iFM
  and incident root causes.  To this extent, RCA is a great
opportunity for the investigation of iFM effectiveness.

<cit.> reported about
deficiencies of information gathering (RCA) for databases on
computer-related accidents back in the early 1990s. 
He noted that independent, well-known, but confidential databases
might reduce under-reporting and were thus believed to improve safety
culture. 
Reporting has not much improved as observed by
<cit.>.
To understand the current RCA situation, we
studied 
a sample of 377 reports from open field incident databases (in
aviation, automotive, rail, energy, and others) finding the
following <cit.>:


  * RCA in these reports were of poor quality, either because they
  were not going deep enough, economically or technically infeasible, or
  inaccessible to us.

  * Particularly, root causes (software faults, specification
  errors) were rarely documented in a way that useful information about
  the technologies used (software) or consequences in the
  development process could be retrieved from the reports.

  * Reports in some sectors (aerospace, rail, power plants,
  process industry) contain more in-depth RCA than others (automotive)
  because of different regulations.

  * Some sectors operate official databases (NHTSA[National Highway Traffic Safety Administration,
    <https://www.nhtsa.gov>.] and NTSB[National
    Transportation Safety Board, <https://www.ntsb.gov>.] in the
  US transportation sector) and others do not (German road
  transportation sector).  

  * Our findings suggest that even in domains with regulated RCA,
  reports in open databases tend to be less informative than reports
  in closed databases.

  * The reports from the automotive industry exhibited a
  relatively small fraction of technology-related errors (software-related errors).

To validate our study and to better understand the context of our
findings, we interviewed eight[
  These experts have experience with tool qualification (1)
  and
  safety-critical systems in aviation (3), railway (1),
  automotive (4), and energy systems & turbines (1).  We have to keep
  their names confidential.] safety
experts <cit.>. 
One finding was that, because of an unclear separation of technologies
and a lack of explicit architectural knowledge, a desirable
classification of root causes is sometimes infeasible.  Hence,
accident analysts often close their reports with a level of detail too
low to draw helpful conclusions.  Additionally, one expert stated that
the hidden number of software-related or software-caused field
  incidents in dependable systems practice is likely much larger than
  the known number.  This matches our intuition but we are missing
clear evidence.

, a researcher involved in
the further development of IEC 61508, demands regulations to mandate
the use of systematic RCA.[From personal
  communication.]  In support of his view, we believe that rigorous
in-depth RCA based on iFM can be helpful to gain clarity
about actual root causes.
Again, beyond this undesirable form of late error removal, RCA data
is essential for the measurement of the effectiveness of
error removal techniques, particularly iFM.

The “Toyota unintended acceleration” incident exemplifies the
difficulty of drawing conclusions without using powerful RCA
techniques: a first RCA concluded that floor mats and sticky
throttle pedals caused a fatal car mishap.  A second RCA carried
out by NASA experts and based on testing and automated static
  analysis of the control system (software and hardware) was not
conclusive.  A third RCA[See expert interview by
  embedded software journalist from EE Times in 2013 on
  <https://www.eetimes.com/document.asp?doc_id=1319903   page_number=1>.]
based on code reviews—we could not find out which level of
formal inspection was used—detected defects in the control software
and safety architecture, demonstrated to be likely the causes of the
accident <cit.>.


  We could invest in iFM for RCA based on standardised data
  recording (aircraft black boxes), especially important for
  RAS where human operators cannot practically perform incident
  response.
  Based on lessons from formal RCA, we could further invest in the
  employment of integrated formal methods in RAS assurance and
  certification to prevent field incidents, major product recalls, and
  overly lengthy root cause investigations.




 §.§ The Desire of Assurance to Form a Mature Discipline



In his Turing Award acceptance speech in 1981, Tony
 reviewed type safety
precautions in programming languages and concluded: “In any
respectable branch of engineering, failure to observe such elementary
precautions would have long been against the
law” <cit.>.

Inspired by this comparison, it can be helpful to look at other
engineering disciplines such as civil, mechanical, or electrical
engineering to identify transfer opportunities for iFM.  There,
engineers use FM in many of their critical tasks.  However,
nowadays these methods are often hidden behind powerful software tools
usable by qualified professional engineers.  Although type systems,
run-time bounds checking, and other variants of assertion checking
have been frequently used in dependable systems practice, the overall
level of FM adoption is still comparatively low.

even in less critical mechanical engineering domains,
vocationally trained engineers use computer-aided engineering, design,
and manufacturing software.  Whether for designing machine parts for
serial production (specification) or for calculations (dimensioning, force or material flow simulations) for these parts and
their assembly (for prototype verification), these engineers use
tools based on canonical mathematical models.

Nowadays, drawings from computer-aided mechanical design carry at
least two types of semantics: one declarative based on calculus for
dimensioning (1), and one procedural for the synthesis of
Computer-Numerical-Control programs for production machines processing
materials to realise the drawings (2).  Note that the unifying base of
these two semantics is geometry, a well-studied mathematical
discipline.
Although higher levels of complexity demand more sophisticated
analytical expertise, typically from engineers with several years of
work experience, many tasks can be accomplished by less trained
engineers using the corresponding tools.

Whereas in computer-aided mechanical design both semantics seem to be
used to a similar extent, in DA we observe that analogous semantics
are rarely used even if tools are available, and less often we see (1)
and (2) being consistently used.
Low adoption might result from the semantics for dimensioning and
production automation being usually less abstract than the semantics
for verification (1) and synthesis (2) of computer programs.
Accordingly, Parnas suggests a shift from correctness proof to
property calculation to develop practical formal
methods <cit.>.

Patterns have had a long history in many disciplines.
In mechanical engineering, patterns are better known as machine
  elements and are particularly useful in high-reliability
applications.  Machine elements (and standardised forms thereof) have
a stabilising impact on the outcome of an engineering project.  The
process of element selection and composition can take tremendous
advantage not only from the reuse of proven design knowledge
but also from the reuse of complex calculations (from gear
transmissions, injection moulding tools, skeleton framings).
Moreover, modern tools typically foster the use of element
  libraries and parametric design.  Importantly, because the
properties of such elements are in many cases well known, calculations
for assemblies (compositional verification) get relatively
easy. However, the higher the required precision of these calculations,
the more expensive is their computation.

These observations are in line with what we know from collaborations
in robotics, like mechatronics, a discipline where many
engineering domains have to play together well:  FM are
heavily used for the analysis of robot controllers and for various
kinds of simulations and tests <cit.>.

Digital circuit engineering is a domain where FM such as model
checking have been successfully applied decades ago.  However,
systematic hardware errors, such as Spectre and Meltdown, and the
unavailability of temporal specifications of optimised
operations (branch-prediction and speculative execution)
discontinue the verifiability of recent computer architectures.  This
lack of verifiability of the assumptions (partitioning,
information flow) about the execution platform complicates the
verifiability of the software (an operating system) running on
such a platform.[See blog post on the seL4 microkernel,
  <https://research.csiro.au/tsblog/crisis-security-vs-performance/>.]


  Dependability assurance has not yet successfully adopted iFM
  as a vital part of their key methodologies.  If FM seem
  relatively well established in other disciplines, we might also be
  able to successfully transfer iFM to RAS assurance and 
  assurance in other domains.
  Beyond software design patterns, we could benefit from best
  practices in formal specification and development manifested in
  repositories of FM patterns.
  Moreover, we could aim at the further unification of established
  FM to provide common formal semantics for various domains.




 §.§ The Desire for Adequate and Dependable Norms



Dependable systems practice usually includes the transition from what
is called the system specification to an artefact called
system design.  Typically, software and hardware
  specifications are then derived from these two artefacts before
delving into detailed technology choice and development.
<cit.> observe that
safety culture in such a framework is more important than strict
standards, but adequate standards and certification regimes can
establish and strengthen the safety culture desirable in dependable
systems practice.

A striking finding in one of our recent discussions
of dependable systems standards (IEC 61508,
ISO 26262,[For: Road Vehicles – Functional Safety.] DO-178C)
is that normative parts for specification (RE), for
specification validation (avoiding and handling requirements
errors), and for hazard and risk analysis (particularly in
early process stages) seem to be below the state of the
  art <cit.>,
despite several observations that significant portions <cit.> of the causes of safety-critical
software-related incidents fall into the category of
specification
  errors <cit.>.

If one identifies an error in the software specification, do causes of
this error originate from an erroneous system specification?  How are
system, software, and hardware specifications (formally) related?
Control software typically governs the behaviour of a whole machine.
Hence, core components of a software specification might, modulo an
input/output relation <cit.>, very well govern
the narrative of the overall system specification.  Inspired by the
issue of specification validity as highlighted in
<cit.>, do these standards provide
guidance for checking the validity and consistency of core parts of
system, software, and hardware specifications?

The literature provides plenty of evidence of undesired impacts of
specification errors dating back as early as the investigations of
<cit.> and <cit.>.  As reported by
<cit.>, the 92% of
computer-related field incidents caused by human-computer interaction
also illustrate the gap between specifications and capabilities of
humans to interact with automation.  Despite these older figures, we
are talking of one of the most critical parts of standards.
Practitioners could expect to receive strong guidance from these
parts.  Moreover, the requirements to show conformance to these parts
should not be vacuous.

Many standards define specific sets of requirements (for
error removal and fault-tolerance) depending on the level of risk a
system (or any part of it) might cause.  The higher this level,
the more demanding these requirements.  Examples of demanding
requirements include SIL 3-4 (IEC 61508),
ASIL C-D (ISO 26262), SC 3-4 (IEC 61508),
DAL A-B (DO-178C).  Even for the highest such levels the
mentioned standards only “highly recommend” but not mandate the use
of FM.

Guidelines for embedded software development such as
MISRA:1994 <cit.>
recommend FM for SIL 4, although MISRA:2004 no
longer includes such information and instead refers back[This
  might also the case for MISRA:2012 from March 2013.  We are unaware
  of the opposite but were also unable to receive a copy of this
  version.] to MISRA:1994.  As already mentioned, ISO 26262 as the
overriding standard does not go beyond high recommendation of FM
for ASIL D.  <cit.> reported in 2014
that, in the US, car manufacturers are not required to follow 
MISRA and that there are no other software certification
requirements.  This currently also applies to autonomous road vehicles.

In an interesting anecdote, 
reported on his lack of success in introducing systematic hazard (and
risk) analysis methodology into normative parts of this
standard <cit.>.  Moreover, he
mentioned unsuccessful attempts to strengthen the role
of FM in IEC 61508 and on the “broken standardisation” in
assurance practice.  In reaction to that, he proposed the use of
evidently independent peer reviews to “dampen committee-capture by
big-company bully players”.See System Safety Mailing
  List message from 4/11/2018,
  <http://www.systemsafetylist.org/4183.htm>
  and <cit.>.

Additionally, <cit.> observed: “There
is an expectation by the community that standards will embody the best
available technology and that their presentation will allow
determination of conformance to be fairly straightforward.  A
criticism that is seldom heard is that some standards are, in fact,
technically flawed and poorly presented.”  He exemplifies his
critique by several issues with IEC 61508 and RTCA DO-178B and
suggests to make the meaning of “conformance [or compliance] with a
standard” more rigorous.  Particularly, he encourages to replace
indirect (process-related) evidence (documentation of
specification activities) in assurance cases by direct (artefact-related) evidence (unsuccessful checks for presence of
certain specification faults, successful checks for absence of
implementation errors).[While formal verification serves the
  check of absence of property violations, conventional testing can
  only serve as a check of presence of such violations.]  With the
observation in software quality control that “there is little
evidence that conformance to process standards guarantees good
products”, <cit.> delivered a
reasonable basis for 's
suggestions.

Regarding the integration of dependability approaches and FM,
<cit.> had stated by 1993 that they
“do not know how to combine formal methods assurance with metrics
collected from other techniques such as fault-tolerance”.  Is this
still an issue?  From a practical viewpoint, standards such as, IEC 61508, ISO 26262, and DO-178C, provide recommendations about
techniques for the reduction of both random hardware failures (by
fault-tolerance techniques) and systematic hardware and software
failures (by FM, static analysis, and testing).  If
iFM can support the combined application of the recommended
techniques and achieve an improvement in practice then we should
really strive to demonstrate this.

We believe that critical fractions of strong direct evidence can be
delivered through the use of FM.  In support of
's
argument <cit.>, we see a great opportunity
for an assessment of how the corresponding guidelines in these
standards can be extended and aligned with recent results in FM
research.


  We as researchers and practitioners could support the creation of
  adequate state-of-the-art regulations with improved guidance on
  specification construction and validation.  That way, we could
  foster well-certified high-risk software in a time where dangerous
  autonomous machines are about to get widely deployed in our society.




§ THREATS TO THE ADOPTION OF INTEGRATED FORMAL METHODS




This section closes the environmental part of our SWOT
analysis by identifying threats to FM transfer as well as
challenges that arise from alternative or competing approaches taking
the opportunities mentioned in <Ref>.  We also
outline remedies to these threats.

The development of effective iFM and their successful transfer into
practice can be impeded by 


  * a lack of agreement on a sound semantic base for domain-specific
  and cross-domain FM
  integration (<Ref>),

  * missing support for widely used and established
  tools (<Ref>),

  * a lack of interest in practical problems on the side of FM
  researchers (<Ref>),

  * a lack of incentives for FM researchers to engage with current
  practice and for software practitioners to engage with recent
  theoretical results (<Ref>),

  * a bad reputation among practitioners and applied
  researchers (<Ref>),

  * proofs that are faulty or do not
  scale (<Ref>),

  * the quest for soundness overriding the quest for
  usefulness (<Ref>).

We discuss these threats and barriers in more detail in the following.



 §.§ Difficulties and Misconceptions of Unification



According to <cit.>, the
successes and failures of semi-formal languages (UML, SysML)
suggest that FM, once wrapped in FM-based tools, get exposed to the
quest for a unified syntax, one main objective of the UML
movement in the 1990s.  Rather than a unified syntax, it is more
desirable to have a unified semantics and several well-defined
mappings to domain-specific syntax wherever
convenient (<Ref>).  This approach is
occasionally taken up by DSL in MDE (<Ref>).
<cit.> argued that one cannot achieve proper integration of
methods and notations without a unifying semantics.  This argument
carries over to the problem of tool integration as already discussed
in <Ref> and revisited below.
Particularly, the following challenges apply to FM when used in MDE:


  * the maintenance of a single source of information serving in
  the (automated) derivation of downstream artefacts (proof
  results, code via
  synthesis) <cit.>, 

  * a clear mapping between the DSL presented to the
  engineer (using intuitive notation) and the DSL semantics serving as
  the basis of formal verification,

  * the embedding of a lean domain-specific formalism into a
  common data model <cit.> suitable
  for access and manipulation by engineers through their
  various
  tools <cit.>.

These challenges are complicated by irreducible unidirectionalities
in automated transformations (model-to-code) limiting the
desirable round-trip engineering <cit.> (the change
between views of the same data).

We discussed SACM <cit.> as an assurance DSL in
<Ref>.
Likewise, architecture description languages (the
Architecture Analysis & Design Language
<cit.>, EAST-ADL
<cit.>) are DSL for overall embedded
system design.
DSL can be seen as one shortcut to the still ongoing efforts of
arriving at a reduced version or a variant of UML where a
semantics can be defined for the whole
language <cit.>.

At a higher level of abstraction, so-called architecture
  frameworks (ISO 42010, 
the Department of Defense Architecture Framework)
and artefact and traceability
  models <cit.>
have been proposed, aiming at the standardisation of specific parts of
the systems and software engineering life-cycle and of the
documentation and data models used there.
These frameworks and models are similar to the models used in product
data/life-cycle management in fields like mechanical or civil
engineering.

To our best knowledge, no cross-disciplinary semantic unification has
been undertaken yet (see <Ref>), serving as a
basis for dependable systems engineering.  Although many of these
approaches have not been developed with the aim of formalisation and
the unification of semantics, we believe that this effort has to be
made when developing powerful iFM.


  The main threat is the lack of agreement on a sound semantic base
  for domain-specific and cross-domain iFM.



  To reduce this threat, FM integration and refinement-based
  software engineering could be better aligned with artefact
  models <cit.>.  This alignment may
  foster the unification of formal semantics to strengthen
  traceability among the artefacts and to aid in a variety of change
  impact analysis tasks in the engineering
  process <cit.>.




 §.§ Reluctant Integration Culture and Legacy Processes



Tool integration is about the integration of engineering IT,
tools for requirements specification, computer-aided software
engineering, and computer-aided mechanical design.  Among the wide variety
of solutions to capture and track model data, the majority deals with
linking or merging data
models <cit.> in
one or another shallow way (software repositories, data exchange
formats, product/engineering/application data or life-cycle management
systems).

Some tools with sustainable support are heavyweight, making it
difficult to agree on lean model semantics, while others are
proprietary, accompanied with interest in hiding model semantics.  The
surveys of <cit.>,
<cit.>, and
<cit.> confirm that method and model
integration have not yet been solved in MBD, MDE, and dependable
systems practice.
Moreover, frequent proposals by
researchers <cit.>
to formalise fragments or variants of UML and SysML
have not yet received wide attention by
practitioners and standardisation authorities.

DSL-based integrated development environments (using Xtext
and Sirius) get close to what is suitable for FM-based tools.
Such tools rely on a trusted representation of the formal semantics
integrating the model data.  For successful iFM transfer to
assurance practice, tools need to be built on a lean and open central
system model <cit.>.

An even greater barrier than loosely integrated tools are legacy
language and modelling paradigms, an established tool and
  method market carried by legacy stakeholders and, possibly,
a neglected continuous improvement of FM education and
  training.


  The main threat is discontinuous and disintegrated FM
  education, transfer, and tool development.  



  To reduce this threat, continuous adaptation and improvement of
  education through teaching, of transfer through training,
  application, and feedback, and of tool development through regulated
  interface standards are necessary.




 §.§ Reluctant Transfer Culture and Exaggerated Scepticism



Finally, the vision of introducing iFM into assurance practice
might be hindered by a lack of FM researchers able or willing to
engage with industrial assurance practice, as diagnosed
by <cit.>.  It is certainly hard work to collect
sufficient evidence for FM effectiveness in assurance practice
because of intellectual property rights and other legal issues but
also because of a lack of awareness among FM
researchers <cit.>.  However, for credible method comparison experiments,
<cit.> recommended a sample of 20
similar projects split into two groups, 10 projects without
treatment (not using FM) and 10 projects with
treatment (using FM) to establish strong evidence (evidence of level 5 or above <cit.>).


Exaggerated scepticism on the side of practitioners and applied
researchers that has piled up over the years might be the
most important barrier to cross.  Early failures to meet high
expectations on FM and FM transfer might have led to what
can be called an “FM Winter”.  However, we think crossing a few
other barriers first might make it easier to cope with scepticism in
the assurance community and initiate an “FM Spring”, at least in
assurance practice.  The recent successes with FM
for certification of commercial medical
devices <cit.>,
and the associated burgeoning field of FM for
HCI <cit.>, are examples that could help to
overcome this scepticism. Moreover, their is potential for transfer of
these results to RAS engineering, where the need for safety
assured HCI is also
paramount <cit.>.


  The main threat is the reluctance of FM researchers to
  regularly engage in transfer efforts combined with an exaggerated
  scepticism of practitioners and with other mechanisms (lack of
  funding, poorly focused research evaluation, intellectual property
  rights) preventing both sides from engaging in an effective
  bidirectional transfer.  



  To reduce this threat, building awareness
  among researchers as well as stronger incentives (regulation)
  to provide continuous transfer funding for FM research (not relying on short-term projects like PhD theses) is needed.  A
  good start on the academic side could then be a specific
  standardised repository of FM case studies.




 §.§ Too Many Errors in Proofs and Failure to Scale



From the perspective of measurement,
<cit.> stated that
“proofs of correctness sound useful, but [i] errors in the proofs
themselves seem to be common failings not covered by the literature.
Further, large applications may have thousands of provable algorithms,
and [ii] the time required to prove them all might take many years”.
For [i], the authors opposed 7% of erroneous bug repairs to up to
100% of erroneous proofs, though stating that the latter was based on
an anecdote and there had been little data around.
 elaborated an example for
[ii]: Assuming one provable algorithm per 5 function points[A
  function point is a measure of the conceptual complexity of an IT
  system relevant for the estimation of the amount of work required to
  engineer this system.]  and on average 4 proofs per
day, 
Microsoft Windows 7 (160,000 function points) would have about 32,000
provable algorithms, taking a qualified software engineer about 36
calendar years.  They highlighted that typically only around 5% of the
personnel are trained to do this work, assuming that algorithms and
requirements are stable during proof time.

's argument is based on
the view of practical program verification as a largely manual
activity.  However, research in reasoning about programs has devised
promising approaches to proof automation (bounded model checkers,
interactive proof assistants).  Assessing such approaches,
<cit.> compared rigorous but
manual formal proof with mechanised or automated proof.
He could not find a case where mechanised proof threw doubt upon an
established mathematical theorem.
 observed that
this underpins the robustness argument of
<cit.> for proofs as manual social
processes rather than lengthy mechanical
derivations (<Ref>).
However, opposing 's view,
<cit.> concluded that
structuring of knowledge about computing ideas is the actual issue,
and not the avoidance of mechanisation.  Furthermore,
<cit.> mitigated
's issue of the reality
gap in program verification <cit.>
by referring to researchers' continuous efforts in verifying hardware,
programming languages, and compilers in addition to individual
programs.  Finally, in support of
's concerns,
<cit.> highlighted the validity
of specifications, manual and automated proofs rely on, as a
serious issue indeed having received too little
attention from researchers (<Ref>).


  The main threat is the lack of qualified personnel to cope with the
  required amount and type of proof.  



  We believe, one angle of attacking this threat is the use of proof
  assistants well-integrated with common environments for
  requirements specification and software development combined with
  continuous research and education in the corresponding methods and
  tools.




 §.§ Failure to Derive Useful Tools



Being loosely related to erroneous proofs, the information
  overload through false-positive findings of errors is a well-known
problem in static program analysis.  Semi-formal pattern
checkers,[Also called bug finding tools.]
such as PMD and FindBugs, are exposed to this
threat <cit.>.  Additionally,
FM-based verification tools, such as Terminator and
ESC/Java <cit.>,
can be unable to correctly report all potential problems, because they
are bounded and therefore unsound.  While such tools can be helpful,
confronting developers with many irrelevant findings (false
positives) or a high risk of critical misses (false negatives)
can lead to decreased use of FM-based tools.

<Ref> relates the two information retrieval
metrics, precision and recall, with two adequacy
criteria of proof calculi, soundness and completeness.
Precision denotes the ratio of actual (solid circle) to correct (true
positive findings in the hashed area) findings, while recall measures
the ratio of correct to all theoretically correct (dotted circle)
findings.  The ideal value for both metrics is 1, meaning that there
are only true negatives and true positives.  Completeness, although
unachievable for richer theories, would correspond to recall and
soundness would correspond to a precision of 1.

On the one hand, the usefulness of the calculi underlying FM is
directly proportional only to their completeness and (traditionally)
expires with a precision of less than 1.  In other words, we usually
try to avoid calculi that allow the derivation of false theorems.  On
the other hand, semi-formal pattern checkers have shown to have a
wide, sometimes unacceptable, range of precision and recall of their
findings.  The usefulness of practical FM-based tools might lie
somewhere in the middle between classical calculi and bug finding
tools with poor precision/recall values.


  The main threat is the struggle of academia and tool vendors to
  provide adequate tools, suited to adapt to novel scientific
  insights, to be integrated with other tools, and to be maintained in
  a flexible and independent manner.  



  To reduce this threat, an improvement of education and strong
  incentives can play an important role
  here (<Ref>).








§ A VISION OF INTEGRATED FORMAL METHODS FOR ASSURANCE



The following discussion applies to many domains of dependability
assurance.  However, the complexity of robots and autonomous systems
forms a key opportunity for the progress of iFM research and for
its successful transfer.  Accordingly, <Ref>
summarises the discussion in
<Ref> with an
interpretation into RAS assurance practice.  Based on the strengths
and opportunities described in the
<Ref>, we formulate our
vision in terms of working hypotheses:



  * From <Ref>: Software tools for
  the construction of arguments and production of evidence using
  iFM can meet the challenge of assuring RAS
  safe.  Computer-assisted assurance cases supported by heterogeneous
  formal models will increase confidence in their sufficiency,
  and also aid in maintenance and evolution through
  modularisation of arguments and evidence.

  * From <Ref>: iFM, in
  particular modern verification tools, will enable automation
    of the evidence gathering process, and highlight potential
  problems when an assurance case changes or when an incident occurs.


  * From <Ref>:
  There is no stable path to assured autonomy without
    the use of iFM.  Acceptable safety will be much more likely
  achieved with iFM than without them.

  * From <Ref>: The success of
  iFM depends on the ability to integrate a variety of FM for
  different aspects of RAS (HCI,
  safety-security interaction, missing human fallback,
  environment/world modelling, uncertain prediction/behaviour), which
  is not currently possible.

  * From <Ref>:
  Sophisticated techniques for model integration and
    synchronisation are necessary to support MDE with iFM.  This
  way, iFM will make it easier to express consistent RAS models
  covering all relevant aspects, make their modelling assumptions
  explicit, and improve future assurance practices.


  * From
  <Ref>:
  iFM can be beneficial in the short term.  However, an important
  engineering principle is to be
  conservative <cit.> and,
  therefore, not to change procedures unless there is compelling
  evidence that iFM are effective.  Such evidence can be delivered
  through empirical
    research <cit.> 
  and collaboration of academia and industry.  That evidence
  is required to re-evaluate research and foster research
    progress and transfer.

  * 
  From <Ref>: The demonstration of cost
  effectiveness in addition to technical effectiveness of new
  iFM is necessary to justify further research.

  * From <Ref>: Norms are a lever of
  public interest in dependability <cit.>.
  Current norms seem to deviate from the state of the art and may fail
  to guarantee product certification procedures that satisfy the
  public interest.


<Ref> assigns these hypotheses to the relationships
between foundational and transfer-directed iFM research by
example of the RAS domain.  Overall, we believe that iFM
have great potential and can improve assurance but practitioners do
not use them accordingly.


  We could take and enhance credible measures to convince assurance
  practitioners of our results and effectively transfer these results.
  For this to happen, we have to answer further research questions.






§ EMPIRICAL, APPLIED, AND FOUNDATIONAL RESEARCH



Based on the aforementioned working hypotheses, we state several
objectives for foundational and transfer-directed iFM research,
formulate research questions, and show our expectations on desirable
outcomes of such research.



 §.§ Research Objectives and Tasks



To validate and transfer our research results, we need to


  * evaluate how assurance case construction and management for
  certifiable RAS can be improved by
  iFM <cit.>.

  * debunk or justify arguments against the use of FM or FM-based
  tools in RAS assurance.

  * foster a culture of successful FM research transfer to
  industries performing RAS assurance.

Taking an iFM foundational point of view, we need


  * foundational research on the integration and unification of FM to
  tackle the complexity of RAS <cit.>.

  * a unified semantic foundation for the plethora of notations in
  RAS assurance, to enable method and tool integration.  There
  are a number of promising research directions still being
  investigated <cit.>.

Taking an evidence-based point of view, as already highlighted in 1993
by <cit.>, we need to


  * understand the difference between the state of assurance
  practice and assurance research.

  * understand in which ways current RAS assurance practices fail,
  and suggest effective approaches from assurance research.
  In this way, we can be sure that assurance practice is equipped with
  state-of-the-art assurance technology for defence against potential
  liability claims, and that assurance practitioners do not fail in
  fulfilling their obligations.

  * understand how results from assurance research can be validated
  to be sure that research follows promising directions with high
  potential of success in assurance practice.

Based on that, we need to 


  * set concrete directions for empirical FM research in RAS
  assurance.

  * train FM researchers in applying empirical research designs in
  their work on rigorous assurance cases.
  <cit.> corroborated this objective by
  saying that “formal methods champions need to be aware of the need
  to measure costs”.

  * avoid biases as found in various branches of scientific
  research.  in the social and biomedical sciences, researchers
  identified such biases through meta-analyses and suggested
  measures for bias
  avoidance <cit.>.

  * increase the level of evidence of FM research to level 2
  according to the hierarchy
  in <cit.>.

  * avoid knowledge gaps about whether (a) RAS practice is keeping
  up with the state of the assurance art, and (b) whether recent academic
  or industrial research is going in the right direction.
  In this way, we can be sure that we do our best to inform and
  serve the society.

Using appropriate research designs, we need to


  * invite the RAS industry to enhance their efforts in engaging
  with recent iFM research.

  * foster goal-oriented interaction (a) between assurance
  practitioners and researchers and (b) between FM researchers 
  and assurance researchers.
  In this way, we can be sure to do everything to keep researchers up
  to date with respect to practical demands.

  * join the FM research and applied assurance research
  communities (<Ref> on
  page fig:refinedapproach), both vital for the progress and
  transfer of assurance research into RAS assurance practice.
  This way, we can be sure to foster necessary knowledge transfer
  between these two communities.

  * summarise achievements in practical applications of iFM
  for constructing assurance cases.

  * suggest improvements of curricula for RAS assurance.

  * guide the RAS industry in process improvement, training,
  and tool support.

  * guide vendors of FM-based assurance tools to assess and improve
  their tools and services.




 §.§ Some Research Questions addressing these Objectives



The research questions below are relevant for FM in general.  We
consider these questions as crucial to be answered for RAS assurance
to address the aforementioned objectives:


  * What is the true extent of computer-related accidents up to
  2019 <cit.>?  What would
  these figures mean for the RAS domain?

  * Does the use of formalism detect severe errors to a larger
  extent than without the
  use of formalism <cit.>? 

  * Does the use of formalism detect severe errors earlier than
  without using formalism? 

  * Why would such errors be a compelling argument for the use of
  FM? 

  * Apart from error avoidance and removal, which other benefits of
  iFM in practice are evident and can be utilised for method
  trade-offs?

  * Which criteria play a central role in measuring iFM
  effectiveness?  Particularly, how can FM-based tools be used at
  scale?

  * How would Commercial-off-the-Shelf and
  System-Element-out-of-Context verification by iFM pay off?

  * Which hurdles need to be overcome to use iFM in practice
  to the maximum benefit?

  * How do we know when these hurdles are actually overcome?

  * How can FM (from different disciplines) be used
  together (iFM, unification)?

  * How can FM be used to assure systems (computer vision
  in road vehicles) involving AI techniques like
  machine learning and deep neural networks?

  * How can FM be integrated into assurance cases to support
  certification against international safety and security standards?

  * How can we best combine formal and informal methods?  how
  can we deal with the issue of the validity of specifications that
  proofs rely on <cit.>.

  * How can we best present formal requirements, evidence, and artefacts in an
  assurance case?

  * How can empirical research help in successfully demonstrating
  the capabilities of iFM for rigorous and certifiable autonomy
  assurance?

This list of research questions can easily be extended by further more
detailed empirical questions from the settings discussed in 
<cit.>.



 §.§ Some Envisaged Research Outcomes



Our vision of rigorous RAS assurance implies foundational iFM
research to result in


  * novel semantic frameworks unifying best practice methods,
  models, and formalisms established in RAS

  * new concepts for iFM-based development environments

  * new computational theories to support formal modelling and
  verification of RAS

  * evaluations of
  
  
  * assurance tools, languages, frameworks, or platforms used in
    practice regarding their support of iFM
  
  * the integration of iFM into modelling and programming
    techniques, assurance methods, and assurance processes
  
  * languages for linking informal requirements with evidence from
    iFM
  
  * (automated) abstraction techniques used in assurance and
    certification
  

  * opinions, positions, and visions on FM integration and
  unification for rigorous practical assurance.

Our vision of rigorous RAS assurance implies applied and
empirical iFM research to result in


  * comparisons of
  
  
  * projects applying iFM in assurance practice with similar practical
    projects applying non-iFM approaches
  
  * iFM-based (embedded software) assurance with assurance
    approaches in traditional engineering disciplines
  


  * checklists, metrics, and benchmarks (for and beyond tool performance)
  for
  
  
  * the evaluation and comparison of iFM-based assurance
    approaches (confidence level)
  
  * relating error removal and incident root cause data (efficiency and effectiveness in removal of severe errors or in
    avoidance of severe accidents,
    <cit.>)
  
  * usability and maturity assessment of iFM (abstraction
    effort, proof complexity, assurance case complexity, productivity)
  
  * the evaluation of FM budget
    cases (<cit.> in electronic
    hardware development).
  


  * experiences in or surveys (systematic mappings and reviews
  of assurance case research, interview studies with assurance
  practitioners, <Ref>) of
  
  
  * iFM transfers and applications (case studies in assurance
    and certification projects)
  
  * challenges, limitations/barriers, and benefits of
    iFM in assurance and certification projects,
  
  

  * research designs (for controlled field experiments) for the
  practical validation of iFM in assurance and certification projects


  * opinions, positions, and visions on future research, education,
  and training in the use of iFM in assurance and certification.




§ SUMMARY



Along the lines of <cit.>, we
analysed strengths, weaknesses, opportunities, and threats to
determine the potential of integrated formal methods to improve the
practice of dependability assurance.  Emphasising robots and
autonomous systems as an area in the spotlight of dependability
assurance, we express our expectations of research progress and
transfer.  From these expectations, we derived a research and research
transfer agenda with the objective of
[(i)]

  * enhancing the foundations of integrated formal methods,

  * collecting evidence on the effectiveness of integrated formal
  methods in practice,

  * successfully transferring integrated formal methods into the
  assurance practice, with a short-term focus on robots and autonomous
  systems, and

  * fostering research progress, education, and training from the
  results of this transfer effort.


 



  
Acknowledgements

This work is partly supported by the Deutsche
Forschungsgemeinschaft (DFG) under the Grant no. 381212925 and the
EPSRC projects CyPhyAssure,[CyPhyAssure Project:
  <https://www.cs.york.ac.uk/circus/CyPhyAssure/>.] grant
reference EP/S001190/1, and RoboCalc, grant reference EP/M025756/1.
We are deeply grateful to Michael Butler, Ana Cavalcanti, John
Fitzgerald, Cliff Jones, and Peter Gorm Larsen for helpful feedback
on previous versions of this manuscript and for their genuine
support in shaping the direction of this work.

 





§ 



§ STUDYING FORMAL METHOD PRACTITIONERS: A BALLPARK FIGURE



In this section, we make a brief excursion to the relationship between
FM and FI, closing with a rough estimate of the size of the
population of FM users and the meaning of such an estimate for
the empirical study of that population.  Such studies include
cross-sectional and longitudinal surveys based on questionnaires or
semi-structured interviews.



  
Formal Inspection versus Formal Methods

FI encompasses a variety of techniques (peer reviews,
walk-throughs) where critical process artefacts (program code)
are checked (manually or using software tools) against a variety
of criteria (checklists), usually by a group of independent
qualified engineers.  For the sake of simplicity of the following
discussion, we assume that FM can be seen as a particularly
rigorous variant of FI where formal specifications serve as a
particular way of formulating checklists.

We compare the use of FM with the use of FI.  According to
<cit.>, formal
inspections are used in more than 35% of commercial defence, systems,
and embedded software projects, and FM are estimated to be applied in
less than 1% of overall commercial software engineering projects.  To
get an idea of this coverage data, we perform an analysis of the
global embedded software market based on other global software market
indicators in <Ref>.  We found estimates of systems and
software professionals world-wide and estimates of annual US business
values.
[See <https://en.wikipedia.org/wiki/Software_industry>
  and
  <https://softwareengineering.stackexchange.com/questions/18959/what-proportion-of-programming-is-done-for-embedded-systems>.]

A uniform distribution would entail roughly 37000 USD/year per person
in the general software domain and 10000 USD/year per person in the embedded
software domain.  Clearly, geographically strongly differing salaries and
part-time engagement rule out a uniform distribution, yet providing
figures helpful for our purposes.

Next, we apply the following proportions: From a worldwide population
of around 18.5 million software developers in
2014 <cit.>, about 19% live in the US, 10% in China,
9.8% in India, 36% Asia/Pacific region, 39 % live in Europe, the
Middle East, and Africa; and 30% in the Americas.
[See
  <https://adtmag.com/Blogs/WatersWorks/2014/01/Worldwide-Developer-Count.aspx>.]
The design to quality assurance (verification and test)
cost ratio is observed to be approximately 30:70.
[See <https://www.slideshare.net/pboulet/socdesign>.]
About 20% of embedded software personnel are quality assurance
engineers (test, verification, or validation engineers).
[See
  <https://de.slideshare.net/vdcresearch/searching-for-the-total-size-of-the-embedded-software-engineering-market>.]



The estimates in <Ref> suggest that around 2% of the
overall pure software market are allocated to the embedded pure software
market.  35% coverage of formal inspection in about 13.5% of the
overall software market (161/(689+515) = 0.134) would result in
roughly 4.7% coverage of all software projects by formal inspection
versus at most 1% coverage by FM.  However, from this data we can
hardly know whether rates of FM use get close to or beyond 10% in
high-criticality systems projects.

Assuming that in about 35% of embedded software projects the quality
assurance personnel would use formal inspection and that in every
fifth (1:4.7) of such projects formal methods would be used, the
current population of regular practical FM users would globally amount
to about 5040 (= 72,000 * 0.34 * 0.20) persons.  Note that these
numbers are rough estimates.  However, we believe their order of
magnitude is realistic.  Given that these persons would on
average earn about 100,000 USD/year each, we would speak of an annual
business value of around USD 504 million.



  
Empirical Studies of FI and FM Practitioners

Importantly, from these data we can determine minimum sample sizes for
surveys.  assume we want to have 95% confidence in our test
results and are fine with a confidence interval of ±7%.  Then,
for regular practical FM users, a population of the size
of 5040 persons would require us to sample 189 independent data
points (questionnaire responses).  The population of
regular practical FI users, 25200 (=72,000*.35) would
imply a minimum sample size of 194.

For any sample of such size, any survey has to argue why the sample
represents the population.  This step depends on the
possibilities given during the sampling stage.  Obviously, reaching
out to 189 out of 5040 persons whose locations might be largely
unknown is an extremely difficult task that might only be tackled in
terms of a global group effort among researchers and practitioners.
Given that this challenge can be tackled, these figures determine the
type of surveys required for the collection of confident evidence.
Moreover, these figures limit the manual effort to perform and repeat
valuable qualitative studies to a reasonable amount.



§ FORMAL METHODS IN DEPENDABLE SYSTEMS ENGINEERING



<Ref> on page fig:refinedapproach
depicts our research setting for this survey.  There, we describe
iFM as an enhancement of FM and the assurance of
RAS as a special field of dependable systems engineering.
Because many of the discussed issues are of a more general nature, we
first prepared a SWOT analysis of FM in dependable systems
engineering in <Ref>.  Then, we refined this
analysis in <Ref> to accommodate specifics of
iFM for RAS.



 