TEC-ED & TEC-SW Final Presentation Days 2014 May

21 May 2014, 08:30 → 22 May 2014, 18:30 CET

Einstein (ESA/ESTEC)

The Software Systems Division (TEC-SW) and Data Systems Division (TEC-ED) Final Presentation Days are scheduled on Wednesday 21 May and Thursday 22 May in conference room Einstein (ESA/ESTEC, The Netherlands)

All material presented at the workshop must, before submission, be cleared of any restrictions preventing it from being published on this web-site.

Wednesday 21 May

08:30 → 08:50 Registration

Speaker: Kathleen Gerlo (ESA/ESTEC - Software Systems Division)

08:50 → 09:00 Introduction

Speakers: Mr Kjeld Hjortnaes (ESA/ESTEC - Software Systems Division), Mr Philippe Armbruster (ESA/Data Systems Division)

Slides Introduction_to_Final_Presentation_Days.pdf

09:00 → 09:50 Wireless Passive Sensors for Monitoring Systems

Activity: ITI ESA TO: Mr. Jean-François Dufour - Data Systems Division This work is devoted to the feasibility study of a wireless sensing system, mainly based on passive surface acoustic wave (SAW) sensors, for remote measurement of temperature aboard space platforms. The use of passive sensors is particularly attractive since they need no battery and are robust in extreme environments, as they contain no active electronic circuits. The main objective of this study is the complete characterization of the wireless system environment, in order to determine the main fundamental limits of this technology from a communication theory point of view. Preliminary experimental measurements are used for both defining the main environment parameters, validating some of the theoretical limit computations and proving the space application feasibility.

Speaker: Mr Pier Giorgio Arpesi (Selex)

Slides Wireless_Passive_Sensors.pdf

09:50 → 10:40 Single Board Computer Core SBCC

Activity: GSTP ESA TO: Mr. Kostas Marinis - Data Systems Division RUAG Space is the major independent European supplier of Data Handling Systems (DHS) and On-Board Computers (OBC) for launchers, satellite platforms, payload control and similar equipment based on advanced computer technology. In order to remain competitive and to be able to provide the European space community with a high performance computer core, a need to integrate the processor, telemetry, telecommand and reconfiguration functions on the same board forming a Single Board Computer Core (SBCC) has been identified. The main enabler for the SBCC is the next generation system-on-chip. In the first phase of the activity an FPGA (Field Programmable Gate Array) prototype of this chip, called CREOLE (derived from the current generation chips CROME combined with the COLE) has been developed. The development has been divided into three separate phases, where the end result will be the CREOLE ASIC (Application Specific Integrated Circuit) and its corresponding software drivers that will be used for the next generation of highly integrated DHS and OBCs. This presentation will summarize phase 1 which was finished in early 2014. The CREOLE integrates all major functions of the COLE, CROME and HAMSTER chips that form the basis of the current generation computers form RUAG Space. Functions include a LEON fault tolerant processor, I/O controllers, telecommand decoder, telemetry encoder, reconfiguration controller and Mass memory controller needed to support many different applications. An FPGA breadboard called MFC (Multi-Functional Core) has been developed including the CREOLE FPGA. It is a high performance multi-functional board with many I/O options that makes it suitable for a large number of prototype developments. Software drivers for the MFC board have been developed, in line with the software drivers supplied with the current flight generation of computers from RUAG Space.

Speakers: Mr Martin Lindskog (RUAG Space), Mr Peter Sinander (RUAG Space)

Slides Single_Board_Computer_Core.pdf

10:40 → 11:00 Coffee Break

11:00 → 11:50 Partitioning and Maintenance of Flight Software in Integrated Modular Avionics for Space

