Published: 25th June 2018|
|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|
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.
(Inria Lille – Nord Europe, France)
Saddek Bensalem (Verimag / Université Grenoble Alpes, France)
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.