A Brute-Force Schedulability Analysis for Formal Model under Logical Execution Time Assumption

International audienceThis article presents a schedulability analysis for real-time systems designed under the Logical Execution Time (LET) assumption. This assumption increases the predictability of real-time systems by separating time events from scheduling events. A toolchain based on the formal language Fiacre combined with the LET assumption is designed to organize a set of tools to model, verify, and generate code. In this context, an exact brute-force schedulability analysis based on a simulation is proposed. The tools and algorithms to manage the computation are described and a speedup is proposed. An experiment on a synthetic system shows the efficiency of this approach