Activity: GSTP ESA TO: Mr. Martin Hiller - Software Systems Division Led by the ESA/ESTEC IMA-SP program, this study – namely In-Flight Hosting of Prototype Applications (IHPA) project – presents an experiment of Flight Software partitioning in an Integrated Modular Avionics for Space (IMA-SP) system. This experiment also tackles the maintenance aspects of IMA-SP systems. The fundamental objective of this experiment is to demonstrate through a representative use case that the successful IMA concepts deployed in the civil aviation industry is also beneficial to Space Avionics and in particular to the OBSW developments and life-cycle. The main objectives are however to explore and to demonstrate approaches for software maintenance of an IMA-SP system. The presented case study is PROBA-2 Flight Software. The study addresses and discusses the following subjects: On-Board Software Maintenance in IMA-SP, boot strategy for Time and Space Partitioning, considerations about the ground segment related to On-Board Software Maintenance in IMA-SP, and architectural impacts of Time and Space Partitioning for PROBA software’s. In the field of embedded system, the term OBSW Maintenance (OBSM) basically consists in updating whole or parts of the system or application software or data. In an IMA-SP environment, it concerns the partitioning kernel as well as the system and application partitions. The goal is then to be able to update any individual partition independently of the others. Finally, this presentation shares the results and the achievements of the study and it appeals at further perspectives for IMA-SP and Time and Space Partitioning. Keywords: Time and Space Partitioning, Integrated Modular Avionics, Spacecraft, On-Board Software Maintenance, PROBA platform.

Speakers: Mr Johan Hardy (SpaceBel), Mr Philippe Creten (SpaceBel)

Slides Partitioning_and_Maintenance_of_Flight_SW_in_....pdf

11:50 → 12:40 MultiIMA - Multi-Core in Integrated Modular Avionics

Activity: GSTP AO ESA TO: Mr. Martin Hiller - Software Systems Division Multi-core technologies are a natural trend towards fulfilling recent space applications requirements. This transition to multi-core is being driven by the growing demand for more autonomous missions and greater system integration. However, for embedded real-time systems to profit from the additional computation power introduced by multiprocessor and multi-core architectures, another paradigmatic change is required. This time, in the way the software is developed and integrated. Time-critical tasks need to be redesigned to account for parallel flows of execution and therefore allow the mapping of such flows through the set of processors. Furthermore, new classes of software failures are bound to appear and move from a mere theoretical possibility to actual systems crashes. To enable the use of multi-core technologies in the safety critical domain, guarantees against such failures must be introduced. Time and Space Partitioning is a promising solution to bridge the gap between safety critical application and multi-core technologies. In MultIMA, we identify and address the challenges and opportunities met when using multi-core technologies to support safety critical real-time applications. This assessment is used as an input for the design of the multicore versions of the AIR ARINC 653 operating system and of the SIMA ARINC 653 simulator. Finally, the challenges faced during the implementation of these multi-core versions are presented.

Speaker: Mr Claudio Silva (GMV Portugal)

Slides MultIMA.pdf

12:40 → 14:00 Lunch

14:00 → 14:50 Dynamic Translation Based On-Board Processor Emulator - QERx

Activity: GSTP ESA TO: Mr. Michael Schön - Software Systems Division Previously SCISYS presented QERx, an open source, faster than real time processor emulator for the ERC32 and LEON2 processor families. The latest evolution of QERx adds LEON3 to the suite of supported processors and greatly extends the feature set, most notably to include the emulation of multicore processors and an enriched cache model, whilst maintaining its faster than real time speed advantage. QERx has been validated using a SPARC compliance test suite, by integrating it into existing the Gaia Operational Simulator, the Earthcare STF, and through direct comparison against the hardware. QERx records a fourfold execution time improvement over the LEON3 hardware and a tenfold execution time improvement over TSIM.

Speaker: Mr Daniel Townson (SciSys UK)

Slides Dynamic_Translation_Based_On-Board_Processor_Emulator.pdf

14:50 → 15:20 OBC Simulator Architectures and Interfaces to System Test Benches / LeonSVF - Progress Presentation

