Op0009:15add Op00 to agenda

 INVITED TALKS OF THE CONFERENCE PRESIDENTS

09:15 - 09:45 - Keynote speach on "European Space - facts and figures" by  Kjeld Hjortnaes

09:45 - 10:30 - Keynote speach on "Internet of Things: challenges & opportunities"  by Joseph Sikakis

We.1.A.111:00add We.1.A.1 to agenda

Download We.1.A.1

Data Flow Model Coverage Analysis: Principles and Practice

Jean-Louis Camus - Esterel Technologies, France Carole Haudebourg - Esterel Technologies, France Marc Schlickling - Konzept Informationssysteme GmbH, Germany Jörg Barrho - MTU, Germany

Safety critical software requires rigorous processes in order to achieve a high degree of integrity. These processes include so-called “verification of verification”. In the case of Model Based Development and Verification, DO-178C/DO-331 requires model coverage analysis. This paper reminds the objectives of model coverage analysis and the difference with structural code coverage analysis. It proposes coverage criteria suited to data flow models. These criteria are a generalization of the functional masking effect and also take into account modularity and in-lining of the model operators. It presents a tool supporting model coverage analysis according to these criteria. It concludes with industry field experience and future extensions.

We.1.A.211:30add We.1.A.2 to agenda

Download We.1.A.2

Applying Model-Based Techniques for Aerospace Projects in Accordance with DO-178C, DO-331, and DO-333

Ulrich Eisemann - dSPACE, Germany

The new standard for software development in civil aviation, DO-178C, mainly differs from its predecessor DO-178B, in that it has standard supplements to provide greater scope for using new software development methods. The most important standard supplements are DO-331 on the methods of model-based development and model-based verification and DO-333 on the use of formal methods such as model checking and abstract interpretation. These key software design techniques offer enormous potential for achieving highly efficient software development in the aerospace sector while not only maintaining the high quality and safety requirements for software but actually improving them. This article presents a model-based tool chain for DO-178C/DO-331-compliant projects making use of several innovative techniques like mechanisms for converting textual requirements to formalized requirements, the representation of requirements as specification or design models, the use of automatic production code generation to develop source code and various verification techniques. The latter involve the use of simulation, automatic test case generation and model checking to verify models as well as highly integrated execution environments to verify the executable object code. In summary, the techniques presented provide powerful mechanisms not only for requirements definition and design, but especially for the various verification steps to meet the objectives of DO-178C.

We.1.A.312:00add We.1.A.3 to agenda

Download We.1.A.3

Introducing SCADE Model–Based Development into a Safety-Critical System Environment

Philip Birkin - Rolls-Royce - Controls and Data Services, United Kingdom of Great Britain and Northern Ireland Duncan Brown - Rolls-Royce - Controls and Data Services, United Kingdom of Great Britain and Northern Ireland

With the publishing of ED-12C and ED-218, an opportunity has been created in which Model-Based Development is better defined for a Safety Critical System Environment. This positioning paper describes the approach and methodology applied to move from a conventional development, to a Model-Based Development. The major issue of how to integrate the two development methodologies and the business benefits is discussed.

We.1.B.111:00add We.1.B.1 to agenda

Download We.1.B.1

Hard Real Time and Mixed Time Criticality on Off-The-Shelf Embdedded Multi-cores

Albert Cohen - INRIA-Parkas, France Valentin Perrelle - CEA-List, France Dumitru Potop-Butucaru - INRIA-AOSTE, France Marc Pouzet - INRIA-Parkas, France Elie Soubiran - IRT/SystemX & Alstom Transport, France Zhen Zhang - INRIA-Parkas, France

This paper presents the design of a synchronous language enabling hard real-time applications to run on off-the-shelf multicore platforms.

We.1.B.211:30add We.1.B.2 to agenda

Download We.1.B.2

DREAMS about reconfiguration and adaptation in avionics

Guy Durrieu - ONERA, France Gerhard Fohler - TU Kaiserslautern, Germany Gautam Gala - TU Kaiserslautern, Germany Sylvain Girbal - Thales, France Daniel Gracia Perez - Thales, France Eric Noulard - ONERA, France Claire Pagetti - ONERA, France Simara Perez - TU Kaiserslautern, Germany

The paper describes the reconfiguration approach implemented in the DREAMS middleware to cope with failures and how the concepts are tested on an avionic demonstrator.

