Published: 25th June 2018
DOI: 10.4204/EPTCS.272
ISSN: 2075-2180

EPTCS 272

Proceedings of the 1st International Workshop on
Methods and Tools for Rigorous System Design
Thessaloniki, Greece, 15th April 2018

Edited by: Simon Bliudze and Saddek Bensalem

Preface
Simon Bliudze and Saddek Bensalem
Invited Paper: System Design in the Era of IoT — Meeting the Autonomy Challenge
Joseph Sifakis
1
Invited Talk: TASTE — Using Model-Driven Code Generation for Safety-Critical Targets
Thanassis Tsiodras
23
Model-Based Design of Energy-Efficient Applications for IoT Systems
Alexios Lekidis and Panagiotis Katsaros
24
A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems
Pujie Han, Zhengjun Zhai, Brian Nielsen and Ulrik Nyman
39
Formal Verification of Usage Control Models: A Case Study of UseCON Using TLA+
Antonios Gouglidis, Christos Grompanopoulos and Anastasia Mavridou
52
SENSE: Abstraction-Based Synthesis of Networked Control Systems
Mahmoud Khaled, Matthias Rungger and Majid Zamani
65
Process Network Models for Embedded System Design Based on the Real-Time BIP Execution Engine
Fotios Gioulekas, Peter Poplavko, Panagiotis Katsaros and Pedro Palomo
79
DesignBIP: A Design Studio for Modeling and Generating Systems with BIP
Anastasia Mavridou, Joseph Sifakis and Janos Sztipanovits
93
Verification of Shared-Reading Synchronisers
Afshin Amighi, Marieke Huisman and Stefan Blom
107
Treo: Textual Syntax for Reo Connectors
Kasper Dokter and Farhad Arbab
121

Preface

This volume contains the proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (MeTRiD 2018), held on the 15th of April, 2018 in Thessaloniki, Greece as part of ETAPS 2018, the European Joint Conferences on Theory and Practice of Software.

The term Rigorous System Design (RSD) denotes the design approach that is based on a formal, accountable and iterative process for deriving trustworthy and optimised implementations from models of application software, its execution platform and its external environment. Ideally, a system implementation is derived from a set of appropriate high-level models by applying a sequence of semantics-preserving transformations.

The ambition of MeTRiD is to promote the use of formal methods, in general, and the RSD approach, in particular, in the industrial applications and, reciprocally, bring the attention of the formal methods researchers to such industrial applications in order to develop realistic case-studies and guide the evolution of tools. Striving towards this ambitious goal, we have solicited contributions of three types:

We have received 13 submissions (7 regular, 4 tool and 2 case study papers), whereof 8 (5 regular, 2 tool, 1 case study paper) have been accepted for presentation at the workshop.

Each submitted paper was reviewed by three independent reviewers under a lightweight double-blind policy. This policy requires the authors to invest reasonable effort into concealing their identities. However, the main goal was to allow for unbiased review: anonymisation should not have affected the quality of submissions, nor in any way hamper their evaluation.

Pre-proceedings versions of the accepted papers, as well their corresponding presentation slides, and a video recording, synchronised with the presentation slides, of the invited talk by Joseph Sifakis, are available on the MeTRiD website.

In this volume, the final versions of the accepted papers are complemented by an invited paper by Joseph Sifakis.

We would like to thank the authors of all the submitted papers for their interest in the workshop, the PC members for their efforts, and the workshop attendees for active participation in the discussion, all of which together have provided for the success of the MeTRiD workshop. We thank Joseph Sifakis and Thanassis Tsiodras for accepting our invitations to present their recent work, and the ETAPS 2018 organisers — particularly the general chair Panagiotis Katsaros — for providing an excellent environment for the preparation and staging of the event. We are very much grateful to Rob van Glabbeek and the EPTCS staff for their help in preparing these proceedings.

Simon Bliudze (Inria Lille – Nord Europe, France)
Saddek Bensalem (Verimag / Université Grenoble Alpes, France)

Program committee


TASTE — Using Model-Driven Code Generation for Safety-Critical Targets

Thanassis Tsiodras (European Space Agency)

Back in 2004, while working as the Senior Software Engineer and Technical Lead of Semantix — a company he co-founded — Dr Tsiodras found himself facing a significant technical challenge: 7 different versions of evolving telecom protocols had to be properly handled, with more than three thousand validation rules (for each one of them!) requiring implementation...

Reading the right paper at the right time, Dr Tsiodras realized that instead of writing the code himself, he could instead create a small language to describe the logic of the validations, mergings, etc. — and then create a parser and code generator that would write the code for him.

Six months and about a dozen code generators later, 700'000 lines of C++ code were automatically created — addressing all the needs for all possible versions of these files — validations, conversions, mergings, mass-processing, etc. The resulting product line was released, and it quickly became world leading — with the rather distinctive characteristic of zero bug reports after more than a decade — in spite of the fact that major telecom companies from all over the world are using the tools on a daily basis, processing millions of call records...

ESA became aware of this work through a presentation done a few years later. The Agency had always been — and still is — on the lookout for ways to shield mission codebases from errors; since any one of them may lead to mission loss. The right people from ESA witnessed that presentation, and involved Dr Tsiodras' company — and him personally — in a series of projects, where TASTE was born and rapidly evolved into an ever-expanding set of closely knit model-to-model and model-to-code transformation engines.

In this talk, Dr Tsiodras shared with the workshop attendees what TASTE is, how it started, how it evolved into what it is today, and what it provides in terms of real-world semantics-preserving model transformations; with specific emphasis on targeting the safety-critical domains.