Activity: GSTP & Strategic Initiative Denmark ESA TO: Mr. Mauro Caleno - Software Systems Division The goal of the project “OBC Simulator Architectures and Interfaces to System Test Benches” is to define architectures and interfaces for simulators of on-board computers based on Leon 2 and Leon 3 System on Chips (SoC). The primary output of the activity is a PCIe FPGA Leon Emulation Board (LEB) together with a number of reusable VHDL and software simulation components to tailor the FPGA to a specific target SoC. The LEB executes the actual Leon VHDL code thus enabling hardware-in-the-loop (HIL) emulation of Leon SoC’s. The LEB designed for Linux workstations and is controlled via an API compatible with TSIM by Aeroflex-Gaisler. The activity also has two secondary goals: exploring whether a model of a spacewire IP Core written by hardware engineers in SystemC/TLM could be reused in an OBC simulator (HW/SW engineering); and exploiting the SOIS layered architecture to skip simulation of and abstract from the OBC HW/SW ICD in an OBC simulator. This GSTP project started in March 2013 with Astrium SAS (France) and Terma AS (Denmark) and is currently under extension by CCN due to conclude with the Acceptance Review in September 2014. However the project has already achieved large part of its baseline goals, so its status is being presented at the FPD in May and at the DASIA. The LEB is an evolution of the earlier project “Leon Software Validation Facility” presented at DASIA 2008. The LEB enables connecting software simulations to addresses in the I/O space, internal APB and AHB AMBA spaces, managing simulation time events as well as transmitting and receiving entire spacewire packets when a SpW IP Core is embedded in the FPGA. The transfer of entire spacewire packets and connecting simulations to the internal APB and AHB AMBA busses are new function that enable HIL simulation of SoCs. Whenever simulation events trigger (I/O, AMBA, time or packet), the clock signal to the Leon IP Core is suspended to keep time representativity for the on-board software (OBSW) while the simulations execute. The project produced 3 configurations of the LEB for the Atmel AT697, for a generic Leon3 configuration and for a Leon3 configuration inspired from the SCOC3 SoC by Astrium and which embeds the Spacewire IP Cores. The LEB is the core of the OBC simulator integrated in the EagleEye ATB in the ESTEC avionics Lab via SMP2 interfaces.

Speaker: Mr Mauro Caleno (ESA/ESTEC - Software Systems Division)

Slides OBC_Simulator_Architectures_and_Interfaces.pdf

15:20 → 15:40 Coffee Break

15:40 → 16:30 Verification Models for Advanced Human-Automation Interaction (VASCO)

Activity: GSP ESA TOs: Ms. Maite Trujillo - Independent Safety Office & Mr. Yuri Yushtein - Software Systems Division HAI (Human Automation Interaction) is often a contributor to failures in complex systems. These failures are frequently caused by system interactions that were not anticipated by designers or analysts. While there are many useful analysis techniques that can be used to address these types of problems, none consider all of the possible interactions that can occur and can thus miss critical system conditions. Formal verification, and in particular model checking, is capable of such exhaustive analyses. In model checking, the behavior of a target system is represented in a formal model. Specification properties, which describe either desirable or undesirable behavior of the system, are constructed for this model. A model checker then proves (formally verifies) whether or not the model adheres to the specification by automatically searching through the model’s entire state space. One approach for using formal method to evaluate HAI focuses on including models of human behavior in the formal system model so that the impact of human behavior on system safety can be evaluated with a model checker. The presented project extended this method and evaluated it by using it to analyze the HAI of two realistic, aerospace test cases. EOFM (Enhanced Operator Function Model) is an XML-based language for modeling human task analytic behavior that can be evaluated with formal methods. An automated translator is available that is capable of representing the human behavior captured in an EOFM in the input language of a model checker (SAL; Symbolic Analysis Library) so that it can be included in a larger formal system model. The EOFM to SAL translator also supports two different types of erroneous behavior generation that enables analysts to optionally include human errors in an EOFM’s formal model representation. Collectively, these features allow analysts to use model checking to evaluate whether or not a system satisfies safety properties with both normative and potentially unanticipated erroneous human behavior. Previous work on EOFM required analysts to manually formulate the specification properties they intended to check. Such a practice can be prone to analyst error and oversight. Thus, in the work developed for this project, EOFM was extended to automatically generate specification properties capable of evaluating a system’s HAI, giving analyst a means of potentially finding unanticipated HAI problems. The EOFM-supported methodology was evaluated in two test cases, a satellite ground station control system and an unmanned air vehicle (UAV) ground control system. Results from the evaluation show that the methodology allows normative representations of human-interactive systems to be modeled and formally verified against manually created safety specifications. The method also enables the generation of specification properties from task models, which are capable of detecting potentially unanticipated problematic HAI conditions. Finally, it supports the inclusion of generated erroneous behaviors that can be used to evaluate the robustness of the system’s HAI and the system’s safety.

