Proceedings 4th International Workshop on
Edited by: Jun Pang, Yang Liu and Sjouke Mauw
Engineering Safety and Security Systems
Oslo, Norway, June 22, 2015
Yang Liu, Sjouke Mauw and Jun Pang||1|
Indefinite waitings in MIRELA systems
Johan Arcile, Jean-Yves Didier, Hanna Klaudel, Raymond Devillers and Artur Rataj||5|
Verification of railway interlocking systems
Simon Busard, Quentin Cappart, Christophe Limbrée, Charles Pecheur and Pierre Schaus||19|
Automatic Generation of Minimal Cut Sets
Sentot Kromodimoeljo and Peter A. Lindsay||33|
Breaking Dense Structures: Proving Stability of Densely Structured Hybrid Systems
Eike Möhlmann and Oliver Theel||49|
Formal Verification of Real-Time Function Blocks Using PVS
Linna Pang, Chen-Wei Wang, Mark Lawford, Alan Wassyng, Josh Newell , Vera Chow and David Tremaine||65|
Using Indexed and Synchronous Events to Model and Validate Cyber-Physical Systems
Chen-Wei Wang, Jonathan S. Ostroff and Simon Hudon||81|
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
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).
30th of April, 2015
Jun Pang, Yang Liu, Sjouke Mauw
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.
- É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
- Alvaro Botas
- Francesco Gallo
- Pingfan Kong
- Sander de Putter
- Ling Shi