Preface

The present volume contains the proceedings of the Fourth International Workshop on Engineering Safety and Security Systems (ESSS'15). The workshop was held in Oslo, Norway, on June 22nd, 2015, as a satellite event of the 20th International Symposium on Formal Methods (FM'15).

The goal of the workshop was to establish a platform for the exchange of ideas on

• methods, techniques and tools for system safety and security;
• methods, techniques and tools for analysis, certification, and debugging of complex safety and security systems;
• model-based and verification-based testing;
• emerging application domains such as cloud computing and cyber-physical systems;
• case studies and experience reports on the use of formal methods for analyzing safety and security systems.

This year, the 2nd International Workshop on Safety and Formal Methods (SAFOME'15) was merged into ESSS'15. This resulted in 15 submissions in total, which were all reviewed by at least three referees. After an intensive discussion by the PC members, we selected 6 papers for presentation at the workshop and inclusion in the proceedings. The program of ESSS'15 also included invited talks by Marieke Huisman (University of Twente, Netherlands) and Audun Jøsang (University of Oslo, Norway).

We would like to thank all the authors for submitting their work to ESSS'15 and SAFOME'15 and the members of the Program Committee as well as the external reviewers for their efforts and high-quality reviews. Finally, thanks are due to the organizers of SAFOME'15, Ricardo J. Rodríguez (Universidad de León, Spain) and Stefano Tonetta (Fondazione Bruno Kessler, Italy).

Abstracts of the Invited Talks

• Speaker: Marieke Huisman (University of Twente, Netherlands)
  Title: Verification of Concurrent Software
  Abstract: This talk presents the VerCors approach to verification of concurrent software. First we discuss why verification of concurrent software is important, but also challenging, and we show how permission-based separation logic allows one to reason about multithreaded Java programs in a thread-modular way. We discuss in particular how we extend the logic to reason about functional properties in a concurrent setting. Further, we show how the approach is also suited to reason about programs using a different concurrency paradigm, namely kernel programs using the Single Instruction Multiple Data paradigm. Concretely, we illustrate how permission-based separation logic is used to verify functional correctness properties of OpenCL kernels.
• Speaker: Audun Jøsang (Universiy of Oslo, Norway)
  Title: Modelling Reliability with Degrees of Uncertainty based on Subjective Logic
  Abstract: System reliability analysis is typically probability-based. However, it is often the case that some input arguments are missing or that they are affected by considerable uncertainty, in which case it becomes difficult or impossible to complete the reliability analysis. Subjective logic offers a simple solution whereby probabilistic arguments can be expressed with degrees of uncertainty. This approach can also be used for developing probabilistic formal models of systems, where e.g. assumptions and arguments can be expressed with degrees of uncertainty. This talk presents subjective logic and gives examples of how it can be applied to system reliability analysis.

Program Committee

• Étienne André, University Paris 13, France
• Thomas Arts, Quviq, Sweden
• Guangdong Bai, National University of Singapore, Singapore
• Clara Benac Earle, Universidad Politécnica de Madrid, Spain
• Marius Bozga, VERIMAG, France
• Elena Gómez-Martínez, Universidad Politécnica de Madrid, Spain
• Hans Hansson, Mälardalen University, Sweden
• Marieke Huisman, University of Twente, The Netherlands
• Weiqiang Kong, Dalian University of Technology, China
• Keqin Li, Huawei, Germany
• Yang Liu (PC co-chair), Nanyang Technological University, Singapore
• Sjouke Mauw (PC co-chair), University of Luxembourg, Luxembourg
• Thomas Noll, RWTH Aachen University, Germany
• Peter Csaba Ölveczky, University of Oslo, Norway
• Jun Pang (PC co-chair), University of Luxembourg, Luxembourg
• Cristian Prisacariu, University of Oslo, Norway
• Ricardo J. Rodríguez, Universidad de León, Spain
• Kristin Rozier, NASA/Cincinnati University, USA
• Harald Ruess, Fortiss, Germany
• Wilfried Steiner, TTTech, Austria
• Cong Tian, Xidian University, China
• Stefano Tonetta, Fondazione Bruno Kessler, Italy
• Mohammad Torabi Dashti, ETH Zurich, Switzerland
• Catia Trubiani, Gran Sasso Science Institute, Italy
• Anton Wijs, Eindhoven University of Technology, The Netherlands
• Yoriyuki Yamagata, Japan Advanced Institute of Science and Technology, Japan
• Tian Zhang, Nanjing University, China

External Reviewers

• Alvaro Botas
• Francesco Gallo
• Pingfan Kong
• Sander de Putter
• Ling Shi