Methodology of Combining Empirical Stress Testing and Formal-Methods Based Schedulability Analysis for Real-Time Multicore Software

Current certification guidance documents for aircraft provide plans, processes, and objectives. This has been successful in terms of achieving safety but it comes at the expense of leading to a less agile software development; this makes software development slow for greenfield development, prevents rapid updates of software, and prevents rapid upgrades of hardware. The use of formal methods (FM) has the potential to avoid some of these drawbacks. A critical issue today is the use of multicore and their potential to introduce inter-core interference which can violate real-time requirements. Therefore, in this paper, we present a two-step reasoning framework that can be used to bring some FM to the analysis of real-time requirements of software executing on multicore.