We.1.B.312:00add We.1.B.3 to agenda

Download We.1.B.3

A Multi-Core Interference-Aware Schedulability Test for IMA Systems, as a Guide for SW/HW Integration

Soukayna M'Sirdi - Airbus Group Innovations / IRIT lab, France Wenceslas Godard - Airbus Group Innovations, France Marc Pantel - IRIT, France

We propose a formal and computer-aided approach for the reuse of IMA (Integrated Modular Avionics) legacy code on multi-core platforms. No software nor hardware modification is needed. We focus on the SW/HW integration phase, where (i) IMA partitions are allocated to cores, (ii) a scheduling table is produced, and (iii) scheduling analysis is performed to ensure the validity of the final configuration. We aim to automate as much as possible these three activities, and reduce time-to-market by integrating timing analyses inside the design space exploration phase for the partition-to-core allocation. The exploration and analysis are interference-aware, since a safe bound for memory interference is produced for each task. To do so, we formulate an optimization problem for the allocation of IMA partitions to the cores of a multi-core. For each tested allocation, the schedulability of the partitions and tasks are verified. Partitions are schedulable if there exists a feasible schedule for their tasks, and if the time window necessary for each partition is smaller than their respective deadlines. The schedulability of the tasks is verified with the response time analysis, a necessary and sufficient condition of schedulability. Inside the response time analysis, a safe bound for worst case memory interference of each task is taken into account. To compute these bounds, we use the method published by H. Kim in cite{X}, based on a detailed modeling of intra-bank and inter-bank DRAM access delays. We adapt Kim's work to the avionics case to take the partitions level into account in the inter-task memory interferences. %To sum up, we perform interference-aware schedulability analysis inside the design space exploration of partition-to-core allocation. To sum up, we guide the partition-to-core allocation research process with interference-aware schedulability analysis, integrated inside the design space exploration process.

We.1.C.111:00add We.1.C.1 to agenda

Download We.1.C.1

Formal Specs Verifier ATG: a Tool for Model-based Generation of High Coverage Test Suites

Alberto Ferrari - Advanced Laboratory on Embedded Sys (ALES) S.r.l., Italy Orlando Ferrante - Advanced Laboratory on Embedded Sys (ALES) S.r.l., Italy Marco Marazza - Advanced Laboratory on Embedded Sys (ALES) S.r.l., Italy

In this paper we describe Formal Specs Verifier Automatic Test Generation, a tool generating high coverage test suites for embedded systems. Our tool implements a test case synthesis algorithm using a combination of model checking and optimization techniques starting from a Simulink/Stateflow model of the System Under Test. The main contributions of this paper are the following: we (1) give an extended description of our test generation algorithm, (2) describe the algorithm implementation as part of the Formal Specs Verifier framework, (3) present a concrete application of the tool to a cruise control case study and discuss experimental results comparing our algorithm with a state-of-the art COTS tool.

We.1.C.211:30add We.1.C.2 to agenda

Download We.1.C.2

Model Checking of Scade Designed Systems

Sebastien Heim - CSSI, France Xavier Dumas - CSSI, France Philippe Dhaussy - ENSTA-Bretagne, France Ciprian Teodorov - ENSTA-Bretagne, France Eric Bonnafous - CS-SI, France Luka Leroux - ENSTA Bretagne, France

Model checking is a well-known method to verify a formal model in all possible configurations. Nevertheless this technique can hardly scale up to industrial asynchronous systems because of the state-space explosion problem. To address this challenge, a new approach based on context specification (the environment of the system) and an observation engine called OBP (Observer Based Prover) has been developed. The idea is that given a property to be verified, one doesn’t need to explore all possible configurations of the complete system. Among all possible behavior of the system, a tiny part is representative enough for the property to be verified. Thus, specifying a pertinent environment (a context) allows restricting the system behavior on those only parts where the property is worth verifying. The objective of our work is to apply this Context-aware verification method to the verification of SCADE systems designed in LUSTRE language, in order to check behavioral properties related to system safety. Moreover LUSTRE is a synchronous language whereas OBP exploration engine takes as input an asynchronous model designed in FIACRE language. To cope with this problem our approach consists in developing a GALS method combining asynchronous contexts with synchronous models.

We.1.C.312:00add We.1.C.3 to agenda

Download We.1.C.3