Speaker: Mr R. van Paassen (TU Delft)

Slides Verification_Models_for_Advanced_Human-Automation_Interaction.pdf

16:30 → 17:20 RTEMS Leon Upgrade

Activity: GSTP ESA TO: Mr. Christophe Honvault - Software Systems Division In the frame of the General Support Technology Programme, EDISOFT executed the activity named On Board operating system Upgrade for LEON, contract number 4000103825. The Kick-Off of RTEMS LEON Upgrade was performed in the 9th February 2012 and ended on 31st March 2014. The following activities have been achieved during the study. • RTEMS was enhanced to provide means to store inside RTEMS the fatal and non-fatal error messages with the file and line of error occurrence. The mechanism used has two distinct ring buffers, one for fatal error messages and another to non-fatal error messages, with the capacity of 100 and 200 messages, respectively. RTEMS is now capable of storing internal error messages and provides a similar method for the application to store and report fatal and non-fatal errors. • RTEMS Rate Monotonic Manager was enhanced to include the definition of the deadline concept. RTEMS is now able of detecting and signalling the periodic tasks deadline misses and of measuring execution time of periodic tasks. • RTEMS thread dispatch was improved to detect task stack overflow and underflow. The mechanism used is based in an insertion of 2 unsigned 32-bits integers with a special “watermark” (0xAAAAAAAA and 0x77777777) in the stack header and footer. Within the thread dispatch, both stack footer and header are compared with the predefined “watermark” to detect stack overflow and underflow. • RTEMS now includes an API to mask and unmask a specific interrupt in the hardware. • Binary semaphores with priority inheritance and ceiling are now safer to be used. RTEMS currently does not allow that a task that owns semaphores having priority inheritance or priority ceiling protocols to be suspended, to change the task mode to non-preemptible, to change priority, to be blocked in calls with the exception of obtaining semaphores with priority inheritance and ceiling, respectively, and to mix semaphores with different priority protocols. • Additionally, the removal of the dynamic memory allocation in the RTEMS initialization was performed. Although it was detected an improvement in some RTEMS directives, the modification introduced a significant increase in memory occupancy of applications, limited the tasks stack to 8Kbytes and obliged the use of floating point (CPU_HARDWARE_FP) in a task. • Several combinations of compilers, linkers and assemblers were used with RTEMS. The conclusions taken in the execution of this task, based on the measurements taken in the CPU Occupancy, Timing Report and Memory Report for the different toolchains, optimizations and hard-float flag, were to maintain the RTEMS Improvement original toolchain (GCC 4.2.1 and Binutils 2.18) in the development of RTEMS LEON Upgrade project. The modifications to RTEMS that could lead to a significant loss of product history were not introduced in the RTEMS Improvement main stream but kept in a specific configuration controlled branch. The RTEMS Improvement, implementing now the RTEMS LEON Upgrade results, is currently being used in several ESA space missions, including Galileo FOC, Solar Orbiter, IXV, IMA, smallGEO, Sentinel2, MTG and EarthCare.

Speaker: Mr Helder Silva (Edisoft)

Slides RTEMS_Leon_Upgrade.pdf

Thursday 22 May

08:30 → 08:50 Registration

Speaker: Kathleen Gerlo (ESTEC - TEC-SW)

08:50 → 09:00 Introduction

Speakers: Mr Kjeld Hjortnaes (ESA/ESTEC - Software Systems Division), Mr Philippe Armbruster (ESA/Data Systems Division)

Slides Introduction_to_Final_Presentation_Days.pdf

09:00 → 09:50 Avionics Architecture Modelling Language

