No.121 Towards industrial application of advanced formal methods for cyber-physical system engineering

NII Shonan Meeting:

Shonan Village Center, November 5-8, 2018

Organizers

  • Fuyuki Ishikawa,  National Institute of Informatics,  Japan
  • Alexander Romanovsky,  Newcastle University,  UK
  • Thierry Lecomte,  ClearSy,  France

Overview

Description of the meeting

Software systems plays an increasingly critical role in the society, as well as in the real
world, as being further investigated in the emerging paradigms such as Cyber-Physical
Systems (CPS), Internet of Things (IoT), and Smart City/Office/Home. The demand for
dependability is very strong in such systems, while the difficulties in its assurance is
increasing more than ever, for example, due to the unprecedented complexity of the
systems and their environments. Creation of the theoretical foundations – specifically
based on mathematics – are instrumental for tackling the difficulties when they are
elaborated into systematic methods with engineering disciplines, i.e., formal methods.

At the same time, there have been serious discussions on how formal methods should be
or can be introduced and leveraged in the industry [1]. Myths are often cited,
representing typical kinds of “misunderstanding” such as necessity for extreme
mathematical skills [2-4]. Such perceptions, true or false, can create a sense of doubt,
distance, or even antipathy against formal methods. Even if engineers appreciate values
of formal methods, there are obstacles in their effective and efficient applications.
Typical obstacles include the initial costs of investment and education, the difficulties in
tailoring a method for the target projects, and difficulties in convincing the stakeholders
(including, the managers) in terms of various aspects such as cost-efficiency. It is worth
noting that the discussion of these issues is not limited to a specific world of formal
methods – which often provides useful exemplification of very general issues, including:
what are knowledge and skills necessary in software engineering, how technology from
the academia can be perceived and (un)accepted by the industry, and so on.

Today we have further drivers that motivate an active discussion of these issues. First,
the increasing difficulties of the emergent systems are making it necessary to rethink the
existing approaches to dependability assurance, including formal methods. Second, the
recent technical advances are changing feasibility and usages of formal methods, e.g.,
enhancement of SAT/SMT solvers, as well as the infrastructure (GPU, clouds, etc.).
Finally, most importantly, the industry has recently been achieving clear successes in
the advanced use of formal methods. ClearSy showed the feasibility of
correct-by-construction approach (obtaining the already-verified code) in their
worldwide business [5]. Amazon showed how formal methods spread from one team to
various teams [6]. Facebook embedded a formal verification tool into its agile culture
[7]. Sony FeliCa established use of formal specification as readable documents [8].
Similar examples can be found by ARM, RATP, Siemens, etc.

To address the issues above we plan a Shonan Meeting to discuss the issues around the
application of advanced formal methods in industry. We aim at promoting further
discussions on the classical but essential issues, while timely responding to the rapid
changes around software-intensive systems including the movement towards CPS. This
meeting invites leading researchers and practitioners who are actively working in the
industry or in the academia-industry collaboration.

The meeting will involve two kinds of sessions (possibly with a special session
described below). One is presentations and targeted discussions, where each participant
presents ideas and positions that then kicks off various directions of discussions. The
organisers will ensure that these presentations are structured around specific topics. The
other is sessions consisting of intensive follow-up discussions involving mixed groups
of participants. The meeting will use a dedicated method for conducting the intensive
discussion, the current plan is to use a variation of the world café method:
http://www.theworldcafe.com/method.html. The topics will be discovered at the
meeting, though the organizers will prepare some beforehand, e.g., what advance is
required for formal methods to deal with future CPS.

As many Japanese companies are interested in leveraging formal methods, we plan to
have a special session involving participants from these companies -not only the listed
invitees for attendance through the week but more invitees who can only attend half or
one day without stay. We may instead plan the session to be held at NII, before or after
the Shonan meeting, for the convenience of the venue.

[1] D. Bjørner et al. : 40 Years of Formal Methods – Some Obstacles and Some Possibilities?, FM 2014. Singapore.
[2] A. Hall : Seven Myths of Formal Methods, IEEE Software, Vol.7 No.5, 1990
[3] J. P. Bower et al. : Seven More Myths of Formal Methods, IEEE Software, Vol.12 No.4, 1995
[4] L. Maccherone et al. : Software Mythbusters Explore Formal Methods, IEEE Software, Vol.26 Nov.6, 2009
[5] T. Lecomte, Industrial use of Formal Methods for Safe and Secure Systems, Invited Talk. ISSRE 2016. Ottawa. Canada
[6] C. Newcombe et al. : How Amazon Web Services Uses Formal Methods, Communications of the ACM, Vol.58 No.4, 2015
[7] C. Calcagno et al. : Moving Fast with Software Verification, NFM 2014
[8] T. Kurita et al. : Practices for Formal Models as Documents: Evolution of VDM Application to “Mobile FeliCa” IC Chip
Firmware, FM 2015