Industrial Grade Model Checking

Mathieu Clabaut - Systerel, France Ning Ge - Systerel, France Nicolas Breton - Systerel, France Eric Jenn - IRT Saint-Exupéry, France Rémi Delmas - Onera, France Yoann Fonteneau - Systerel, France

Model checking has made a lot of progress since its infancy. For a long time, industrial applications were still limited to some very specific domains out of which the technique bumps into the state explosion wall. Nowadays things evolve and some tools are able to tackle real world use cases outside of the known domains. We give here the feedback collected when using model checking on several industrial strength use cases and give indication on how we take into account the specific domain constraints.

We.1.D.111:00add We.1.D.1 to agenda

Download We.1.D.1

Safety and Security for the internet of Things

Mehmet Oezer - SYSGO, Germany Jacques Brygier - Sysgo, Germany

A key software component for safe and secure IoT There is no need today to present the Internet of Things (IoT) paradigm as the topic is so visible and well recognized by a large audience that goes beyond the scope of industrial players and professionals. There is a consensus within the industry and the public authorities that the IoT represents the major evolution of the coming decade regarding the design and production of equipments and devices developed in all industrial and consumers’ areas. One of the most important parts of this technological evolution is the new role played by the embedded systems that are now at the heart of all connected objects. Embedded systems are defined as the combination of hardware and software solutions that implement the functionality and the services offered by the device. The increasingly important element of the system is the software component that interfaces the hardware with the application software. For very small devices using MCU (Micro Controller Unit), this component could be quite limited but the growing need of functionality combined with the availability of powerful yet affordable processors makes the use of RTOS (Real-Time Operating System) more and more necessary. The technological evolution induced by the IoT impacts also the design of RTOSs. A new generation of RTOSs is required to address the new requirements of modularity, security, safety, and virtualization. This last capability is getting more and more popular with the emergence of so-called “hypervisors”, but the combination of a true RTOS and a hypervisor covering all requirements mentioned above is still rare. Embedded virtualization as a foundation IoT bears new challenges where safety critical control tasks are executed with high dynamic and interconnected environment with persistent security threats. An attack to a water heating system, which provides boiling water instead of tempered water, or a control valve for a chemical process, which is ‘out of control’ will compromise the systems safety. Thus, the safety function cannot be treated in isolation and the only way for dependable IoT architectures is to implement devices with safety and security by-design. The current approach to security in complex interconnected systems can be called from “hope” in the worse case to “patching day” in the best case with focus rather on individual aspects (e.g. cryptography) and ignoring the architecture level. These approaches work well until a skilled programmer finds the next vulnerability. That is, we need a new approach to fundamentally secure connected device. The very same holds for physically separated or air-gapped devices because they still have external interfaces (e.g. USB for maintenance). Stuxnet is a good public example for the fact that physical separation does not secure system. We propose to treat safety and security right at the resource management level of an IoT device. The resource management is implemented as a high-assurance embedded hypervisor PikeOS which controls CPUs, memory, IO memory, GPU, FPGA, IO devices, communication stacks to the environment, inter-application communication channels, management API. The safety properties are real-time, worse case-execution time, time- and space separation, non-interference, predictability, assurance levels with respect to the required safety standards. The relevant safety standards are ISO 61508 (safety), IEC50128/529 (railway), DO-178B (avionics), ISO 26262 (automotive). The security properties are integrity and confidentiality of data stored and used on the device resources, availability of the device resources, resistance to malicious behavior when any application can be source of an attack, secure communication and update, separation of applications, and assurance levels as defined in Common Criteria and IEC-62443 standards. Hypervisor properties required to solve the problem We present how usage of an appropriate hypervisor transparently forces system architect to build-in safety and security in the device. The basic concept is simple “divide et impera” and is implemented as seamless process of appointing applications to their virtual machines, assigning resources and execution time to virtual machines, defining explicit communication means etc. We show how the hypervisor takes over the rest, i.e. it guarantees that, that is not specified will not happened. This based on the main safety and security paradigms of PikeOS, which are separation of resources and data, controlled information flow and white list policy. A typical use-case already developed for the automotive industry shows how PikeOS can be used to address the different industrial requirements (see figure 1). This type of approach has been successfully implemented for many industrial applications in the avionics and railway areas, where safety and now security certifications are required. A vehicle is one example of the new IoT world, even if automobiles are not especially new equipment. What makes this equipment a true part of the IoT world is the fact that a car is more and more seen as a connected object. In the paper we present we however illustrate the usage of hypervisor-based platforms on three other IoT use-cases: • IoT gateway: we focus on inter-working, multitude of communication interfaces and field buses, as well as performance and real-time requirements • Sensor fusion: we bring the separated sensed data into the comprehensive picture while preserving and providing platform for local processing • Networked industrial control system: we show how SCADA, ICS, and operational plane are work together with preserving properties of the technological process while constantly providing the system level security