Activity: TRP ESA TO: Mr. Christophe Honvault - Software Systems Divisions The ESA AAML (Avionics Architecture Modelling Language) study, led by GMV and with the participation of TAS-F, aimed at advancing the avionics engineering practices towards a model-based approach by identifying and prioritizing the analyses of interest to be performed based on an avionics architecture model, specifying the modelling language features necessary to support those analyses, and prototyping a software tool to demonstrate the automation of the analyses. In the AAML study a set of relevant avionics analyses, mapped to the main satellite functions, were identified. In order to support modelling and analysis of the avionics system, a process based on three levels of definition was specified: 1) The avionics functional definition, used to design the avionics system as a set of avionics functions that communicate each other exchanging data. 2) The avionics logical architecture definition, that consists of a representation of how the system will be logically structured so as to fulfil the requirements and expectations of the users. 3) The avionics physical architecture definition, which comprises an allocation of logical components to physical components and the consolidation of the interfaces between components in their final form. The three previous levels are complemented by an orthogonal one where the corresponding non-functional properties are specified. This process provides the means to manage the different phases of conception and implementation of the avionics system as a sequence of subsequent refinements of the avionics definition. The most noteworthy characteristics of the AAML modelling language are: • The avionics analyses are performed based on the information extracted from the AAML model entities. This way, the model represents a single source of input for the various analyses, guaranteeing overall consistency. • The language supports most of the developments across the different project phases and allows expressing the concepts of the avionics architecture in the model, keeping the best possible compromise between abstraction and precision. • The language also supports the possibility of first providing a coarse-grained specification of the model entities and their non-functional properties, which can then be refined to introduce more details in the suitable consecutive project phase. This allows the user to perform an early coarse-grained analysis to obtain an initial set of analyses results, which is of great value for the so called “design space exploration”. • The language accommodates a component-based design to allow developing a common library of COTS models for various architectural elements (e.g., buses, devices). During the study an implementation of the Avionics Architecture Modelling Language and a sub-set of the relevant avionics analyses selected (in particular, the bus load and data latency analysis, the commandability and observability analysis and the on-board functions and performance analysis) was developed. Additionally, a prototype tool was developed to conduct the system avionics definition process, to support the model definition and to execute the analyses. This prototype implementation was evaluated and tested by means of an use-case, based on the ESA’s Sentinel-3 satellite, consisting of an avionics architecture model developed using the AAML modelling language.

Speaker: Ms Elena Salazar (GMV)

Slides AAML_Study.pdf

09:50 → 10:40 The Free SDL State Machine Editor in TASTE

Activity: Lab Investment ESA TO: Maxime Perrotin - Software Systems Division The Specification and Description Language (SDL) is an international standard designed to describe communicating systems in an unambiguous way. The language includes high level graphical view as well as an action language and a semantic of execution. That allows to describe with the required level of detail the dynamic behaviour of a model, leaving out of the description any ambiguity. Native support of ASN.1 data types in SDL allows to share data description with other types of models, and guarantees static compatibility between the different elements. The use of SDL in TASTE to describe the behaviour of architectural elements raises the level of description to a new level. By extension it opens the door to simulation, verification, model checking, test, and test generation. Once the element is verified, the support of ASN.1 guarantees interoperability with the description of other elements. In this presentation, the SDL principles will be presented and illustrated with the new TASTE SDL editor. The set of related tools will then be presented and demonstrated including simulation, trace generation, test generation and model checking.

Speakers: Mr Emmanuel Gaudin (Pragmadev), Mr Eric Brunel (Pragmadev)

Slides SDL-FSM-Editor_ESA_20140522.pdf

10:40 → 11:00 Coffee Break

11:00 → 11:50 Formal Verification of the PolyORB-HI/C Middleware

Activity: Lab Investment ESA TO: Maxime Perrotin - Software Systems Division TASTE relies on code generation since its inception. As part of the TASTE process, code generation aims at automating tedious and error prone software engineering activities, so as to leverage models to synthesize the corresponding source-level artefacts. A current research challenge lies in the quality of the generated code. Peer-review is not sufficient: one needs to ensure preservation of semantics, absence of runtime errors, etc. ISAE led an effort to evaluate the applicability of theorem proving applied to the TASTE runtimes. The objective is to demonstrate formally the code generated, and its associated runtimes are free of typical runtime errors (buffer overflows, off-by-one, numerical errors). To do so, we rely on the ACSL annotations to define formal contracts associated to each function, and use Frama-C to show the implementation conforms to those formal contracts. At the end of the study, we could demonstrate a significant part of the TASTE runtime is free of runtime errors, increasing the confidence in the whole TASTE toolchain.

Speaker: Mr Jérôme Hugues (ISAE)

Slides Formal_Verification_of_the_PolyORB-HI_Middleware.pdf

