Towards Integration of Adaptability and Non-Intrusive Runtime Verification in Avionic Systems ∗ José Rufino jmrufino@ciencias.ulisboa.pt LaSIGE, Faculdade de Ciências, Universidade de Lisboa, Portugal ABSTRACT 1. INTRODUCTION AND MOTIVATION Unmanned autonomous systems (UAS) avionics call for ad- Avionic systems have strict safety and timeliness require- vanced computing system architectures fulfilling strict size, ments as well as strong size, weight and power consumption weight and power consumption (SWaP) requisites, decreas- (SWaP) constraints. Modern unmanned autonomous sys- ing the vehicle cost and ensuring the safety and timeliness of tems (UAS) avionics follow the civil aviation trend of tran- the system. The AIR (ARINC 653 in Space Real-Time Op- sitioning from federated architectures to Integrated Modular erating System) architecture defines a partitioned environ- Avionics (IMA) [1] and resort to the use of partitioning. ment for the development and execution of aerospace appli- cations, following the notion of time and space partitioning Partitioned architectures implement the logical separation (TSP), preserving application timing and safety requisites. of applications in criticality domains, named partitions, and allow hosting both avionic and payload functions in the same The plan for a UAS mission may vary with the passage of computational infrastructure, thus fulfilling both SWaP and time, according to its mode/phase of operation, and the safety/timeliness requirements [24]. The notion of temporal vehicle may be exposed to unpredictable (environmental) and spatial partitioning (TSP) implies that the execution of events and failures, calling for the advanced adaptability and functions in one partition does not affect other partitions’ reconfigurability features included in the AIR architecture. timeliness and that separated addressing spaces are assigned This paper explores the potential of non-intrusive runtime to different partitions [21]. The design and development of verification (RV) mechanisms, currently being included in AIR (ARINC 653 in Space Real-Time Operating System) AIR, to improve system safety and to decrease the com- has been motivated by the interest in applying TSP concepts putational cost of timeliness adaptability and of the corre- to the aerospace domain [20]. sponding overhead on the system. Usually, an UAS mission goes through multiple phases (e.g., launch, flight, approach, exploration). Adaptation to chang- Categories and Subject Descriptors ing temporal requirements throughout all the mission phases C.4 [Computer System Organisation]: [Fault tolerance]; is of great importance for a mission’s survival [23]. The de- C.3 [Special-Purpose and Application Based Systems]: sign of AIR Technology already includes mechanisms of sup- Real-time and embedded systems; D.4.7 [Operating sys- port for adaptation and reconfiguration. Nevertheless, given tems]: Organization and Design—Real-time systems and the high complexity of UAS functions, modern avionic sys- embedded systems tems may largely benefit from the verification in runtime that the system/mission specification is being fulfilled or Keywords that some deviation has just occurred. dependability, timeliness, adaptability, runtime verification, This paper addresses how fundamental timeliness adapta- time and space partitioning, integrated modular avionics. tion mechanisms can be combined with advanced runtime ∗This work was partially supported by FCT, through project verification (RV) capabilities in time- and space-partitioned PTDC/EEI-SCR/3200/2012 (READAPT) and through LaSIGE systems. To reduce the temporal overhead of such mech- Strategic Project PEst-OE/EEI/UI0408/2014. This work inte- anisms in the operation of onboard systems an innovative grates the activities of COST Action IC1402 - Runtime Verifica- non-intrusive design approach is followed. tion beyond Monitoring (ARVI). The paper is organized as follows. Section 2 introduces the AIR architecture for TSP systems. Section 3 details the AIR adaptability and reconfigurability capabilities. Section 4 de- scribes the non-intrusive RV features being introduced in the AIR architecture and Section 5 describes how to integrate them with AIR system adaptability and reconfigurability. Section 6 describes the related work and, finally, Section 7 EWiLi’15, October 8th, 2015, Amsterdam, The Netherlands. issues concluding remarks and future research directions. Copyright retained by the authors. Partition P1 Partition P2 Partition P3 ... Second hierarchy level Process Scheduler Process τ1,1 Process τ1,2 Process τ2,1 Process τ2,2 Process τ3,1 Process τ3,2 Tasks (processes) Process τ1,3 Process τ1,4 Process τ2,3 Process τ3,3 in partition P2 ... τ2,1 τ2,2 τ2,1 τ2,3 Native POS Native POS Native POS Process Scheduler Process Scheduler Process Scheduler 20 60 Mode-based selection PST1 PMK AIR PAL Process Deadline Violation Monitoring (Active) PST2 0 20 60 130 150 190 Partition Dispatcher Partition Scheduling Tables Schedule_id Schedule_id Schedule_id Major Time Frame (MTF) PST Schedule Schedule Schedule ChangeActions ChangeActions ChangeActions (Inactive) Schedule Schedule Schedule Partition P1 Partition P2 Partition P3 Partition Scheduler Mode-based Schedules PST3 (Inactive) First hierarchy level Partition Scheduler Figure 2: Two-level hierarchical scheduling with Figure 1: AIR architecture for TSP systems partition scheduling featuring mode-based schedules cording to a partition scheduling table (PST) repeating over 2. AIR TECHNOLOGY FOR TSP SYSTEMS a major time frame (MTF). The PST assigns execution time The AIR Technology evolved from a proof of feasibility for windows to partitions. Inside each partition’s time windows, adding ARINC 653 functional support to the Real-Time Ex- its processes compete for processing resources according to ecutive for Multiprocessor Systems (RTEMS) to a multi-OS the POS’s native process scheduler. (operating system) TSP architecture [20]. The AIR modular design aims at high levels of flexibility, hardware- and OS- independence, easy integration and independent component 2.3 Health monitoring and error handling verification, validation and certification. The AIR architecture incorporates Health Monitor (HM) functions that aim to contain faults within their domains of occurrence and to provide the corresponding error handling 2.1 System architecture capabilities. Support to these functions is spread throughout The AIR modular architecture is pictured in Figure 1. The virtually all of the AIR architectural components. AIR Partition Management Kernel (PMK) is the basis of a core software layer, enforcing robust TSP properties and The HM plays an important role in achieving system safety hosting crucial functionality such as partition scheduling and given it prevents/mitigates ill-effects of process and/or par- dispatching, low-level interrupt management, and interpar- tition level errors in the remaining partitions. The action tition communication support. Temporal partitioning en- to be performed in the event of an error is defined by the sures that the real-time requisites of the different functions application programmer through an appropriate error han- executing in each partition are guaranteed. Spatial parti- dler. This may comprise adaptability features such as the tioning relies on having dedicated addressing spaces for the redefinition of timing and control parameters or the issue functions executing on different partitions. of a different schedule request. If no handler is provided, a response action defined by the partition’s HM ARINC 653 Each partition can host a different OS (the partition operat- configuration table is executed, as shown in Figure 3. ing system, POS), which in turn can be either a real-time op- erating system (RTOS) or a generic non-real-time one. The Application EH: event handler AIR POS Adaptation Layer (PAL) encapsulates the POS Activate (event-driven) POS Process of each partition, providing an adequate POS-independent interface to the surrounding components. Exception! no no yes The Portable Application Executive (APEX) interface [22] Interrupt traps System level? EH defined? EH running? yes no yes provides a standard programming interface derived from the others yes ARINC 653 specification [1], with the possibility of being AIR PMK/POS interrupt handling Action defined? Ignore no Restart subsetted and/or adding specific functional extensions for AIR Health Monitor Default Action Shutdown certain partitions [19]. The organization of vehicle functions in different partitions Figure 3: Health monitoring requires interpartition communication facilities, since a func- The design of AIR allows HM handlers to simply replace tion hosted in a partition may need to exchange information existing exception handlers or to be added to existing ones, with other partitions. Interpartition communication consists in pre- and/or post-processing modes. of the authorized transfer of information between partitions without violating neither spatial separation constrains nor 3. ADAPTABILITY information security properties [21, 20, 5]. The adaptation to changing environmental or operating con- ditions is crucial for unmanned space and aerial missions 2.2 Two-level scheduling survivability, which can be significantly improved through The AIR technology employs a two-level scheduling scheme, software reconfigurability, as studied in [23]. as illustrated in Figure 2. The first level corresponds to par- tition scheduling and the second level to process scheduling. The design of AIR integrates special-purpose mechanisms Partitions are scheduled on a cyclic basis, through the parti- to address specific adaptation requirements, thoroughly de- tion scheduling and dispatching components (Figure 2), ac- scribed in [7] and summarised next. 3.1 Mode-based schedules The usage of reconfigurable logic supporting versatile plat- Timing requirements may change according to a mission’s form designs (e.g., soft-processors) enables innovative ap- phase since certain functions should only execute during cer- proaches to RV [17], herein explored in the context of TSP tain phases. The original ARINC 653 notion of a single fixed systems. An enhanced AIR architecture makes use of an PST [1], defined offline, is limited in terms of timeliness AIR Observer (AO) featuring: non-intrusiveness, meaning adaptability, as well as safety and fault-tolerance control, system operation is not adversely affected and code instru- and surely contributes to some degree of resource utilization mentation with RV probes is not required; configurable, be- waste. To address this primary limitation, the AIR design ing able to accommodate different event observations. incorporates the notion of mode-based partition schedules, inspired by the optional service defined within the scope of ARINC 653 Part 2 specification [2]. Bus Observer Interfaces Buses Instead of one fixed PST, the system can be configured with Time Base multiple PSTs, which may differ in terms of the MTF du- ration, of which partitions are scheduled, and of how much Mgmt. currentTicks Configuration processor time is assigned to them, as shown in Figure 2. Interface The system can then switch between these PSTs; selection of the active PST is performed through a service call issued System Clock by an authorized and/or dedicated partition. To avoid vio- lating temporal requirements, a PST switch request is only Figure 4: AIR Observer architecture effectively granted at the end of the ongoing MTF. The AO is plugged to the platform where the AIR software Hosting multiple PSTs aboard autonomous vehicles opens components execute, and comprises the modules depicted in room for the (self-)adaptability of unmanned missions, in Figure 4: Bus Interfaces, capturing all physical bus activity, function of passage of time and of changing environmen- such as bus transfers or interrupts; Management Interface, tal and operational conditions. Pre-generation of differ- enabling AO configuration; Configuration, storing the pat- ent partition schedules can be aided by a tool that applies terns of the events to be detected; Observer, detecting events rules and formulas to the temporal requirements of pro- of interest based on the registered configurations. cesses/partitions, taking into account the functions’ needs in different anticipated conditions [20, 8]. Unforeseeable con- Though RV concepts can be applied to both time and space ditions can be handled thorough the mechanisms for remote partitioning, this paper is restricted to temporal issues. Thus, update of PSTs and onboard software described in [19]. it is assumed that a robust time base1 accounts for, in the AO hardware (Figure 4), the number of POS-level clock 3.2 Process deadline violation monitoring ticks elapsed so far, to which AIR components have access, During runtime execution, it may be the case that a process through the read only currentT icks variable/register. exceeds its deadline. In the AIR architecture, the PAL com- ponent monitors, at each POS clock tick, if some process in 5. INTEGRATING ADAPTABILITY AND the active partition has violated its deadline (Figure 2). In addition, it is also possible that a process exceeds its dead- NON-INTRUSIVE RUNTIME VERIFI- line while the partition in which it executes is inactive. This CATION violation will only be detected when the partition is being The integration of RV features in the AIR architecture uses dispatched, just before the PAL component invokes the POS a dual approach, as follows: process scheduler, as shown in the diagram of Figure 2. • operation enforced in hardware, either totally or with some degree of assistance from software components, The use of offline tools that verify the fulfilment of tim- being the runtime verification actions performed in ing requirements [20, 8], should rule out deadline violations software; due to faulty system planning (e.g., time windows not sat- isfying the partitions’ timing requirements). However, such • operation achieved through the execution of software tools cannot cope with process deadline violations caused by components, with runtime verification actions enforced a runtime malfunction, by transient overload (e. g., due to in hardware. abnormally high event occurrence rates), or by the underes- timation of a process’s worst case execution time (WCET) 5.1 Mode-based schedules at system configuration and integration time. In the generic and highly flexible AIR architecture design presented in [20], the handling of mode-based schedules is 4. MECHANISMS FOR NON-INTRUSIVE entirely integrated within a software-based AIR Partition RUNTIME VERIFICATION Scheduler, as illustrated in the diagram of Figure 2. Runtime verification (RV) obtains and analyses data from In a hardware-assisted approach, partition scheduling switch the execution of a system to detect and possibly react to decisions from the AO hardware are complemented with behaviours, either satisfying or violating the system speci- software RV and partition switch actions: when a partition fication. RV implies that small components, which are not part of the functional system, acting as observers, are added 1 The design and engineering AIR robust timers is out of the to monitor and assess the state of the system in runtime. scope of this paper. It will be addressed in a future work. Algorithm 1 AIR Partition Scheduler with Runtime Veri- Algorithm 2 AIR Partition Dispatcher fication featuring adaptation through mode-based schedules 1:  Entered from the AIR Partition Scheduler after partition switch 1:  Entered upon exception: partition preemption point detected actions 2:  Runtime verification actions 2: SaveContext(activePartition.context) 3: if schedules currentSchedule .table tableIterator .tick 6= 3: activePartition.lastTick ← currentTicks − 1 (currentTicks − lastScheduleSwitch) mod 4: elapsedTicks ← currentTicks − heirPartition.lastTick schedules currentSchedule .mtf then 5: activePartition ← heirPartition 4: HealthMonitor(activePartition) 6: ReplacePreemptionPoint(heirPartition.tick ) 5: else  Partition switch actions 7: RestoreContext(heirPartition.context) 6: if currentSchedule 6= nextSchedule ∧ 8: PendingScheduleChangeAction(heirPartition) (currentTicks − lastScheduleSwitch) mod schedules currentSchedule .mtf = 0 then 7: currentSchedule ← nextSchedule Algorithm 3 AIR PAL – pre POS process scheduler 8: lastScheduleSwitch ← currentTicks 1:  Executed immediately after AIR Partition Dispatcher and 9: tableIterator ← 0 at every POS-level clock tick 10: end if 2: PAL ClockTickAnnounce(elapsedTicks) 11: heirP artition ← 3: elapsedTicks = 1 schedules currentSchedule .table tableIterator .partition 4: POS ProcessScheduler() 12: tableIterator ← (tableIterator + 1) mod schedules currentSchedule .numberPartitionPreemptionPoints 13: end if 5.2 Process deadline violation monitoring Process deadline violation monitoring, a RV action, was is dispatched, the absolute value (in POS-level clock ticks) made non-intrusive in the AIR hardware-assisted design. of its partition preemption point is inserted in the AO con- Each process issues, when required, system calls through the figuration; when this instant is reached, an AO’s hardware APEX interface. For those listed in Table 1, AIR PAL en- exception triggers the execution of Algorithm 1. capsulation provides the registering of the process’ deadline in the AO (updating the process’ entry, or creating a new The RV actions of Algorithm 1 check, from the active PST, one, if not configured yet) or its unregistering (removing if the current instant is a partition preemption point (line 3). the process’ entry from the AO configuration). If a process’ If that is not the case, a severe system level error has oc- deadline instant is reached, the AO detects the timeliness curred and the HM is notified (line 4) to handle the situation. violation and issues a hardware exception that once caught The remaining lines (6-12) implement the partition switch activates the process level event handler defined by the ap- actions of [20], checking (line 6) if there is a pending schedul- plication programmer, as illustrated in Figure 3. The APEX ing switch to be applied and the current instant is the end primitive RAISE APPLICATION ERROR is used for that of the MTF. If these conditions apply, a different PST will purpose, with PAL encapsulating a software-based RV ac- be used henceforth (line 7). The processing resources are tion confirming the process deadline violation. assigned to the heir partition, obtained (line 11) from the PST in use, until the next partition preemption point. The Table 1: APEX primitives needing access to the AO AIR Partition Scheduler is set (line 12) to access the heir to support process deadline violation monitoring partition parameters. Primitive Short description This hardware/software co-design allows to maintain some Need to register/update deadline in the AO degree of AIR architectural flexibility with advantages in [DELAYED ]START Start a process [with a given delay] terms of improved safety and timeliness. This is particularly PERIODIC WAIT Suspend execution of a (periodic) process until the next release point useful for running AIR in platforms integrating processor REPLENISH Postpone a process’s deadline time cores (e.g., dual-core ARM) and FPGA logic [10]. Need to unregister deadline from the AO The partition switch actions are followed by the execution STOP[ SELF] Stop a process [itself] of the AIR Partition Dispatcher specified in Algorithm 2. Two significant differences from [20] do exist: suppression The occurrence of process-/partition-level errors may be sig- of specific elapsed clock ticks setting, which are no longer nalled through interpartition communication to a (system required because the partition dispatcher is always invoked partition) process performing a Fault Detection, Isolation after a partition switch; insertion of the next partition pre- and Recovery (FDIR) function. A system-wide reconfigura- emption point in the AO configuration (line 6). The remain- bility logic should be included in FDIR [7, 20]. ing actions in Algorithm 2 are related to saving and restoring the execution context (lines 2 and 7) and evaluation of the elapsed clock ticks (line 4). Line 8 enforces the execution 5.3 Analysis and discussion of pending actions the first time after a PST change the Critical software, namely that developed to go aboard an partition is executed [20]. aerial or space vehicle, goes through a strict process of ver- ification, validation and certification. Compared with the equivalent specification in [20], the de- sign of Algorithm 3 was greatly simplified since all the ac- Code complexity affects the effort required for that process, tions concerning process deadline violation monitoring were being one relevant metric for code complexity its size, in removed. The needed actions are now restricted to the sig- lines of source code. Towards the usage of standardized ac- nalling of the elapsed clock ticks (line 2) and to the instan- counting methods one employ the logical source lines of code tiation of the POS native process scheduler (line 4). (logical SLOC) metric of the Unified CodeCount tool [15]. The C implementation of fundamental AIR software compo- Parameters: nppp = 6; TSD = 0,00015 time units; Ttick = 1 time unit nents is assessed in Table 2, which shows its logical SLOC Processing overhead difference (v) 0,00016 count along with the entity instantiating the component, 0,00014 and implicitly, the instantiation frequency. 0,00012 0,00010 Most AIR software components have linear complexity, O(1): 0,00008 Full hardware AIR Partition Scheduler/Dispatcher 0,00006 accesses to multielement structures are made by index, be- Hardware-assisted AIR Partition Scheduler/Dispatcher 0,00004 ing independent of the number and position of the elements. 0,00002 The exception concern process deadline verification in the 0,00000 software-based approach, which in the worst case wields 10 30 50 70 90 110 130 150 170 190 O(n), being n the number of processes in the partition. TMTF (time units) Similar considerations apply to timing issues. The AIR ob- Figure 5: Analysis of AIR Partition Scheduler and server and the non-intrusive hardware-assisted approach has Dispatcher processing overheads reduced the number and code complexity of software compo- nents in the path of POS-level clock tick processing. This is specially true for Algorithm 3 and its software-based coun- which includes recommendations for adaptation of IMA-like terpart code complexity and worst case timing, though in the architectures. Some results on reconfigurable IMA [4] and normal and most frequent case where no process deadlines UAS adaptive and reconfigurable control [25] do exist. occur, both components exhibit similar execution times. A hardware/software co-design approach and the concept of Comparing the normalised processing time overheads of AIR system observer is present in the Simplex Architecture [3]. Partition Scheduler and Dispatcher (TSD ), in the software- Emergence of non-intrusive runtime verification techniques based and hardware-assisted approaches, along a full nor- for embedded systems in general is addressed in [26, 18], malised MTF period (TM T F ): while its applicability to complex safety-critical systems is presented in [13]. However, no previous work have applied TSD Sof t − TSD Hard such techniques to the realm of TSP systems. υ = (1) TM T F ≈ TSD Sof t − TSD Hard . nppp (2) 7. CONCLUSION Ttick TM T F This paper addressed fundamental mechanisms providing support for adaptive and self-adaptive behaviour to appli- where, nppp is the number of partition preemption points in cations based on the AIR architecture for time- and space- the MTF and Ttick is the normalised POS-level clock tick. partitioned systems. The usage of hybrid platforms com- The normalisation of timing parameters in Figure 5 take bining processor cores and programmable logic makes ad- the experimental values TSD Sof t = 150 ns and Ttick = 1 ms vantageous the use of a hardware-assisted design comple- as references, making TSD Hard ≈ TSD Sof t for hardware- mented with some simple software-based components. The assisted and TSD Hard = 0 for a full hardware implementa- computational cost of such components decreases and the tion of the AIR Partition Scheduler/Dispatcher. non-intrusive runtime verification of the system enables im- provements in both safety and timeliness properties. The difference to software-based processing overheads (υ) in function of MTF duration is represented in Figure 5. Non-intrusive runtime verification is a relevant contribution For the full hardware implementation, that difference is in- with respect to verification, validation and certification ef- dependent from the MTF value being, in any case, up- forts of TSP systems that will be extended in future research. per bounded by the TSD Sof t /Ttick ratio, which typically Additional works aim to taking advantage of multicore plat- have quite small values due to the efficient coding of AIR forms in AIR [6], which include adaptation/reconfiguration Partition Scheduler and Dispatcher components. For the features and, in the near future, RV capabilities. hardware-assisted approach the processing overhead differ- ence is smaller, dependent on the number/frequency of parti- tion preemption points and only asymptotically approaches 8. REFERENCES [1] AEEC (Airlines Electronic Engineering Committee). the TSD Sof t /Ttick limit. Avionics Application Software Standard Interface, Part 1 - Required Services, Mar. 2006. Though POS-level hardware-assisted mechanisms are also deemed to benefit partition/process scheduling timeliness [2] AEEC (Airlines Electronic Engineering Committee). and jitter, those issues have not been addressed so far. Avionics Application Software Standard Interface, Part 2 - Extended Services, Dec. 2008. 6. RELATED WORK [3] S. Bak, D. Chivukula, O. Adekunle, M. Sun, To the best of our knowledge, contemporary approaches M. Caccamo, and L. Sha. The System-level Simplex to flexible scheduling in TSP systems are restricted to the Architecture for improved real-time embedded system mode-based scheduling feature of the commercial Wind River safety. In 15th IEEE Real-Time and Embedded Tech. VxWorks 653 product [27]. Previous research on other TSP and Applications Symposium, pages 99–107, Apr. 2009. solutions [9] and works on scheduling analysis for avionic [4] P. Bieber, E. Noulard, C. Pagetti, T. Planche, and systems [14, 11] do not foresee mechanisms for timeliness F. Vialard. Preliminary design of future reconfigurable adaptation. Alternatives to TSP/IMA are compared in [12], IMA platforms. In Second Int. Workshop on Adaptive Table 2: Logical SLOC metrics and instantiation entities for fundamental AIR software components Software-based approach Hardware-assisted approach Logical SLOC Instantiation Logical SLOC Instantiation AIR Partition Scheduler a 13 POS-level clock tick - - b AIR RV Partition Scheduler - - 12 partition preemption point c AIR Dispatcher 10 POS-level clock tick 8 partition preemption point AIR PAL – register deadline 34 APEX call 4 APEX call AIR PAL – unregister deadline 12 APEX call 6 APEX call d AIR PAL – Pre POS Process Scheduler 16 POS-level clock tick 4 POS-level clock tick POS-level clock tick ISR >190 e POS-level clock tick >190 POS-level clock tick a Specified and analysed in [20, 7] b Specified in Algorithm 1 c Specified in Algorithm 2 d Specified in Algorithm 3; software-based approach specified and analysed in [20, 7] e RTEMS 4.9 [16] C code only; plus >182 assembly instructions in the POS-level clock interrupt service routine (ISR) and Reconfigurable Embedded Systems, pages 21–24, Forum on COCOMO and Systems/Software Cost Grenoble, France, Oct. 2009. Modelling, Los Angeles, USA, 2007. [5] J. Carraca, R. C. Pinto, J. P. Craveiro, and J. Rufino. [16] On-Line Applications Research Corporation. RTEMS Information security in time- and space-partitioned C User’s Guide, 4.9.4 edition, 2010. architectures for aerospace systems. In Proc. 6th [17] R. C. Pinto and J. Rufino. Towards non-invasive Simpósio de Informática (INForum 2014), pages run-time verification of real-time systems. In 26th 457–472, Porto, Portugal, Sept. 2014. Euromicro Conf. on Real-Time Systems - WIP [6] J. P. Craveiro. Real-Time Scheduling in Multicore Session, pages 25–28, Madrid, Spain, July 2014. Time- and Space-Partitioned Architectures. PhD [18] T. Reinbacher, M. Fugger, and J. Brauer. Runtime thesis, Universidade de Lisboa, Portugal, Aug. 2013. verification of embedded real-time systems. Formal [7] J. P. Craveiro and J. Rufino. Adaptability support in Methods in System Design, 24(3):203–239, 2014. time- and space-partitioned aerospace systems. In [19] J. Rosa, J. P. Craveiro, and J. Rufino. Safe online Proc. 2nd Int. Conf. on Adaptive and Self-adaptive reconfiguration of time- and space-partitioned systems. Systems and Applic., Lisbon, Portugal, Nov. 2010. In Proc. 9th IEEE Int. Conf. on Industrial Informatics [8] J. P. Craveiro and J. Rufino. Schedulability analysis in (INDIN 2011), Caparica, Lisbon, Portugal, July 2011. partitioned systems for aerospace avionics. In Proc. [20] J. Rufino, J. Craveiro, and P. Verissimo. Architecting 15th IEEE Int. Conf. on Emerging Technologies and robustness and timeliness in a new generation of Factory Automation, Bilbao, Spain, Sept. 2010. aerospace systems. In A. Casimiro, R. de Lemos, and [9] A. Crespo, I. Ripoll, and M. Masmano. Partitioned C. Gacek, editors, Architecting Dependable Systems embedded architecture based on hypervisor: the VII, volume 6420 of LNCS. Springer, 2010. XtratuM approach. In Proc. 8th European Dependable [21] J. Rushby. Partitioning in avionics architectures: Computing Conf., Valencia, Spain, Apr. 2010. Requirements, mechanisms and assurance. Technical [10] DILIGENT. ZYBO Reference Manual, Feb. 2014. Report NASA CR-1999-209347, SRI International, [11] A. Easwaran, I. Lee, O. Sokolsky, and S. Vestal. A California, USA, June 1999. compositional scheduling framework for digital [22] S. Santos, J. Rufino, T. Schoofs, C. Tatibana, and avionics systems. In Proc. 15th IEEE Int. Conf. J. Windsor. A portable ARINC 653 standard Embedded Real-Time Computing Systems and interface. In Proc. 27th Digital Avionics Systems Applications, Beijing, China, Aug. 2009. Conf., St. Paul, MN, USA, Oct. 2008. [12] B. Ford, P. Bull, A. Grigg, L. Guan, and I. Phillips. [23] M. Tafazoli. A study of on-orbit spacecraft failures. Adaptive architectures for future highly dependable, Acta Astronautica, 64(2-3):195–205, 2009. real-time systems. In Proc. 7th Ann. Conf. on Systems [24] TSP Working Group. Avionics time and space Engineering Research, Loughborough, UK, Apr. 2009. partitioning user needs. Technical Note [13] A. Kane. Runtime Monitoring for Safety-Critical TEC-SW/09-247/JW, ESA, Aug. 2009. Embedded Systems. PhD thesis, Carnegie Mellon [25] B. Vanek. Future trends in UAS avionics. In Proc. University, USA, Feb. 2015. 10th Int. Symp. of Hungarian Researchers on [14] Y. Lee, D. Kim, M. Younis, and J. Zhou. Partition Computational Intelligence and Informatics, scheduling in APEX runtime environment for Budapest, Hungary, Nov. 2009. embedded avionics software. In Proc. 5th Int. Conf. on [26] C. Watterson and D. Heffernan. Runtime verification Real-Time Computing Systems and Applications, and monitoring of embedded systems. Software, IET, pages 103–109, Hiroshima, Japan, 1998. 1(5):172–179, October 2007. [15] V. Nguyen, S. Deeds-Rubin, T. Tan, and B. Boehm. A [27] Wind River. Wind River VxWorks 653 Platform 2.4 SLOC counting standard. In The 22nd Int. Ann. and 2.5, 2015. Retrieved Jun 29, 2015.