We.1.D.211:30add We.1.D.2 to agenda

Download We.1.D.2

A Distributed User-Centered Approach For Control In Ambient Robotic

Nicolas Verstaevel - Sogeti High Tech, France Regis Christine - IRIT - Université de Toulouse, France Marie-Pierre Gleizes - IRIT - Université de Toulouse, France Fabrice Robert - SOGETI HIGH TECH, France

Designing a controller to supervise an ambient application is a complex task. Any change in the system composition or end-users needs involves re-performing the whole design process. Giving to each device the ability to self-adapt to both end-users and system dynamic is then an interesting challenge. This article contributes to this challenge by proposing an approach named Extreme Sensitive Robotic where the design is not guided by finality but by the functionalities provided. One functionality is then seen as an autonomous system, which can self-adapt to what it perceives from its environment (including human activity). We present ALEX, the first system built upon the Extreme Sensitive paradigm, a multi-agent system that learns to control one functionality in interaction with its environment from demonstrations performed by an end-user. We study through an evolutive experimentation how the combination of Extreme Sensitive Robotic paradigm and ALEX eases the maintenance and evolution of ambient systems. New sensors and effectors can be dynamically integrated in the system without requiring any action on the pre-existing components.

We.1.D.312:00add We.1.D.3 to agenda

Download We.1.D.3

Development of an algorithm for energy efficient automated train driving

Artem Ozhigin - Siemens LLC, Russian Federation Pavel Prunev - Siemens LLC, Russian Federation Victor Sverdlin - Siemens LLC, Russian Federation Yulia Vikulina - Siemens LLC, Russian Federation

Automated train driving function is highly demanded in high-speed and commuter trains operated by Russian railways. Siemens Corporate Technology is involved in development of such real-time function within "robotized" train control system. Main intention of the system is not only to relieve the human driver from routine control over traction and brakes (letting him to pay more attention to assurance of safety) but also to increase train efficiency by reducing the amount of consumed energy. System architecture of Siemens trains implies that automated train driving control is performed indirectly through train safety control systems and therefore it should satisfy certain conditions to give a tangible effect on energy efficiency. This paper presents the experience in implementation and verification of automated train driving algorithms for Velaro RUS and Desiro RUS trains.

We.2.A.114:45add We.2.A.1 to agenda

Download We.2.A.1

Structural Coverage Criteria for Executable Assertions

Cyrille Comar - AdaCore, France Jérôme Guitton - AdaCore, France Olivier Hainque - AdaCore, France Thomas Quinot - AdaCore, France

Programming languages such as Eiffel or Ada 2012 promote the notion of ``design by contract'' or ``contract based programming'', where expectations regarding the program behavior are stated as ``assertions'' (Boolean expressions expected to always hold True) at various points. When assertions translate as executable code, tests verify that the expectations are obeyed. For safety critical software requiring structural coverage analysis, specific criteria typically apply to Boolean expressions in general, with variations depending on the certification level. A typical example is the DO-178 standard for airborne software, which mandates ``decision coverage'' at the so-called level B and ``MCDC coverage'' at level A. We believe that these traditional criteria aren't quite adequate for the particular case of assertions, for which coverage can never be achieved for these criteria, as they by construction never evaluate to False. In this paper, we therefore propose alternative coverage criteria for such expressions, for various criticality levels.

We.2.A.215:15add We.2.A.2 to agenda

Download We.2.A.2

MIMOSA: Towards a model driven certification process

Pierre Bieber - ONERA, France Frédéric Boniol - ONERA, France Guy Durrieu - ONERA, France Olivier Poitou - ONERA, France Thomas Polacsek - ONERA, France Virginie Wiels - ONERA, France Ghilaine Martinez - DGA, France

