Frédéric Lang

Francesco Flammini

Preface to the special issue on Formal Methods for Industrial Critical Systems (FMICS'2014) This special issue contains improved and extended versions of selected papers from the 19th International Workshop on Formal Methods for Industrial Critical Systems (FMICS), which was held in Florence (Italy) in September 2014.

The aim of the FMICS workshop series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. In particular, FMICS brings together scientists and engineers that are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. The FMICS workshop series also strives to promote research and development for the improvement of formal methods and tools for industrial applications. Topics of interest include:

• design, specification, code generation and testing based on formal methods;

• methods, techniques and tools to support automated analysis, certification, debugging, learning, optimization and transformation of complex, distributed, real-time systems and embedded systems; • verification and validation methods that address shortcomings of existing methods with respect to their industrial applicability (e.g., scalability and usability issues); • tools for the development of formal design descriptions;

• case studies and experience reports on industrial applications of formal methods, focusing on lessons learnt or identification of new research directions; • impact of the adoption of formal methods on the development process; application of formal methods in standardization and industrial forums.

The papers presented in this special issue are the result of several evaluation steps. FMICS 2014 received 26 papers among which 13 were accepted. After the workshop, selected papers were published in Lecture Notes of Computer Science volume 8718. The authors of 6 papers were invited to submit extended versions for publication in this special issue. Those papers passed two to three rounds of review and finally 5 were accepted to be included in the journal.

The contents of this issue illustrate the variety of problems, techniques, and application domains in the scope of formal methods for industrial critical systems. Four out of the five papers are about the application of formal methods to a particular problem, in a particular application domain, whereas the last one addresses the development of a formal verification technique, independently of any particular application domain:

• Lars Lockefeer, David M. Williams, and Wan Fokkink use process algebra and enumerative verification methods to verify that the TCP (Transmission Control Protocol) telecommunication protocol satisfies its requirements when extended with the Window Scale Option, an option of the protocol that was not taken into account in previous formal verification efforts. • Zhen Zhang, Wendelin Serwe, Jian Wu, Tomohiro Yoneda, Hao Zheng, and Chris Myers present a fault-tolerant routing algorithm in Network-on-Chip (NoC) architectures providing adaptivity for on-chip communications. Since fault-tolerance adaptivity increased algorithm complexity, formal verification techniques were needed and employed to check the correctness of the design and to prove properties like deadlock/livelock freedom and tolerance to single-link faults. • Thang Nguyen and Dejan Ničković apply a technology called assertion-based monitoring for mixed-signal systems to a real-world case study from the automotive domain, namely a Distributed System Interface mixed-signal protocol implementation in an airbag system-on-

chip application.

• Brian Campbell and Ian Stark apply formal techniques to test random instruction sequences on a microcontroller. The testing technique relies on a HOL (Higher-Order Logic) model of the microcontroller and an SMT (Satisfiability Modulo Theories) solver to find suitable microcontroller states in which instruction sequences are relevant. • At last, David Bühler, Boris Yakobowski, and Sandrine Blazy describe an enhanced abstract interpretation framework for sequential programs, which exploits the conditions of branches along the program control flow to improve performance of the analysis in particular situations.

The editors of this special issue thank the editorial board of Science of Computer Programming, who was of constant help in the process of producing this special issue. We also thank ERCIM and the board of its working group on Formal Methods for Industrial Critical Systems, the local organizers of FMICS 2014 in Florence, the participants to the workshop, and the authors.

Particularly warm thanks go to the anonymous referees of both the workshop and the special issue. We enjoyed preparing this issue and we hope you will enjoy reading it.

Frédéric Lang Inria Grenoble Rhône-Alpes/LIG/Université de Grenoble Alpes, 655, avenue de l'Europe, 38330 Montbonnot, France E-mail address:Frederic.Lang@inria.fr Francesco Flammini Ansaldo STS, Via Argine 425, 80147 Naples, Italy E-mail address:Francesco.Flammini@ansaldo-sts.com