11:50 → 12:40 Data Modelling with ASN.1 for Space Applications

Activity: Lab Investment ESA TO: Maxime Perrotin - Software Systems Division Abstract Syntax Notation One (ASN.1) is a well-established data modelling language, used every day in the code of hundreds of millions of embedded devices, to exchange message data in a performant and type-safe manner. It has been put to great use in the TASTE toolchain (http://taste.tuxfamily.org), a software engineering toolchain built under the supervision of ESA, where it is used as a baseline that drives a lot of functionality: (a) automatic integration of code generated by multiple modelling tools, through machine-generated ASN.1bridges (b) integration of HW components via automatically generated device drivers and VHDL/SystemC skeletons (c) automatic generation of TM/TC graphical user interfaces (d) machine-generated gateways for code written in any of a set of programming languages, including C/C++, SPARK/Ada, and Python (allowing for both statically-typed and dynamically-typed programming for TASTE systems) (e) automatically generated Interface Control Documents (ICDs), and many more (see the project wiki at http://taste.tuxfamily.org/wiki/index.php?title=Main_Page). TASTE is also using its own open-source ASN.1 compiler ( https://github.com/ttsiodras/asn1scc ) - written in an ML-derivative to specifically target embedded/space systems, and generating C/C++ as well as SPARK/Ada code - thus offering guarantees of code correctness for safety-critical systems. Our ASN.1 compiler is also generating complete test harnesses, that exercise the message data encoders and decoders to full statement coverage (100%), thus further increasing confidence in the generated code. In this presentation, we will focus on the latest additions to the TASTE toolchain, which include automatic mappers between ASN.1 and many publicly available database engines (PostgreSQL, MySQL, etc), which guarantee semantic consistency between instances of data models as they exist inside the applications' process spaces and as they are serialized inside databases.

Speaker: Mr Thanassis Tsiodras (Neuropublic)

Slides Data_Modelling_with_ASN.1.pdf

12:40 → 13:40 Lunch

13:40 → 14:30 FDIR Development and V&V Process

Activity: TRP ESA TO: Mr. Yuri Yushtein - Software Systems Division During FAME study, a FDIR Development and V&V Process has been defined and Failure and Anomaly Management Engineering (FAME) Environment has been developed to support the process. The FAME process is technology-independent and covers phases B, C, D. It is composed by the following activities: • Analyze User Requirements composed by the following tasks: • Define RAMS and Autonomy Requirements • Build Mission Phase/Spacecraft Operational Mode matrix • Define Partitioning/allocation composed by the following tasks: • Define Partitioning/allocation • Define Architecture • Define FDIR objectives and strategies composed by the following tasks: • Define FDIR objectives • Define FDIR strategies • Perform Timed Fault Propagation Analysis composed by the following tasks: • Specify TFPM • Analyze TFPM • Design composed by the following tasks: • Define detailed FDIR implementation • Define Detailed SW Specification • Define Detailed Spacecraft Data Base specification • Implement FDIR, V&V • Implement FDIR composed by the following tasks: • Validate and verify at Unit level • Validate and verify at Subsystem level • Validate and verify at System level The FAME environment is developed on top of, and extends, the COMPASS approach and toolset. The main ingredients and functionalities provided by the FAME environment are: • Modeling and verification framework inherited from COMPASS. This includes: use of formal models, written in the SLIM language, for nominal models, error models and FDIR models; model extension and fault injection to automatically extend the nominal models with error specification; definition of properties using property patterns; formal verification techniques, based on model checking, that cover a broad range of activities (functional verification, safety assessment, FDIR effectiveness analysis, performability analysis, etc.) • Definition of mission phases and operational modes, mission requirements and FDIR requirements, to specify the desired requirements on the FDIR • Modeling of fault propagation using TFPGs (Timed Failure Propagation Graphs) • Analyses of TFPGs o Behavioral validation, to check compliance of a TFPG with respect to a SLIM model o Effectiveness validation, to check suitability of a TFPG for implementing a diagnoser • Automatic synthesis of a TFPG from a model. (This feature is currently under implementation.) • Automated synthesis of an FDIR model o Synthesis of an FD model from a TFPG o Synthesis of an FR model, using conformant planning routines

Speakers: Mr A. Guiotto (TAS-I), Mr M. Bozzano (FBK)

Slides FAME.pdf

14:30 → 15:20 Requirements Definition for Onboard Data Systems for Life-Cycle Support and Management of End-to-End Security

Activity: TRP ESA TO: Mr. Marco Rovatti - Data Systems Division On-board TM/TC link security approaches currently implemented are reviewed in order to derive reference architectures featuring a security handling function. From this reference, the Security Engineering Process is analysed, i.e. a process that aims at protecting the system development, and not the system itself, against aggressions, and recommendations are proposed. These guidelines are complemented by detailed recommendations for the management of security services: functional (keys management) and non-functional (FDIR). The current security key management approaches are analysed, and possible short-term and longer-term improvements are proposed. Failures and attacks scenarios that can potentially compromise cryptographic capabilities of a satellite are analysed, identifying the most appropriate redundancy schemes and FDIR procedures and techniques for security units.

Speaker: Mr Jean-Paul Blanquart (Airbus Space and Defence)

Slides Requirements_Definition_for_Onboard_Data_Systems.pdf

15:20 → 15:40 Coffee

15:40 → 16:30 Verification Models for Advanced Human-Automation Interaction (VASCO)

Activity: TRP ESA TOs: Ms. Maite Trujillo - Independent Safety Office & Mr. Yuri Yushtein - Software Systems Division Considering human factor issues during system engineering supports the development of systems which compensate limitations and support strengths of human behaviour characteristics. The objective of the VASCO study is the development and validation of a methodology for formal verification of human-automation interaction in safety critical environments based on models of the overall human-automation system. The developed Formal Verification Methodology approaches human-automation interaction from a holistic cooperative system perspective where the object of design is a system of human agents (operators) and machine agents (automated systems) jointly performing a series of tasks (e.g., acquiring data, computing trajectories) aiming at satisfying higher level global tasks (e.g., controlling a spacecraft). This talk will present: 1) a database of analysis questions that address relevant aspects of human-automation interaction together with a catalogue of formal methods to approach these analysis questions, 2) the Formal Verification Methodology that is used to perform the verification of analysis questions, and 3) experiences and results of a case study used to validate the Formal Verification Methodology. As case study the air flow subsystem of the ISS Columbus module was chosen. The case study demonstrates that using formal verification techniques for the analysis of human-automation interaction is feasible. However, it revealed that a high modelling effort and utilization of standards for modelling is a prerequisite for an efficient integration of the Formal Verification Methodology in system design processes.

