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