Thursday 1 February
Th.1.A.109:00add Th.1.A.1 to agenda
System Optimization: A Use Case in the Space Domain
The JUpiter ICy moons Explorer mission, JUICE, is the first large-class mission in the Cosmic Vision 2015-2025 program of the European Space Agency. Planned for launch in 2022 and arrival at Jupiter in 2030, it will spend at least three years making detailed observations of the biggest planet in the Solar System and three of its largest moons, Ganymede, Callisto and Europa. JUICE will carry a total of 11 scientific experiments (instruments) to study the gas giant planet and its large ocean-bearing moons. Each instrument will do a number of readings producing streams of data, which will be stored in the on-board mass storage and then transmitted to Earth via a specific protocol. In this paper we present a model-based approach for system optimization in terms of instrument parameters, mass storage configuration, and transmission band allocation. We use standard modeling and testing languages with formal semantics for describing the system and the different configuration scenarios, which are then executed in co-simulation mode to produce (1) very precise results and (2) graphical comparison of different configurations to help trade off.
Th.1.A.209:30add Th.1.A.2 to agenda
Launcher Sequential Analysis
This paper addresses the use of a set of techniques (domain specific language, constraint’s solving, model checking and simulation) to capture, implement and verify a launcher sequential in an industrial context. Instead of developing new techniques (which is more relevant to a research institute than to an industrial), this paper shows an example of activities and tools which allow engineers non-expert in these techniques taking benefits from them
Th.1.A.310:00add Th.1.A.3 to agenda
A Lightweight Meta-Model to Support Automotive Systems and Software Engineering
Modern automotive systems exhibit an increased level of automation as well as an ever-tighter integration with other vehicles, traffic infrastructure and cloud services. Novel features, such as advanced driver assistance systems or automated driving functions, drive the need to master the increased complexity of these systems and ensure consistency of the development along the entire product life cycle. Model-based development (MBD) is still the most promising approach to tackle these issues and support development of system-wide features (such as safety and security). With MBD approaches, the model become the central role for analysis and construction of system under development and for information exchange between stakeholders. Unfortunately, many existing automotive meta-models are enormously complex and tedious to use in efficient manner. This is especially cumbersome in European R&D project cooperation, when different institutions with different field of expertise and diverse tool- and process- setups are required to work together. Therefore, this paper aims at improving the information interchange continuity of architectural designs from system development level to software development level with the elementary meta-model required to support systems and software engineering for embedded automotive systems. The presented UML model supports managing of development artifacts and seamless information interchange across tool boundaries to merge heterogeneous tools required for the development of automotive multi-core software
Th.1.B.109:00add Th.1.B.1 to agenda
Safe and Secure Autopilot Software for Drones
We are interested in the problem of providing safe and secure software for drones to make them as safe as airplanes. As there is no certification standard for most commercial drones that exist today, we have chosen the well-known DO-178C/ED-12C avionics standard as a framework to define a suitable formal development and verification process. Our process is based on this standard and its three supplements: DO-331/ED-218 (model based development), DO-332/ED-217 (object oriented technology) and DO-333/ED-216 (formal methods). Our process is an original adaptation of the usual V-cycle based avionics processes to an iterative and incremental environment, where development and verification are performed in short increments. In this paper, we describe how we achieve that in practice and discuss in more details the integration of the formal methods supplement.
Th.1.B.209:30add Th.1.B.2 to agenda
Autonomous and connected vehicles: Collaboration of Aeronautic and Automotive industries to face the huge challenges for safe and secure embedded systems.
Facing the challenge of the development of safety system for autonomous and connected vehicles, the close collaboration of different partners from aeronautic and automotive fields is a key. By merging the competences and different technological cultures, each partner will take advantages in terms of technical and economical performances. To promote this close collaboration of all the players in Systems of Transportation Autonomous and Connected, Aerospace Valley is setting up a collaborative project (STAC).
Th.1.B.310:00add Th.1.B.3 to agenda
Securing the Connected Car : Application Code Matters
The development of embedded software for automotive applications has seen dramatic changes in recent years. Difficulties with uncontrolled, software induced acceleration in Toyota’s Prius models and surrounding legal issues. The rise of ISO 26262 and the disruption to development practices in its wake. A near exponential rise in embedded software content, and corresponding increases in software engineering complexity. And now, the “connected car” is falling under the spotlight with its vulnerability to attack from malicious hackers being demonstrated in models from a range of manufacturers. This will outline the relationship between automotive software systems architecture, domain separation, and application software. It will assert that no single technology amongst these offers a “silver bullet” to guarantee security, and that no connected system is ever going to be both useful and absolutely impenetrable. It makes sense to protect it proportionately to the level of risk involved if it were to be compromised, and that means applying multiple levels of security so that if one level fails, others are standing guard.
Th.1.C.109:00add Th.1.C.1 to agenda
Evaluation of DREAMS resource management solutions on a mixed-critical demonstrator
The paper describes the resource management developed within the DREAMS middleware and how it is able to support core failures and temporal overload situations. Those capabilities are then highlighted and assessed in the industrial mixed-critical demonstrator of the project.
Th.1.C.209:30add Th.1.C.2 to agenda
BB-RTE: a Budget-Based RunTime Engine for Mixed and Safety Critical Systems
The safety critical industry is considering a shift from single-core COTS to multi-core COTS processor for safety and time critical computers in order to maximize performance while reducing costs. In a domain where time predictability is a major concern due to the regulation standards, multi-core processors are introducing new sources of time variations due to the electronic competition when the software is accessing shared hardware resources, and characterized by timing interference. The solutions proposed in the literature to deal with timing interference are all proposing a trade-off between performance efficiency, time predictability and intrusiveness in the software. Especially, none of them is able to fully exploit the multi-core efficiency while allowing untouched, already-certified legacy software to run. In this paper, we introduce and evaluate BB-RTE, a Budget-Based RunTime Engine for Mixed and Safety Critical Systems, that especially focuses on mixed critical systems. BB-RTE guarantees the deadline of high-critical tasks 1) by computing for each shared hardware resource a budget in terms of extra accesses that the critical tasks can support before their runtime is significantly impacted. 2) by temporarily suspending low-critical tasks at runtime once this budget as been consumed.
Th.1.C.310:00add Th.1.C.3 to agenda
ESPRIT: Overview of the Vehicles Road-Train Real-Time Architecture
This paper deals with the communication and real-time architecture of an innovative articulated vehicle, coupled with up to seven other similar vehicles to form a road-train. The controller device was chosen powerful and flexible enough to prototype an innovative system of vehicles able to reconfigure themselves after a coupling or uncoupling process. Automotive industry standards are considered in order to benefit from existing systems. Implementation on real vehicles demonstrates performances and robustness in scenario conditions.
Th.1.D.109:00add Th.1.D.1 to agenda
Application of a Hybrid Navigation System for an Autonomous Space Air-Launched Vehicle
ALTAIR is a European Commission Horizon 2020 project that proposes a space launch system composed of an autonomous aircraft-rocket assembly, dedicated to the market share of small satellites (50-150 kg) in Low Earth Orbit. The rocket, or Space Launch Vehicle (SLV), comprises a cost-effective lightweight navigation system that fuses Global Navigation Satellite System (GNSS) data and readings from an Inertial Measurement Unit (IMU). The combination of these two technologies allows for a significant cut of the system mass budget with respect to traditional inertial-only navigation systems, without consequential accuracy loss. Additionally, ALTAIR embeds the alignment process on-board the SLV, which is performed during captive flight. Transferring this task to after take-off significantly simplifies ground operations in terms of both time and safety, hence further decreasing the cost of each launch campaign. This paper is divided into two parts: navigation performance assessment and its application for autonomous on-board safety algorithms. First, it presents the sensor fusion algorithm used to hybridize GNSS and IMU during the SLV free flight, including the captive alignment process. It describes a loosely coupled architecture of the hybrid navigation system, which combines a profile-free alignment with a profile-based GNSS/IMU data fusion. It then analyses the performance of this implementation that uses the Indirect (error-based) and Extended Kalman filters. Second, it evaluates the impact of sensor fusion on the safety algorithms that assess the nominal launcher state and engine failure free-fall scenario. Results show that hybrid navigation can be used to maintain a bounded error navigation solution throughout the in-flight initialization, the alignment manoeuvre and the free fall before ignition. Furthermore, transfer-alignment previous to SLV release prevents transient errors during the most critical initial seconds of free flight.
Th.1.D.209:30add Th.1.D.2 to agenda
Autonomous Detect & Avoid
The research department of the firm AKKA technologies, named AKKA research, is working on the development of an Unmanned Aerial Vehicle (UAV) for civil aviation. This project is called OMEGA and in this abstract we are going to present the actual state of the development, particularly the “detect and avoid” part. A simulation approach (MATLAB/Simulink environment) is used in order to test digitally avoidance algorithms before flight tests. Flight simulator software has been created. It embeds flight path monitoring, reference trajectory generation and trajectory tracking for an airship model.
Th.1.D.310:00add Th.1.D.3 to agenda
3D scanner positioning for aircraft surface inspection
The French Air-Cobot project aims at improving preflight maintenance as well as providing a traceability of the performed checks. A collaborative mobile robot has been built in order to carry out those tasks. The robot is able to navigate autonomously around the aircraft and perform non-destructive testing thanks to several sensors. More precisely, in this paper we focus on how to obtain a correct position of the 3D scanner fixed on a scissor with respect to the aircraft. It acquires 3D data which is analyzed to process surface inspection. The functional safety of the scissor is based on automatic visual checking of some cues. The full process demonstrates the feasibility of integrating 3D sensor on a mobile platform in safe conditions.
Th.PO.111:45add Th.PO.1 to agenda
Situation Awareness for Collaborative Robotics in Manufacturing Applications, Feasibility Study
Smart factories could significantly improve operators conditions of work in the manufacturing industry. They involve the collaboration without fences of robots and humans, whose safety needs to be ensured. To handle the safety issues, numerous systems propose standard solutions such as reducing the robot’s execution speed or interrupting its task for the humanrobot collision avoidance case. However, these actions do not take into account the dynamics of the environment to offer adapted and human-like behaviours. This paper proposes an approach based on Endsley’s model of Situation Awareness to predict a hazard, warn the operator and revise the robot’s task according to the context. The feasibility of the method was demonstrated through its application to a collision use case.
Th.PO.211:50add Th.PO.2 to agenda
Overview of the HEAA method defined by Airbus for Alarm design (Human Errors Analysis which concentrates on Alarm titles and their procedures)
Alarms are useful information given to flight crews in case of abnormal situations. In such specific contexts, source of stress, alarms are necessary to make the pilots understand the situation and guide them to safely end the flight. As stated in the AMC CS25.1302 (Acceptable Means of Compliance to the Human Factors Certification Specification), “even well trained, qualified, healthy, alert flight-crew members make error”. In accident we find errors with consequences, but in any routine flight we find errors without. In order to better guide pilots, Airbus is working on specifics methods to design alarms at best. The robustness of these design methods is key, not letting the alarm design to the sole designer’s appreciation. For that, the definition of the alarms is done in two steps. The first step, is the design of the Human Machine Interface & Interaction concept. This step is based on usual Human Factors methods of design, evaluation and validation, driven by Human Factors criteria like task distribution, task chronology, interface cluttering, guidance after interruptions but also commands accessibility, gestural precision…. At the end of this step, the crew tasks, the interaction means, the types and categories of information to be displayed, the location of this information, their sequencing, their formats and the cockpit controls are defined. But alarms are also made of a lot of detailed texts. The purpose of the second step is to concentrate on the quality of these alarms texts in order to make them clear and unambiguous and so to minimize the likelihood for a human error to happen, knowing that in most cases, the pilot even well trained, will discover the alarm during the operational situation. Which kind of criteria do we need to use to drive the design and the assessment of all this detailed texts in order to reduce design choices that could contribute to errors? This paper explains how we proceed to find these criteria. The generic process which has been defined to get these criteria is set as a method and is called HEAA (Human Errors Analysis which concentrates on Alarm titles and their procedures). In order to clarify the scope, we start to present the corpus, through the description of a procedure, checklist, alarm, alert terms. To illustrate, the definition of the alarms we are talking about is: a set of information, which is activated either by systems or on purpose by pilots. This information is: -Title, summarizing the abnormal status of the aircraft -List of actions to be performed (displayed in a do-list format) -Impacted systems (called secondary failure) -Deferred/pending procedures (to be performed at a specific moment of the flight) or at any time -Status page (displayed on System Display which mainly lists inoperative systems, functions and equipment) This article presents first the objective of the work done and the problematic, a state of the art, then how we proceed to define the criteria to drive the design of alarm texts, the results and finally the limits of the method.
Th.PO.311:55add Th.PO.3 to agenda
The Certification Challenges of Connected and Autonomous Vehicles
In the context of connected cars, some technologies or approaches are unavoidable: data-centric and big data. AI/ML-based systems. cloud computing and agility. These points are not limited to connected cars, but are trends in all transportation fields at least. In this paper, we analyze the interest of these technologies. Then, we analyze that these techniques are not completely in phase with traditional ways of developing safety critical software because the standards used for this purpose do not rely fundamentally on the same approaches to develop software.
Th.PO.412:00add Th.PO.4 to agenda
SimfiaNeo, Complex Systems, yet Simple Safety
This paper presents SimfiaNeo, a new tool to support Model-Based Safety Assessment (MBSA), based on AltaRica. It improves user experience in comparison with existing AltaRica editors.
Th.PO.512:05add Th.PO.5 to agenda
Safety Analysis from System Design to System Simulation
Designing a complex system, especially when safety and performance are mandatory, requires cooperation between several engineering teams. We claim that each engineering activity performs better with the support of dedicated model-based tools. The question that raised immediately from the multiplicities of teams and tools is how can they cooperate, ensuring the consistency and efficiency required in all projects? The paper proposes a complete workflow supported by best-in-class tools from ANSYS: • medini analyze for system safety analysis • SCADE Architect for system design • SCADE Suite for embedded software development and V&V • Simplorer for system simulation The focus of the paper is on the workflow and how the models are exchanged to achieve the complete development of a system that must be safe, that includes embedded software code, and that must reach given performance requirements. The extended abstract summarizes the tools capabilities, and means of model exchanges between tools and teams. the final paper will demonstrate the complete workflow on an example.
Th.PO.612:10add Th.PO.6 to agenda
Early Timing, Schedulability and Performance Analysis of Embedded Electronics Architectures
Advanced model-centric engineering environments need to comply at the same time with domain specific modelling paradigms for the end user and with specialised languages required by high value added analysis tools. Frequently, this is achieved by interconnecting existing modelling and model processing tools to minimize development and maintenance costs while using the state-of-the-art solution for each link of the tool-chain. Even then it is difficult and time-consuming to achieve pre-implementation. This paper describes an example of such a heterogeneous coupling between a system engineering platform for embedded electronics (E/E) architectures and a software architecture timing analysis framework.
Th.PO.712:15add Th.PO.7 to agenda
Automatic Parallelization from Lustre Models in Avionics
This poster presents ongoing research on automatic generation and execution of embedded parallel C code. We target safety-critical avionics programs specified in the synchronous language Lustre. The work described is being done in the context of the ITEA 3 project ASSUME (September 2015 - August 2018). ASSUME focuses mainly on embedded software engineering for multi-/many-core platforms. Both synthesis, e.g., automatic code generation, and verification, e.g., static analysis, of programs are addressed in the project. ASSUME is driven by the use cases of its industrial partners. One of these use cases consists in the parallelization of an avionics application comprising about 5500 Lustre nodes. After an overview of the ASSUME project, both parallel code generation and execution on a many-core platform will be presented and demonstrated.
Th.PO.812:20add Th.PO.8 to agenda
SQUORE as a Software Qualimetry solution at Continental PES
Managing extensive software projects requires managing on multiple levels, from intrinsic quality to complexity or test completeness. As these heterogeneous data originate from multiple tools in the course of a software project lifecycle, an industrial solution must be able to process them, in order to provide monitoring and decision-making assistance. This short paper illustrates how the SQUORE tool, having been applied to fields such as Aerospace, Avionics or Energy, has been integrated at Continental PES, as a Software solution.
Th.PO.912:25add Th.PO.9 to agenda
Software Quality Assurance Dashboard for Renault Software Robustness plan with SQUORE tool
Software is becoming one of the main challenge of the vehicle development process. To boost the Renault/Nissan embedded software transformation, a Software Robustness Breakthrough Plan was launched from 2015, with 6 levers of actions. Lever n°5 addresses Software Quality Assurance (SW QA). One of the main action of this lever is to gather and calculate the SW QA key performance indicators (KPI) within the Software Qualimetry project (SOQUAL). SOQUAL mission is to provide a software quality dashboard with relevant indicators. It includes source code and model analysis and other software metrics. SW QA KPI calculation was chosen as a use case to test a Qualimetry tool and to optimize the workload and the cost of Quality assurance activities. SQUORE  tool was selected for a quick development applied on one vehicle project (Start of production 2019). Renault has yet enlarging project scope: SW QA SQUORE tool is being deployed on several vehicle projects. Renault is also writing the specification to select a tool to implement a full Quality model: all software metrics (cost, model, code, schedule, anomalies, SW QA KPI…) should be gathered and aggregated to give the health status of software at vehicle project level, ECU level, function level..
Th.PO.1012:30add Th.PO.10 to agenda
From smartphones to automotive : Development of a generic SW framework to manage audio architecture scalability across embedded platforms
Spanning from smartphones and wearables, to automotive products, the Audio team, initially for Intel, and now for Groupe Renault, is in charge of supporting complex audio use cases across multiple architectures platforms and OSes. Starting since 2011 on Android, the team invested in designing a generic framework to abstract the characteristics of the target into configuration files. With full open source availability, the parameter framework has proven to enable full scalability of the audio SW solution, across platforms, products, and features, now being used in all OSes (Windows, Android, Yocto, Chrome, Ubuntu, etc…), for multiple types of industry (Mobile, Automotive, PC)
Th.PO.1112:35add Th.PO.11 to agenda
Consumer Electronics Processors for Critical Real-Time Systems: a (Failed) Practical Experience
The convergence between consumer electronics and critical real-time markets has increased the need for hardware platforms able to deliver high performance as well as high (sustainable) performance guarantees. Using the ARM big.LITTLE architecture as example of those platforms, in this paper we report our experience with one of its implementations (the Qualcomm SnapDragon 810 processor) to derive performance bounds with measurement-based techniques. Our theoretical and practical analysis reveals that some hardware features may not suit critical real-time needs, and restricted specifications and buggy documentation creates serious difficulties to derive WCET estimates for software running on this platform. From the lessons learned, we identify several main elements to consider to effectively consolidate the sustained performance needs between mainstream and critical real-time markets.
Th.PO.1212:40add Th.PO.12 to agenda
Exploring High-Level Synthesis Tools For Vehicle Perception Tasks
Building Intelligent Transportation Systems (ITS)requires the use of different types of sensors to improve the traffic safety and to ensure an efficient perception. These systems, integrate an increasing number of tasks and require a significant computing power. To develop a base computing platform that can be quickly modified and scaled to meet the cost and performance targets, FPGA platforms represent an appropriate solution that offers modular and scalable architecture. Moreover, with the complexity of applications and the delicacy of manual coding, the High-Level Synthesis (HLS) tools are used to accelerate the creation of the Register Transfer Level (RTL) designs. In this paper, we explore the HLS tools to generate the RTL designs for vehicle perception tasks based on the Zynq-7000 System On Chip (SoC).
Th.2.A.115:00add Th.2.A.1 to agenda
Lightweight Checkers in a New Light
The value of lightweight checkers, aka linters, for finding bugs in C or C++ programs has long been recognized. Their value for strongly typed languages like Ada or OCaml has not been so evident, as the compiler for these languages typically rules out most classes of bugs that C/C++ linters find, either by issuing errors for non-compliance with language rules, or more precise warnings thanks to the additional information available to the compiler. In particular, the availability of deep static analysis tools for these languages makes it uncertain that linters can be of interest too, as the power of their analysis fits between compilers and deep static analysis tools. We have investigated this question for the language Ada, and we have found that linters can play an important role for such languages as well, which is more focused than the role they traditionally play for weaker languages. Our findings are based on the creation of a set of linters for Ada that we applied to multiple industrial active codebases that we maintain at AdaCore. The results of these experiments were eye opening on the value of linters for stronger languages. In this article, we also describe the technology that allows the easy development and deployment of linters, as well as our strategy for adapting linters to the analysis context.
Th.2.A.215:30add Th.2.A.2 to agenda
Why Bother to Unit Test?
This paper addresses a question often posed by developers who are new to the concept of thorough testing: Why bother to unit test? The question is answered by adopting the position of devil's advocate, by presenting and examining some of the common arguments made against unit testing.
Th.2.B.115:00add Th.2.B.1 to agenda
Timed Formal Model and Verification of Satellite FDIR in Early Design Phase
In a previous work, we proposed an extension of the AltaRica language and tools to deal with the modelling and analysis of failures propagation in presence of timed and temporal constraints. This need is crucial in the space industry, where safety functionalities raise new challenges for the early validation of systems during model conception. This paper focuses on the application of our approach to the Fault Detection Isolation and Recovery (FDIR) mechanisms of the Attitude and Orbit Control System (AOCS) of a satellite. We discuss the modelling methodology applied to this system and its properties, as well as the tractability of the model-checking analysis.
Th.2.B.215:30add Th.2.B.2 to agenda
Model-Based Safety Analysis for co-assessment of operation and system safety: application to specific operations of unmanned aircraft
The safety assessment of specific operation of unmanned aircraft requires the characterization of the risks of the concept of operation and the verification that the remotely piloted aircraft system maintains the risk at an acceptable level within this CONOPS. This paper presents how Model Based Safety Analysis can help to achieve these two analysis steps. The approach is applied to a surveillance mission beyond visual line of sight at low level flight.Modelling concerns will be discussed in this context and performance of the presented tools will be highlighted.
Th.2.C.115:00add Th.2.C.1 to agenda
Computing Routes and Delay Bounds for the Network-on-Chip of the Kalray MPPA2 Processor
The Kalray MPPA2 manycore processor implements a clustered architecture, where clusters of cores share a local memory, and communicate through a RDMA-capable network-on-chip (NoC). This NoC has been designed to allow guaranteed delays by the adequate configuration of traffic limiters at ingress and the choice of routing. We first present the challenges related to the routing of concurrent flows and a strategy that solves it. Routing challenges include deadlock-free routing, which is always an issue on wormhole switching networks, fairness of resource allocation between flows, and ensuring the feed-forward property required by deterministic network calculus (DNC). Second, we present a linear formulation based on DNC for computing end-to-end delay bounds of concurrent feed-forward flows on the MPPA2 NoC. Finally, we compare this linear formulation to a classic formulation originally designed for the AFDX avionics networks.
Th.2.C.215:30add Th.2.C.2 to agenda
Using execution graphs to model a prefetch and write buffers and its application to the Bostan MPPA
Verifying the temporal properties of critical systems embedded in vehicles, like planes or cars, is crucial to avoid catastrophic issues. A key component of this verification is the Worst Case Execution Time (WCET) of the programs composing these systems. A common and sound approach to compute WCET is based on static analysis of the programs that requires, in turn, to precisely model the behavior and the timings of the hardware. Processor-specific features such as pipelines, caches, and buffers influence the hardware performances significantly. Hence taking processor features into account when estimating WCET is essential. Modeling the processor's features formally to ensure safe and accurate estimation is then a must. In this paper, we present the methodology applied to capture the behavior of prefetch and write buffers of the Kalray Bostan MPPA microprocessor, and to incorporate the established models with the Execution Graph (XG) to obtain WCET estimation. These analyses are then applied to the Malardalen benchmark suite and the experimentation results validate the feasibility of our approach.
Th.2.D.115:00add Th.2.D.1 to agenda
Full Virtualization of Renault's Engine Management Software and Application to System Development
Virtualization allows the simulation of automotive ECUs on a Windows PC executing in closed-loop with a vehicle simulation model. This approach enables to move certain development tasks from road or test rigs and HiL (Hardware in the loop) to PCs, where they can often be performed faster and cheaper. Renault has recently established a virtualization process for powertrain control software based on Simulink models. If the number of runnables exceeds threshold (about 1500) the execution of the virtual ECU is no longer straight forward and specific techniques are required. This paper describes the motivation behind a Simulink model based process, the virtualization process and applications of the resulting virtual ECUs.
Th.2.D.215:30add Th.2.D.2 to agenda
Model Quality Objectives for Embedded Software Development with MATLAB/Simulink
This paper presents standard quality objectives for models developed with Simulink® at different phases of the software development lifecycle. This standard, named Model Quality Objectives (MQO), has been defined by a group of leading actors from the automotive industry and MathWorks, the company that develops the MATLAB®, Simulink, and Polyspace® products. The purpose of this standard is to clarify and ease the collaboration between OEM and suppliers when sharing Simulink models in the context of embedded software development to drive the production of higher quality and integrity software.
Th.3.A.116:30add Th.3.A.1 to agenda
Interoperable Toolchain for Requirements-Driven Model-Based Development
This paper introduces a toolchain for requirements-driven model-based development of embedded software as used in the automotive industry. Development usually starts with textual functional requirements written in natural language. Verification of functional requirements required in safety critical systems needs traceability on system level and on implementation level. Therefore, the formalization of the provided textual requirements is of vital importance. This however is a challenging task in general, which we approach using an intuitive and graphical formalization language, namely simplified universal pattern. Having the requirements formalized, as a second step an analysis is done to ensure that the requirements are in a consistent state. This is important as within agile development, functionalities are evolving over time and textual requirements are continuously enhanced. To keep track of the implementation, an aggregation of model changes wrt, e.g., consistency, model test status, formal requirement coverage, or modeling guideline conformance during project runtime is done, while all information is visualized inside a single dashboard. An expressive running example implemented as Simulink model will be used to show the formalization and verification workflow using the provided toolchain.
Th.3.A.217:00add Th.3.A.2 to agenda
Development and Verification of UML Architectures by Refinement and Extension Techniques
We have developed an incremental development framework which supports progressive constructions of UML state machines. This framework includes behavioral refinement and extension verifications. In this paper, we extend this framework to UML composite components in order to guide architecture modeling and verification. It consists of a set of construction techniques which assist the designer in two complementary ways: concerning behavioral aspects, the techniques are based on formal relations which determine if the new architectures are true refinement and/or extensions of the former ones. concerning structural aspects, the techniques contribute to the software engineering design principles separation of concerns, information hiding and hierarchical modeling. The paper presents some of these techniques and illustrates them through a case study.
Th.3.A.317:30add Th.3.A.3 to agenda
Temporal Properties in Component-Based Cyber-Physical Systems
Modern cyber-physical system are often responsible for safety critical control functions. The quality and performance of these function is directly linked to asserted realtime behavior. In the literature requirements on this behavior are considered exclusively in the context of central architectural decision making. This can be problematic because such systems can consist of a large number of reusable software components, supplied by different stakeholders that are executed on interconnected processing units. In this work, we present a novel approach to obtain temporal requirements for the design of cyber-physical systems in a more distributed way. The significant advantages are the following: First, our approach simplifies the transfer of assertions made during functional design to the system design process which is important when building systems from reusable components. Second, our approach enables us to consider important aspects of temporal properties in an automated form, that otherwise have to be addressed manually. We demonstrate the applicability of our approach using an automotive use case.
Th.3.B.116:30add Th.3.B.1 to agenda
Using Traffic Sequence Charts at the Development of HAVs
This paper proposes a visual, formal specification language for capturing such scenarios, and thus addresses key industrial needs for supporting scenario catalogue based acceptance testing for HAVs: 1. How can we at all capture the infinite number of possible traffic situations of an HAV in a finite catalogue with finitely represented scenarios? 2. How can we at the same time determine unambiguously whether a particular evolution of traffic situations is covered by a scenario? 3. How can we, thus, decide, whether the reaction of the vehicle-under-test in a given concrete traffic situations is compliant to the scenario catalogue (and thus derive test suites for acceptance testing from scenario catalogs)? 4. How can we assess, whether all possible traffic situations are covered by scenarios? This paper provides answers to challenges 1-3, and provides two necessarily incomplete, complementary proposals of how to deal with challenge 4. Challenge 1 is addressed by proposing a declarative specification language, where thus every individual chart determines via its formal semantics the infinite set of evolutions of an infinite set of initial traffic situations meeting the constraints on individual traffic situations and their evolution specified in a Traffic Sequence Chart (TSC). Each additional chart thus adds further constraints. TSCs observe entities defined in an ontology of the categories of all types of artifacts which must be observable in real traffic situations currently developed within the OpenSCENARIO initiative of OEMs and Tier1 suppliers. A formal dense time world model implements the entities and types, thereby capturing all relevant physical phenomena of the real world. These include as well environmental conditions, such as status of road surface, aquaplaning, lighting conditions, and weather conditions, all influencing the perception and maneuvering capabilities of a HAV. Formally, TSCs have the expressiveness of a first-order real-time temporal logic, where first-order atoms specify individual traffic situations.
Th.3.B.217:00add Th.3.B.2 to agenda
Pattern-based requirements development
In the recent years, several high level requirements languages have been proposed. Although these languages are close to natural language, thanks to the use of dedicated patterns [DAC99], a formal semantics is attached to them. In general, modal logics have been used to express the semantics of such languages as for instance, temporal logics: branching time, linear time, temporized or not. In this paper, we are interested by the preliminary steps of the development of safety critical systems. We investigate how patterns could be used in order to generate refinements automatically. One of our major concern is to produce Event-B machines such that the user can refine them further.
Th.3.B.317:30add Th.3.B.3 to agenda
Formal architecture modeling for documenting and assessing Aeronautics Maintenance: A case study
This paper is a case study that will illustrate what a dedicated formal specification can bring to a socio-technical system description and how it can take place. The illustration will use an ONERA specification language and tool and apply it on the domain of aeronautical maintenance that is being dealt with in the Clean Sky 2 European project ADVANCE-AIRMES. As opposed to informal modeling, formal specification will offer: (1) to automatically assess check some high level properties or indicators and hence compare candidate solutions, (2) to produce a standard documentation conforming for example to the NATO Architecture Framework (NAF), (3) to better support safety and security analysis.
Th.3.C.116:30add Th.3.C.1 to agenda
Model-Based Design, Analysis and Synthesis for TSP Multi-Core Space systems
Symmetric multiprocessing (SMP) and Time and Space Partitioning (TSP) are two complementary paradigms for the design of multi-core-based aerospace systems. They impose new steps in the development process: capturing complex con- figuration attributes, analyzing their correctness – in particular their predictability – while guaranteeing performance. In this context, model-based techniques provide a well-suited framework to design, analyze and automatically synthesize those systems. In this paper, we report on a set of extenstions of TASTE to support SMP and TSP-based multi-core platform. We first present the key architectural elements of these systems and then detail how these have been integrated as part of the code generation tool-chain. We then present experiments realized on two case studies and two hardware targets, both provided with the RTEMS operating system and XTRATUM hypervisor.
Th.3.C.217:00add Th.3.C.2 to agenda
A Model Based Safety Critical Flow for the AURIX Multi-core Platform
In this paper, we present a model based development flow for safety critical applications that target parallel execution on Infineon's latest generation AURIX multi-core chips. The flow is based on an extension of SCADE Suite, that generates parallel code from any legacy Scade application. SCADE Suite is a product line of the ANSYS Embedded software family of products and solutions that empowers users with a Model-Based Development Environment for critical embedded software.The generated parallel code is target independent, an integration step is performed to instantiate OS specific services like communication, synchronization or memory protection. An automated integration process has been developed for the PXROS-HR operating system. PXROS-HR, developed by HighTec EDV-Systeme, is a multicore real-time operating system designed for embedded safety-critical applications. PXROS-HR is able to take full advantage of AURIX performance and safety functionalities. SCADE Suite certified generated code embedded in PXROS-HR certified RTOS provide the streamlined answer to challenging development of critical multi-core embedded applications by enabling seamless automated flow from the application model down to executable binary running on a target embedded processor.
Th.3.C.317:30add Th.3.C.3 to agenda
A model based certification approach for multi/many-core embedded systems
This article presents the first year results of the PHYLOG project that aims at providing a model-based certification framework for aeronautics systems designers when developing multi/many-core-based architectures. After a brief reminder of the certification objectives, we present an overview of the PHYLOG approach. We then detail two points of the methodology: (1) a certification oriented meta-model for multi- and many-core platforms, and (2) an interference prediction method based on this meta-model. This method is then illustrated on a sub-part of the many-core Kalray MPPA R -256.
Th.3.D.116:30add Th.3.D.1 to agenda
Real time and interactive co-execution platform for the validation of embedded systems
The main objectives of this article are to enlighten the importance of early validation and virtual (or hybrid) co-execution in complex systems and to provide associated solution. First step is to define a common ontology as a high level conceptual organization of test based engineering and validation. As a second step, we introduce a real time and interactive co-execution platform that provides heterogeneous model integration, models validation and monitoring. We discuss about technical aspects of platform with emphasize on openness, independent and consistent integration, and system scalability. Then we analysis how such a unified testing system can be leveraged to better coordinate and optimize risk and reduce time to market for complex projects from different abstraction levels. Finally, we explain how real time and interactive co-execution may accelerate the integration tests and system validation in the context of multidisciplinary projects through a collaborative platform
Th.3.D.217:00add Th.3.D.2 to agenda
Coincidence Problem in CPS Simulations: the R-ROSACE Case Study
This paper presents ongoing work on the formalism of Cyber-Physical Systems (CPS) simulations. We focus on a distributed simulations architecture for CPS, where the running simulators exist in concurrent and sequential domains. This architecture of simulation allows the expression of structural and behavioral constraints on the simulation. We call scheduling of simulation The temporal organization of the simulators interconnection. In this paper we address in this paper the problem of the interconnected simulations representativity. To do so, we highlight the similarities and differences between task scheduling and simulation scheduling, then we discuss about constraints expressible over that simulation scheduling. Finally, we illustrate a constraint on simulation scheduling with an extension of the open source case study ROSACE, implemented with CERTI, a compliant High Level Architecture (HLA) RunTime Infrastructure (RTI). HLA is an IEEE standard for distributed simulation.
Th.3.D.317:30add Th.3.D.3 to agenda
Integrating AADL and FMI to Extend Virtual Integration Capability
Virtual Integration Capability is paramount to perform early validation of Cyber Physical Systems. The objective is to guide the systems engineer so as to ensure that the system under design meets multiple criteria through high-fidelity simulation. In this paper, we present an integration scheme that leverages the FMI (Functional Mock-Up interface) standard and the AADL architecture description language. Their combination allows for validation of systems combining embedded platform captured by the AADL, and FMI components that represent physical elements, either mechanical parts, or the environment. We present one approach, and demonstrator case studies.
Regular abstract and short paper submission (4 pages): June 18, 2017 extended to July, 9
September 22, 2017
Regular Paper for review (10 pages):
October 27, 2017
Final Paper submission deadline
(Short & Regular):November 24, 2017
SIEMENS - MENTOR GRAPHICS
Institute of Technology Antoine de Saint Exupéry
REGION OCCITANIE / PYRENEES - MEDITERRANEE