Speaker: Mr B. Wortelen (OFFIS)

Slides Verification_Models_for_Advanced_Human-Automation_Interaction.pdf

16:30 → 17:20 Adoption of Electronic Data Sheets and Device Virtualisation for Onboard Devices

Activity: TRP ESA TO : Mr. Chris Taylor - Data Systems Division The standardisation of the flight avionics infrastructure is progressing on many different fronts: · The SAVOIR initiative has developed a reference avionics architecture identifying individual building blocks · The CCSDS SOIS area has made significant progress in standardising the avionics communication services with many standards already under publication. · The ECSS has developed a number of data link protocols and device interface standards for avionics interconnection. The objective of the Electronic Data Sheets and Device Virtualisation activity was to demonstrate the use of electronic data sheets (EDS) in the above context to replace or supplement existing paper ICDs, and to employ the results to interfacing onboard sensors and actuators. We present the results of the following activities to meet this objective · Evaluate the general requirements on EDS technology, taking account of the reference and communication architectures including the relationship between the central processor and remote terminal units. · Analyse a series of paper based data sheets for a number of devices and define the required contents of an EDS for each of them. · Produce a draft XML schema and CCSDS specification for an EDS to define the functional and data link interface of onboard devices. · Demonstrate the feasibility and advantages of using EDS to specify the device-specific components of SOIS DVS and DAS via a practical demonstration based on actual data sheets using the RASTA test facility. · Provide feedback to the CCSDS SOIS area on progression to standardisation of EDS.

Speaker: Mr Stuart Fowell (SCISYS)

Slides Adoptions_of_EDS_and_Device_Virtualisation_for_Onboard_Devices.pdf