Certification process usually consists in analyzing, in a restricted amount of time a, potentially very large, set of documents that are intended to convince the auditor that the documented system fulfills all its requirements. The MIMOSA Project presented in this paper introduces a model driven certification process based on the key concepts of argumentation step, patterns and composition. The aim is: at first, to structure the documentation provided as evidences of the good properties of the system, and then to check this structure against identified argumentation patterns that will help identifying lacks or misuse of elements. Argumentation step and composition principles as well as a set of patterns for arguing about real-time properties are given along with their expression in a prototype tool, that offers to describe both the architecture, requirements and argumentation in a common language and then offers to compute some basic checks on the argumentation structure.

We.2.A.315:45add We.2.A.3 to agenda

Download We.2.A.3

Perspectives on Probabilistic Assessment of Systems and Software

Emmanuel Ledinot - Dassault Aviation, France Jean-Paul Blanquart - Airbus Defence and Space, France Jean Gassino - IRSN, France Bertrand Ricque - Safran, France Philippe Baufreton - Safran, France Jean-Louis Boulanger - CERTIFER, France Jean-Louis Camus - ANSYS-Esterel Technologies, France Cyrille Comar - Adacore, France Hervé Delseny - Airbus, France

Safety standards in most domains (aeronautics, automotive, industry, nuclear, railway, space) consider software (and more generally, design) as a deterministic artefact. They propose a global rationale combining probabilistic evidence on hardware random failures and deterministic evidence on systematic causes of failures including software. In a context where software is more and more pervasive in all systems, and where it is sometimes advocated that software complexity and size seem to provide some relevance to a probabilistic view of software behaviour, several initiatives suggest to change the way to address software in the global system safety assessment. This is a complex question with many facets. Among them the authors propose to discuss in the paper: - foundations, relevance and limits of probabilistic assessment for software, - relationship between software criticality category, (or class, DAL/SIL/ASIL/SSIL etc.) and probabilistic safety objectives, - the rationale for software diversification and to what extent probabilistic assessment is part of it.

We.2.B.114:45add We.2.B.1 to agenda

Download We.2.B.1

AeroRing: Avionics Full Duplex Ethernet Ring with High Availability and QoS Management

Ahmed Amari - University of Toulouse/ISAE, France Ahlem Mifdaoui - University of Toulouse/ISAE, France Fabrice Frances - University of Toulouse/ISAE, France Jerome Lacan - University of Toulouse/ISAE, France David Rambaud - BetaTech, France Loic Urbain - Eca Group, France

The avionics standard AFDX has been introduced to provide high speed communication for new generation aircraft. However, this switched network is deployed in a full redundant way, which leads to significant quantities of wires. To cope with this issue, a new avionic communication network, named AeroRing, based on a Gigabit Ethernet technology and implementing a daisy-chain wiring scheme on a Full Duplex ring topology, is proposed in this paper to decrease the weight and complexity of wiring, while guaranteeing the avionics requirements in terms of performance and reliability. First, we detail the main features of such a proposal and particularly the QoS and fault management mechanisms. Then, performance and reliability analysis is conducted to highlight its ability to guarantee the avionics requirements.

We.2.B.215:15add We.2.B.2 to agenda

Download We.2.B.2

Performance impact of the interactions between time-triggered and rate-constrained transmissions in TTEthernet

Marc Boyer - ONERA, France Hugo Daigmorte - ONERA, France Jörn Migge - RTaW, France Nicolas Navet - University of Luxembourg, Luxembourg

Switched Ethernet is becoming a de-facto standard in industrial and embedded networks. Many of today’s applications benefits from Ethernet’s high bandwidth, large frame size, multicast and routing capabilities through IP, and the availability of the standard TCP/IP protocols. There are however many variants of Switched Ethernet networks, just considering the MAC level mechanisms on the stations and communication switches. An important technology in that landscape is TTEthernet, standardized as SAE6802, which allows the transmission of both purely time-triggered (TT) traffic and sporadic (or rate-constrained - RC) traffic. To the best of our knowledge, the interactions between both classes of traffic have not been studied so far in realistic configurations. This work aims to shed some light on the kind of performances, in terms of latencies, jitters and useful bandwidth that can be expected from a mixed TT and RC configuration. The following issues will be answered by sensitivity analysis in a quantified manner: How do both classes of traffic interfere with each other? What are the typical worst-case latencies and useful bandwidth that can be expected for a RC stream for various TT traffic loads? To which extent the accuracy of the stations’ clocks does impact the latencies and the useful bandwidth? This study builds on a worst-case traversal time analysis developed for SAE6802, and explores these questions by experiments performed on avionics and automotive configurations of various sizes. Ultimately we aim to provide first methodological guidelines for the deployment of SAE6802 in large time-sensitive applications.

