Date: Thursday 12 March 2015
Time: 16:00 - 17:30
Location / Room: Chartreuse

Chair:
Marc Geilen, Eindhoven University of Technology, NL

Co-Chair:
Laurence Pierre, TIMA Lab, FR

This session presents different aspects of high-level specifications and models. The first paper introduces a new model of computation, fixed-priority process networks to address the need of determinism for multiprocessor applications. The second paper proposes an approach to detect and resolve potential synchronization problems between a discrete event simulation and timed dataflow simulation. The third paper presents a framework for checking the logical consistency of requirements in specifications written in a subset of natural language.

Time	Label	Presentation Title Authors
16:00	12.4.1	MODELS FOR DETERMINISTIC EXECUTION OF REAL-TIME MULTIPROCESSOR APPLICATIONS Speakers: Peter Poplavko1, Dario Socci2, Paraskevas Bourgos3, Marius Bozga3 and Saddek Bensalem3 1Universite Joseph Fourier / Verimag, FR; 2Verimag, ; 3Verimag, FR Abstract With the proliferation of multi-cores in embedded real-time systems, many industrial applications are being (re-)targeted to multiprocessor platforms. However, exactly reproducible data values at the outputs as function of the data and timing of the inputs is less trivial to realize in multiprocessors, while it can be imperative for various practical reasons. Also for parallel platforms it is harder to evaluate the task utilization and ensure schedulability, especially for end-to-end communication timing constraints and aperiodic events. Based upon reactive system extensions of Kahn process networks, we propose a model of computation that employs synchronous events and event priority relations to ensure deterministic execution. For this model, we propose an online scheduling policy and establish a link to a well-developed scheduling theory. We also implement this model in publicly available prototype tools and evaluate them on state-of-the art multi-core hardware, with a streaming benchmark and an avionics case study. Download Paper (PDF; Only available from the DATE venue WiFi)
16:30	12.4.2	PRE-SIMULATION SYMBOLIC ANALYSIS OF SYNCHRONIZATION ISSUES BETWEEN DISCRETE EVENT AND TIMED DATA FLOW MODELS OF COMPUTATION Speakers: Liliana Andrade1, Torsten Maehne1, Alain Vachoux2, Cédric Ben Aoun1, François Pecheux1 and Marie-Minerve Louerat3 1Pierre et Marie Curie University, LIP6, FR; 2École Polytechnique Fédérale de Lausanne (EPFL), CH; 3University Pierre et Marie Curie, FR Abstract The SystemC AMS extensions support heterogeneous modeling and make use of several Models of Computation (MoCs) that operate on different time scales in the Discrete Event (DE), Discrete Time (DT), and Continuous Time (CT) domains. The simulation of such heterogeneous models may raise synchronization problems that are hard to diagnose and to fix, especially when considering multi-rate data flow parts. In this paper, we show how to formally analyze the execution of Timed Data Flow (TDF) models including their interaction with the DE domain by converting the synchronization mechanics into a Coloured Petri Net (CPN) equivalent. The developed symbolic execution algorithm for the CPN allows to detect all DE-TDF synchronization issues before simulation and to propose appropriate sample delay settings for the TDF converter ports to make the system schedulable. The presented technique is validated with a case study including a vibration sensor model and its digital front end. Download Paper (PDF; Only available from the DATE venue WiFi)
17:00	12.4.3	FORMAL CONSISTENCY CHECKING OVER SPECIFICATIONS IN NATURAL LANGUAGES Speakers: Rongjie Yan1, Chih-Hong Cheng2 and Yesheng Chai3 1Institute of Software, Chinese Academy of Sciences, CN; 2ABB Corporate Research, DE; 3School of Computer Science & Technology, Soochow University, CN Abstract Early stages of system development involve outlining desired features such as functionality, availability, or usability. Specifications are derived from these features that concretize vague ideas presented in natural languages. The challenge for the verification and validation of specifications arises from the syntax and semantic gap between different representations and the need of automatic tools. In this paper, we present a requirement-consistency maintenance framework to produce consistent representations. The first part is the automatic translation from natural languages describing functionalities to formal logic with an abstraction of time. It extends pure syntactic parsing by adding semantic reasoning and the support of partitioning input and output variables. The second part is the use of synthesis techniques to examine if the requirements are consistent in terms of realizability. When the process fails, the formulas that cause the inconsistency are reported to locate the problem. Download Paper (PDF; Only available from the DATE venue WiFi)
17:30		End of session