We present here the main features and lessons learned from the first edition of what has now become the ECRTS industrial challenge, together with the final description of the challenge and a comparative overview of the proposed solutions. This verification challenge, proposed by Thales, was first discussed in 2014 as part of a dedicated workshop (FMTV, a satellite event of the FM 2014 conference), and solutions were discussed for the first time at the WATERS 2015 workshop. The use case for the verification challenge is an aerial video tracking system. A specificity of this system lies in the fact that periods are constant but known with a limited precision only. The first part of the challenge focuses on the video frame processing system. It consists in computing maximum values of the end-to-end latency of the frames sent by the camera to the display, for two different buffer sizes, and then the minimum duration between two consecutive frame losses. The second challenge is about computing end-to-end latencies on the tracking and camera control for two different values of jitter. Solutions based on five different tools - Fiacre/Tina, CPAL (simulation and analysis), IMITATOR, UPPAAL and MAST - were submitted for discussion at WATERS 2015. While none of these solutions provided a full answer to the challenge, a combination of several of them did allow to draw some conclusions.

To offer an infrastructure for autonomous systems offloading parts of their functionality, dynamic distributed systems must be able to satisfy non-functional quality-of-service (QoS) requirements. However, providing hard QoS guarantees without complex global verification that are satisfied even under uncertain conditions is very challenging. In this work, we propose a contract-based QoS assurance for centralized, hierarchical systems, which requires local verification only and has the potential to cope with dynamic changes and uncertainties.

Building correct distributed systems is challenging, and any attempt for providing a direct, global proof of correctness of a distributed system is bound to fail. An interesting alternative approach consists in starting from a specification or program of the system under construction, verifying all properties of interest on it - which has a much lower complexity than the verification on a distributed implementation - and finally derive a distributed implementation using some correct by-construction approach. Note that this topic is related to distributed control, where the objective is to enforce in a distributed manner some global constraint on a plant. Deriving such a distributed controller directly is difficult, and the correctness of the resulting controller is difficult to prove. A more feasible approach in this context is to first construct a global controller, then transform it into distributed one, again by means of a correct-by-construction approach.

In this paper, we add to the usual notion of contract a structural part specifying the composition operator used to compose the component and its environment. We provide a framework for compositional verification including a proof rule for dominance between contracts based on apparent circular reasoning. We also briefly describe a consistency condition and a method based on assumption generation to generate or refine contracts.

This paper summarizes our experience with IF, an open validation environment for distributed software systems. Indeed, face to the increasing complexity of such systems, none of the existing tools can cover by itself the whole validation process. The IF environment was built upon an expressive intermediate language and allows to connect several validation tools, providing most of the advanced techniques currently available. The results obtained on several large case-studies, including telecommunication protocols and embedded software systems, confirm the practical interest of this approach.

Abstract We present a method for thecompositional constructionof theminimal transition systemthat represents the semantics of a given distributed system. Our aim is to control thestate explosioncaused by the interleavings of actions of communicating parallel components byreduction stepsthat exploitglobalcommunication constraints given in terms ofinterface specifications.Theeffectof the method, which is developed forbisimulation semanticshere, depends on the structure of the distributed system under consideration, and theaccuracyof the interface specifications. However, itscorrectnessis independent of the correctness of the interface specifications provided by the program designer.