We.2.B.315:45add We.2.B.3 to agenda

Download We.2.B.3

A Symbiotic Approach to Designing Cross-Layer QoS in Embedded Real-Time Systems

Florian Greff - Thales Research & Technology, LORIA (University of Lorraine), France Eric Dujardin - Thales Research & Technology, France Arnaud Samama - Thales Research & Technology, France Ye-Qiong Song - LORIA - University of Lorraine, France Laurent Ciarletta - LORIA - University of Lorraine, France

Nowadays there is an increasing need for embedded systems to support intensive computing while maintaining traditional hard real-time and fault-tolerant properties. Extending the principle of multi-core systems, we are exploring the use of distributed processing units interconnected via a high performance mesh network as a way of supporting distributed real-time applications. Fault-tolerance can then be ensured through dynamic allocation of both computing and communication resources. We postulate that enhancing QoS (Quality of Service) for real-time applications entails the development of a cross-layer support of high-level requirements, thus requiring a deep knowledge of the underlying networks. In this paper, we propose a new simulation/emulation/experimentation framework, ERICA, for designing such a feature. ERICA integrates both a network simulator and an actual hardware network to allow the implementation and evaluation of different QoS-guaranteeing mechanisms. It also supports real-software-in-the-loop, i.e. running of real applications and middleware over these networks. Each component can evolve separately or together in a symbiotic manner, also making teamwork more flexible. We present in more detail our discrete-event simulation approach and the in-silicon implementation with which we cross-check our solutions in order to bring real performance aspects to our work. We also discuss the challenges of running real-software-in-the-loop in a real-time context, i.e. how to bridge it with a network simulator, and how to deal with time consistency.

We.2.C.114:45add We.2.C.1 to agenda

Download We.2.C.1

Fine-Tuning the Accuracy of Numerical Computations in Avionics Automatic Code Generators

Alexis Werey - Airbus Operations SAS, University of Perpignan, France David Delmas - Airbus operations SAS, France Matthieu Martel - University of Perpignan, France

Most of safety-critical embedded software, such as fly-by-wire control programs, performs a lot of floating-point computations. High level specifications are expressed in a formal model edited manually in SCADE through a graphical interface. It generally handles numerical variables and constants as if they were ideal reals. This work, for the purpose of numerical accuracy analysis, presents a new version of an Automatic Code Generator (ACG). This tool transforms high-level models into C codes and performs static computations by using mutiple-precision arithmetic. An accuracy analysis on numerical constant values is presented in a case study.

We.2.C.215:15add We.2.C.2 to agenda

Download We.2.C.2

CompCert – A Formally Verified Optimizing Compiler

Xavier Leroy - Inria Paris-Rocquencourt, France Sandrine Blazy - University of Rennes 1 - IRISA, France Daniel Kästner - AbsInt GmbH, Germany Bernhard Schommer - AbsInt GmbH, Germany Markus Pister - AbsInt GmbH, Germany Christian Ferdinand - AbsInt GmbH, Germany

CompCert is the first commercially available optimizing compiler that is formally verified, using machineassisted mathematical proofs, to be exempt from miscompilation. The executable code it produces is proved to behave exactly as specified by the semantics of the source C program. This article gives an overview of the design of CompCert and its proof concept and then focuses on aspects relevant for industrial application. We briefly summarize practical experience and give an overview of recent CompCert development aiming at industrial usage. CompCert’s intended use is the compilation of life-critical and mission-critical software meeting high levels of assurance. In this context tool qualification is of paramount importance. We summarize the confidence argument of CompCert and give an overview of relevant qualification strategies.

We.2.C.315:45add We.2.C.3 to agenda

Download We.2.C.3

Integration of Polychrony and QGen Model Compiler

Christophe Junke - INRIA Rennes Bretagne Atlantique, France Jean-Pierre Talpin - INRIA Rennes Bretagne Atlantique, France Loic Besnard - INRIA Rennes Bretagne Atlantique, France Thierry Gautier - INRIA Rennes Bretagne Atlantique, France

We present the recent development of a two-way translation tool between the synchronous Signal language and QGen's intermediate language. We show an application of model transformation and distributed code-generation based on an industrial use-case. We also discuss our contributions to the development and verificaton of QGen compiler as well as to the Polychrony toolset.

We.2.D.114:45add We.2.D.1 to agenda

Download We.2.D.1

Lean Model-Driven Development through Model-Interpretation: the CPAL design flow

Nicolas Navet - University of Luxembourg, Luxembourg Loïc Fejoz - RealTime-at-Work, France Lionel Havet - RealTime-at-Work, France Sebastian Altmeyer - University of Luxembourg, Luxembourg

We introduce a novel Model-Driven Development (MDD) flow which aims at more simplicity, more intuitive programming, quicker turnaround time and real-time predictability by leveraging the use of model-interpretation and providing the language abstractions needed to argue about the timing correctness on a high-level. The MDD flow is built around a language called the Cyber-Physical Action Language (CPAL). CPAL serves to describe both the functional behaviour of activities (i.e., the code of the function itself) as well as the functional architecture of the system (i.e., the set of functions, how they are activated, and the data flows among the functions). CPAL is meant to support two use-cases: • A design space exploration platform for CPS with main features being currently the formal description, the edition, graphical representation and simulation of CPS models. • A development and execution platform: the vision behind CPAL is that programs can be executed and verified in simulation mode on a workstation and the exact same code can be later run on an embedded board with the same run-time timing behaviour. The second use case targets embedded domains where a reduced time-to-market compensates for performance loss due to interpretation (versus compiled code).

We.2.D.215:15add We.2.D.2 to agenda

Download We.2.D.2

Making Modeling Assumptions an Explicit Part of Real-Time Systems Models

Pierre de Saqui-Sannes - ISAE, Université de Toulouse, France Ludovic Apvrille - Telecom ParisTech, France

Modeling is an intellectual process that consists in making abstractions. A model conveys a point of view of one system in order to assist a designer in his or her attempt to master the complexity of the system. The statement particularly applies to real-time systems that capture complex problems in terms of parallelism, synchronization, distribution and time constraints. Making abstractions implies making assumptions. In other words, a model works for a precise set of assumptions. For instance, a pressure controller model may be valid under the assumption the pressure sensor it is connected to never fails. Such an information is important to share the model with other people and to make the model easy to understand. Whether the importance of assumptions has regularly been acknowledged in the literature, the inclusion of modeling assumptions into models has not been formally proposed and discussed. In the paper, we conversely support the idea of making assumptions an explicit part of the model and we insist on the importance of assumptions in incremental modeling processes. We also consider that modeling assumptions play a key role in incremental modeling. Therefore, the approach of "versioning" discussed in the paper make it possible to take the way assumptions evolve into account (throughout the entire modeling process). The first part of the paper gives general principles and proposes a meta-model that allow including assumptions in a diagrammatic shape that may accompany a broad variety of models. Then, we show how to add modeling assumptions to real-time systems models expressed in SysML and we implement the approach in the TTool tool. An existing UAV platform, aiming at autonomously navigating in buildings, serves as a case study.

We.2.D.315:45add We.2.D.3 to agenda

Download We.2.D.3

An Architecture-Led Safety Analysis Method

Peter Feiler - Software Engineering Institute, United States of America David Gluch - Software Engineering Institute, United States of America John Mcgregor - Clemson University, United States of America

Safety critical systems require specific development and evaluation activities in the Software Development Life Cycle (SDLC) to ensure that the product is safe. Some of these activities are aggregated into comprehensive safety engineering practices, which are standardized within an industry. The objective of our research is to create a new safety engineering practice that utilizes a fault identification taxonomy and a model-based architecture representation of the system and its operational context. Our practice combines features of several existing safety engineering, model-based requirements analysis, and architecture design practices. It incorporates development and analysis of at least a partial architecture model using notations such as the Architecture Analysis and Design Language (AADL). The resulting practice has been embodied in the Open Source Architectural Tool Environment (OSATE) and piloted on an industrial strength example. The practice operates in coordination with the requirements definition and initial architecture design activities in an iterative, incremental development approach. Using architecture information and a fault taxonomy to inform safety analysis practices leads to an incremental safety-guided engineering practice.