To my friends and all the people who have, in one way or another,

7.9 Schedule of tasks set with the WCET 3 . The symbols ↑ and ↓ indicate activation and completion of tasks, respectively. Here job 1 of 𝑡𝑎𝑠𝑘 3 misses its deadline as indicated by the dashed red circle. . . . . . . . . . . . . . . 131

DEDICATIONS

To my parents, the love you have given me is priceless. All the words in the world cannot express my gratitude. I place in your hands the fruit of long years of study, long months of your love and tenderness, and long days of learning. Your support and encouragement have always given me the strength to persevere in prospering in life.

To Sofia, I know I am not the best sister in the world, but I adore you. You will find a modest testimony of my most sincere affection and deepest attachment in this work.

To my grandmother, you have always treated me as your daughter. I can never thank you enough for that. May God bless you with health, long life, and prosperity.

To my aunts and uncles, I would have liked to thank you all one by one as you deserve, but if I do, my dedications will fill more pages than the whole report.

To Imad, you have always supported me, and no words can describe my gratitude for your encouragement.

ACKNOWLEDGEMENT

This experience spent within Huawei Paris Research Lab and within the Real-Time Systems team of the LS2N (Laboratoire des Sciences du Numérique de Nantes) would never have been so fruitful without the contribution of some people that I would like to thank particularly: First, I would like to thank my three supervisors: Olivier H. ROUX, Jean-Luc BÉCHEN-NEC, and Gaétan HAINS, who knew how to play their roles perfectly. They ensured this project's good progress and managed to provide rigorous and professional seriousness in a friendly and relaxed climate with a disconcerting virtuosity. I am very grateful for their trust and the wise advice they gave me. I am also very honored by the friendship they have shown me, and it is a great opportunity and pleasure for me to work with them during this period.

I want to take this opportunity to thank all the members of the RSD Grenoble team and the Real-Time Systems team of the LS2N for their kindness and the technical and financial resources they have given me to carry out this project in good condition. I cannot forget to thank the members of the CSI Paris team for their welcome, help, and sympathy.

I want to thank the jury members, Mr. Emmanuel GROLLEAU and Mr. Patrick MARTINEAU, who honored me by being the reviewers of this manuscript and for having accepted to evaluate my work. I also thank Mrs. Isabelle PUAUT and Gaétan HAINS, who agreed to examine this project and be a jury members.

Finally, I thank my family, friends, and colleagues who supported me during my thesis years.

INTRODUCTION

Embedded systems are now present in various contexts and applications in our everyday lives. These systems have evolved and need to use increasingly complex hardware and software architectures to achieve the required level of performance. In addition, the demand for high-performance computing among applications has led to a rise in the usage of multi-core chips. Embedded systems are required to implement all of the desired functionalities and validate both the functional and temporal accuracy.

Considering the time, the embedded system is designed as a real-time system for safety-critical reasons. A real-time system interacts with a complex external environment and should meet deadlines, guarantee timing constraints, and consider the correctness of the computation. The design of such a system must thus be predictable, i.e., its behavior must be expected concerning the time requirements. The real-time system has three classifications:

• Hard real-time system: Failure to meet the deadline and time constraints in this system has disastrous consequences;

• Soft real-time system: This system can occasionally miss its deadline without severe consequences;

• Firm real-time system: The system allows infrequently missed deadlines with a specification of which deadlines can be lost. If the system misses more deadlines than defined in the specification, the system fails and can cause serious consequences.

In order to increase confidence and prevent unexpected behavior, system verification is essential. It is crucial to perform time verification and validation to demonstrate that the system will always be able to react according to its time constraints and that the task scheduling sequences will always be appropriate.

The real-time system (RTS) architecture, as represented in Figure 1.1, is composed of a software component, i. e. applications that interact with a Real-Time Operating System (RTOS), and a hardware part that allows its execution. Software components In the RTS software application, tasks communicate with each other by exchanging messages or through synchronization mechanisms. The real-time operating system manages the hardware resources and provides a scheduler. The scheduler is in charge of the order in which tasks are executed to ensure the deadlines are respected. The RTOS evolution is formalized with standards; In the avionics and automotive industries, ARINC 653 [START_REF]Avionics Application Software Standard Interface, Part 1[END_REF], OSEK/VDX, and AUTOSAR [START_REF] Group | OSEK/VDX Operating System Specification tech[END_REF][START_REF] Autosar Gbr | Specification of operating system[END_REF] standards propose implementation rules for software and hardware independence and requirements that an operating system must ensure. Thus, standards provide specifications for developing an RTOS with various features, including scheduling policy, memory, and timing protection.

Software components

Software application

Hardware component

The RTS hardware comprises processors, memories, input/output devices, and additional components. The hardware architecture is often categorized according to the number of processors and cores.

Serious incidents can occur if errors are present in the real-time software system. Therefore, developing a computer system that is free of errors is imperative. Testing is a standard method for identifying software program errors. Because it is not exhaustive, it does not guarantee the elimination of all errors. Furthermore, it is insufficient for real-time critical systems where a failure could have disastrous consequences. Formal verification is a solution to increase the implementation reliability of the system. It is a technique that has been recommended as a safety verification method in the ISO-26262 standard for the automotive industry [4].

Verifying that the system's specification properties are satisfied is required to establish that the system is accurate. Safety and liveness are the two most significant types of these properties [START_REF] Lamport | Proving the Correctness of Multiprocess Programs[END_REF]. While the safety property indicates that an unexpected event will not occur, the liveness property typically implies that a program's finite parts will complete their execution if their input is correct. In addition, it is critical to ensure that the operating system behaves as expected. In fact, the entire system's reliability depends on the operating system that handles its complexity. Therefore, RTOS must adhere to the OS specification to ensure security and functional safety. That emphasizes the need to use a formal approach to provide system verification.

Compliance verification of an OSEK/VDX and AUTOSAR operating system is typically carried out with a test suite consisting of multiple applications. The conformance test suite is thus executed on the RTOS to obtain the standard certification. Contrary to software testing methods that analyze software behavior to reveal defects, formal methods examine the behavior of the software to prove the presence or absence of defects. Formal verification approaches have proven to be highly effective. They allow mathematically proving a system's specification. time stimuli, such as periodic interruptions generated by timers ii) Applications and code blocks of the OS are executed concurrently on several cores iii) Some parts of the OS code can be executed simultaneously by several cores (StartOS service, Spinlock services).

Choice of the model For this purpose, we use formal methods, particularly the modelchecking technique. Model-checking [7] effectively deals with concurrency and interaction between parallel processes, which are the significant sources of error in the systems. These concurrency errors are subtle and complex to reproduce or find in tests because there are many possible interleavings in the parallel processes execution. However, model-checking is ideally suited to identify concurrency bugs and demonstrate their absence in a system. It relies on the algorithmic exploration of the system model's whole state space to verify the correctness of properties on the entire execution path. We apply our approach to the real-time operating system Trampoline [START_REF] Béchennec | Trampoline an open source implementation of the OSEK/VDX RTOS specification in Emerging Technologies and Factory Automation[END_REF], a multi-core RTOS compliant with OSEK/VDX and AUTOSAR standards.

As the RTOS we are dealing with is written in C, a model-checker running on concurrent C programs, such as [START_REF] Gadelha | ESBMC 5.0: An Industrial-Strength C Model Checker in Proceedings of the 33rd ACM[END_REF], may seem usable, but the call to services goes through assembly code whose formal analysis would require a complete hardware architecture model, and which would not be portable. Furthermore, the goal is not to check only the properties of a C program but to check behavioral properties against real-time stimuli and manage the resulting interruptions. Therefore, we need a model-checker on timed models as we consider the execution times of the application tasks. The execution times of the OS instruction blocks are neglected for the genericity of the approach. The knowledge of the execution time would apply only to a precise hardware target.

A product of timed automata as used in [START_REF] Tigori | Formal Model-Based Synthesis of Application-Specific Static RTOS[END_REF] can simulate concurrency and its interleaving. However, it will not be able to model the simultaneous execution of a code sequence on several cores unless the model of this code sequence is artificially duplicated. We will therefore use time Petri nets for concurrency and time modeling. We will extend them with a particular notion of colors so that the same sequence of transitions can be traversed by several tokens, each with a different color modeling the core on which the code is executed.

Scientific contribution

Our thesis work leads us to three main contributions to achieving the objectives presented in the previous section. The first contribution concerns the chosen formalism for the modeling. Since the control of multi-core real-time systems often requires simultaneous access in true parallelism to shared resources and time Petri nets do not capture these features directly, we propose extending the formalism with colored transitions and high-level functionality, i.e., a predefined syntax manipulating different types of expressions made up of variables. The High-Level Colored Time Petri Nets encompasses both timed multi-enableness of transitions and sequential pseudo code, and the reachability problem is decidable for this model. We then use this extended formalism to model the real-time application as a sequence of RTOS system calls in addition to the multi-core RTOS that reproduces the control flow and uses the same variables as those of the implementation.

The second contribution is composed of two parts. First, the formal verification of the RTOS conformity to the AUTOSAR standard; we model the test suite that includes several applications with High-Level Colored Time Petri Nets (HCTPN). Second, we check the inter-core synchronization mechanism involved in concurrent OS service execution. AUTOSAR conformance testing is based on requirements verification. We focus on multi-core operating system (OS) requirements, for which there are eighty. Each specification is formalized by an observer that evaluates compliance. The observer models are innocuous i.e. they do not interfere with system behavior. Cores are associated with Petri net transition colors. Using the model-checking technique, we verify the AUTOSAR specifications. The approach results conclude that the operating system model respects the AUTOSAR requirements. As part of the AUTOSAR compliance verification of the multi-core RTOS and since the AUTOSAR test cases are synchronous; they do not include concurrent situations, we are interested in verifying simultaneous service calls execution on cores for the safety analysis. Specifically, we rely on the modelchecking technique to formally verify multi-core RTOS synchronization mechanisms: concurrent access to OS data structures, multi-core scheduling, and inter-core interrupt handling. That automatically identified two possible errors in the simultaneous execution, proving insufficient data protection and faulty synchronization. Both errors have been corrected and the updated model verified to satisfy AUTOSAR compliance.

Finally, we provide a verification approach to determine the schedulability of real- time applications with dependent preemptive tasks on the detailed multi-core RTOS model. It also allows determining under which temporal conditions the application is schedulable using parameters on the firing intervals. Verification of real-time application schedulability is usually performed using a very abstract system representation, which poorly supports inter-task dependencies. We represent each application task by a Petri net whose transitions carry Best-Case Execution Time and Worst-Case Execution Time [𝐵𝐶𝐸𝑇, 𝑊𝐶𝐸𝑇] firing intervals and make service calls to the OS. Preemption is supported by means of stopwatches. We accurately analyze worst-case response time computation for dependent preemptive tasks in multi-core systems. Thus, our contribution is a complete approach to verifying the schedulability of a real-time system, the AUTOSAR compliance of multi-core RTOS, and the inter-core synchronization mechanism involved in concurrent OS service execution using High-Level Colored Time Petri Nets (HCTPN). The approach steps are illustrated in Figure 1.2. We rely on the Roméo model-checker tool for the verification, available under a free license [START_REF] Roux | Roméo: formal verification and synthesis for timed systems[END_REF].

Software system model

Manuscript outline

The manuscript is structured in two parts:

• Part I introduces the general context of the thesis. It starts with a state-of-the-art in chapter 2 concerning the different formal methods and their application to verifying real-time systems with an RTOS. Chapter 3 presents the Trampoline operating system on which we apply our formal approach. It shows its mono-core and multi-core architectures;

• Part II concerns our contribution and is organized into four chapters: (i) Chapter 4 presents the High-Level Colored Time Petri Nets (HCTPN), the extended formalism used for modeling. (ii) Chapter 5 describes the formal model of the RTOS and the application built with the HCTPN formalism using the Roméo tool.

(iii) Chapter 6 is dedicated to the verification approach of the operating system's compliance with the AUTOSAR specification based on its formal model. It also includes verifying concurrent situations and the errors proving faulty synchronization with the model-checker. (iv) Chapter 7 presents the schedulability verification of real-time application with dependent preemptive tasks.

The last part of this manuscript is a conclusion and some perspectives on our work.

Part I

General context

Chapter 2

FORMAL METHODS FOR REAL-TIME SYSTEMS

Introduction

Formal approaches ensure system confidence, and the emergence of new software tools has led to their usability. We examine in this chapter the existing formal verification methods in the literature, focusing on their use for verifying the application's schedulability and real-time operating systems. We rely on the two most popular families of formal methods: theorem proving and model-checking. In theorem proving, we examine infinite systems specified in an appropriate mathematical logic to verify the properties and provide proof. On the other hand, in model-checking, we examine whether the desired property is satisfied by exploring the entire state space of the finite constructed model. It is an automatic and efficient technique that can also cope with the problem of state space explosion when the number of states grows to infinity with increasing variables and their distinct values as well as components.

Formal verification methods

Testing is widely used in practice, although it is clearly impossible to use it in highly critical systems where test data could cause damage if errors are made before actual deployment. Another solution is to simulate the behavior of the system on a computer. The simulation does not work directly on the real system but on a model. A model represents an abstract representation of the real system, usually written using mathematics or logic. Both testing and simulation are widely used in industrial applications, and their use has proven to be very useful. A drawback, however, is that it is not usually possible to simulate or test all possible scenarios or behaviors of a given system.

Here are some examples where testing and simulation failed. The Air France Flight 447 crash in June 2009 caused the death of the people on board. When the plane was flying from Rio de Janeiro to Paris, the storm caused the airspeed sensors to freeze, leading the autopilot to disconnect. The pilots misinterpreted the noise, leading the plane to ram into the sea. The worst is knowing that the crash could have been prevented. In August 2005, The Boeing 777-200 of Malaysia Airlines Flight 124 suddenly and without warning climbed higher than expected. The crew faced a supposedly impossible situation where the stall and overspeed indicators turned on simultaneously. The aircraft landed about 18 minutes into the flight, and the failure occurred in its air data inertial reference unit. One of the two accelerators controlling the airspeed failed, and due to a software anomaly, the second one used incorrect data from the first accelerator [START_REF] Charette | Automated to death in IEEE Spectrum[END_REF]. Another example is the failure of the Computer Aided Dispatch (CAD) in the London ambulance service. The inquiry team's investigations show that the system and the resilience of the hardware were not fully tested before implementation [START_REF] Finkelstein | Report of the Inquiry into the London Ambulance Service[END_REF].

Formal verification, in contrast to testing and simulation, permits the exhaustive investigation using static analysis based on mathematical models to verify the accuracy of hardware or software behavior. Accidents can then be avoided if the systems are verified and analyzed mathematically. Two categories exist, deductive methods based on theorem proving [START_REF] Cook | The Complexity of Theorem-Proving Procedures[END_REF] and automatic methods based on model-checking [START_REF] Clarke | Exploiting Symmetry In Temporal Logic Model Checking[END_REF].

Theorem-based methods

Formal theorem proving is one of the fastest developing areas in recent years, that verifies the correctness of the system's properties through mathematical reasoning. With the new powerful tools of theorem provers, unsolvable problems several decades ago are being treated today, and new challenges are emerging. Many fields, including computer science [START_REF] Gallier | Logic for Computer Science: Foundations of Automatic Theorem Proving[END_REF], biomedical [START_REF] Rashid | Formal reasoning about systems biology using theorem proving[END_REF], economics [START_REF] Kerber | An introduction to mechanized reasoning[END_REF], machine learning [START_REF] Kaliszyk | HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving[END_REF], and artificial intelligence [START_REF] Wang | Computer Theorem Proving and Artificial Intelligence in Computation, Logic, Philosophy: A Collection of Essays[END_REF], have successfully used theorem provers. It provides a statement from a logical set of axioms or hypotheses to check a system's properties defined with mathematical logic. Theorem provers can be divided into two categories:

• Interactive Theorem Provers (ITPs), known as proof-assistants [START_REF] Harrison | History of Interactive Theorem Proving in Computational Logic[END_REF]: this approach allows proofs to be constructed with a reliance on user guidance. It involves human interaction with the tool in the formal proof development process.

Coq [START_REF] Dowek | The Coq proof assistant user's guide : version 5[END_REF] and Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL: a proof assistant for higherorder logic[END_REF] are some of the most well-known existing tools.

Their performance is outstanding, and they formalized and proved many theorems in the first hundred theorems list 1 .

• Automated Theorem Provers (ATPs) [START_REF] Sutcliffe | Evaluating general purpose automated theorem proving systems[END_REF]: This type consists in building the proofs automatically by the tool without user intervention based on a description of the system to be verified, a set of axioms, and inference rules. Current ATP systems can solve non-trivial problems, such as the Robbins problem [START_REF] Mccune | Solution of the Robbins Problem[END_REF] solved by the EQP automated theorem proving program for first-order equational logic [START_REF] Frege | Conceptual Notation, and Related Articles[END_REF]. In practice, the complexity of most problems is enormous and cannot be solved within resource limits. Thus a significant concern of ATP research is developing more powerful systems that can solve problems within the same resource constraints.

Theorem-proving techniques have limitations, such as the slow process of building proof, even with automatic provers. In addition, most theorems do not support graphical and visualization tools, and logic is not practical as a language. The process requires a high-level of expertise on the user's part, especially for ITPs that require heavy interaction and a lot of energy. These drawbacks are thus an obstacle to adopting theorem proving when dealing with complex systems. However, future works in this direction continue to improve faster and more efficient provers and make them more suitable for the industrial sector by attempting to combine different techniques.

Model-based verification methods

Among the formal methods, model-checking is an automated approach to verify that a model of a system conforms to a specification expressed as a property. This specification defines the requirements for the expected behavior of the system. The verification is performed by exploring the model's states with the help of algorithms and allows to guarantee properties. Achieving the system abstraction and specification is a crucial step that may require system mastery and expertise in the methods used. The model must also be accurate and as close as possible to the system from a behavioral point of view. Therefore, the property verification must be the same for the system and its model.

The system is described by a model that abstracts the system, most often using state machines such as automata, Petri nets, and process algebras. The choice of model de- pends on its expressiveness, i.e., its capacity to represent many system characteristics. In general, the expressiveness of a model can be opposed to its simplicity of verification. As an expressive formalism can be very helpful in modeling, it can also be blocking in the verification phase. The specification of the system is described by properties that can be expressed in the form of observers of the model or using a particular logic such as Linear Temporal Logic (LTL) [START_REF] Rozier | Linear Temporal Logic Symbolic Model Checking[END_REF] and Computation Tree Logic (CTL) or the temporal extension of the latter: TCTL [START_REF] Alur | Model-Checking in Dense Real-time[END_REF]. In [START_REF] Lamport | Proving the Correctness of Multiprocess Programs[END_REF], L. Lamport decomposes the correctness properties of a system into two categories: safety properties which express that an undesired situation will never happen, and liveliness properties which ensure that under certain conditions, the desired situation will eventually occur. These two categories of properties can also be reduced to a reachability verification that looks for a path where the desired situation is met.

Once the model and its specification are built, an analysis of whether the model satisfies the specification is performed. This analysis explores all possible executions of the system from its initial state. The generation of a counter-example is automatic when the property is false in the form of an execution trace starting from the initial state to the state violating the property. Thus, the model-checking approach is performed on two main phases (modeling and specification verification), as shown in Figure 2.1.

With model-checking, the user does not intervene in the verification process and easily identifies the states of the system causing its violation through counter-examples generation. The main advantage is, therefore, its automatic character. However, the approach is limited by computing capacities. The problem of the combinatorial explosion is due to the exhaustive exploration of the system's state space. Several reduction studies are proposed to cope with this limitation of exhaustive approaches [START_REF] Godefroid | Using Partial Orders to Improve Automatic Verification Methods in Proceedings of the 2nd International Workshop on Computer Aided Verification[END_REF][START_REF] Dhaussy | Reducing State Explosion with Context Modeling for Model-Checking[END_REF].

Timed models

Time-based models allow the modeling and verification of real-time applications by considering task execution times and synchronization mechanisms. Adding temporal parameters to the application can restrict its behaviors, limiting the number of states of its model. Moreover, it is necessary to check the quantitative temporal properties to identify specific reasons for failure. The main families of models are extended with time, such as timed automata [START_REF] Alur | A theory of timed automata[END_REF] and time Petri nets [START_REF] Merlin | A Study of the Recoverability of Computing Systems[END_REF].

Timed automata

A timed automaton [START_REF] Alur | A theory of timed automata[END_REF] is an extended finite automaton with clocks to consider time. A finite automaton is an abstract machine with a limited number of states that accepts an input alphabet to evolve its state. The values of the clocks increase during the execution of the timed automaton and can be associated with constraints called invariants [START_REF] Henzinger | Symbolic Model Checking for Real-Time Systems[END_REF].

The invariants of the system control the duration for which the system can remain in a given location and will leave it once the invariant is no longer satisfied. The clocks are then reset to zero when the transition is fired, and the associated action is completed. The formalism is supported by several models checking tools [START_REF] Larsen | Uppaal in a Nutshell[END_REF][START_REF] Yovine | Kronos: A Verification Tool for Real-Time Systems[END_REF][START_REF] Amnell | TIMES b-A Tool for Modelling and Implementation of Embedded Systems in Tools and Algorithms for the Construction and Analysis of Systems[END_REF]. Among them, UPPAAL [START_REF] Larsen | Uppaal in a Nutshell[END_REF] is one of the best-known and most efficient tools. The tool is conceived for the modeling and formal verification of real-time systems using a network of a timed extended finite automaton with useful functions written in the UPPAAL language [START_REF] Bengtsson | UPPAAL -a tool suite for automatic verification of real-time systems in Hybrid Systems III[END_REF]. Kronos, proposed by S. Yovine [START_REF] Yovine | Kronos: A Verification Tool for Real-Time Systems[END_REF], is a software tool that allows users to verify the specifications of a real-time system during its design phase. T.Amnell et al. [START_REF] Amnell | TIMES b-A Tool for Modelling and Implementation of Embedded Systems in Tools and Algorithms for the Construction and Analysis of Systems[END_REF] propose the TIMES tool as a scheduling analyzer based on timed automata and their extensions. It supports simulation, formal verification and code generation of the model. TIMES provides a graphical editor that allows the user to specify the parameters of a set of tasks such as priority, deadline and execution time. Nevertheless, the tool does not allow the analysis of task sets with shared resources.

Petri nets and time

Petri nets have two main temporal extensions: Time Petri nets [START_REF] Merlin | Recoverability of Communication Protocols -Implications of a Theoretical Study[END_REF] and the timed Petri nets [START_REF] Ramchandani | ANALYSIS OF ASYNCHRONOUS CONCURRENT SYSTEMS BY TIMED PETRI NETS tech[END_REF]. Time Petri nets are an extension of the classical Petri net known as a placetransition net, where each transition is associated with a time interval. This interval specifies the possible firing dates. The second temporal extension of Petri Nets is Timed Petri Nets [START_REF] Ramchandani | ANALYSIS OF ASYNCHRONOUS CONCURRENT SYSTEMS BY TIMED PETRI NETS tech[END_REF] where transitions are fired as soon as possible while a transition can be fired within a given interval for Time Petri Nets. Time is thus represented by minimum (or exact) durations for Timed Petri nets. Time can also be associated to transitions (Ttime [START_REF] Berthomieu | Modeling and Verification of Time Dependent Systems Using Time Petri Nets[END_REF]), places (P-time [START_REF] Calvez | P-Time Petri Nets for Manufacturing Systems with Staying Time Constraints[END_REF][START_REF] Bonhomme | A symbolic schedulability technique of real-time systems modeled by P-Time Petri nets[END_REF]) and arcs (A-time [START_REF] Rakkay | Time Arc Petri Nets and Their Analysis[END_REF]). T-time Petri nets are the most widely used in real-time systems and those used in our modeling in this thesis project, and they have the same expressiveness as Turing machines [START_REF] Jones | Complexity of some problems in Petri nets[END_REF], contrary to Timed automata. We present the formalism with its color extension in detail in Chapter 4.

Several software environments for analyzing Petri nets with temporal extensions are developed 2 , allowing the users to edit the system graphically [START_REF] Liu | TiPNet: a graphical tool for timed Petri nets[END_REF][START_REF] Vernadat | Time Petri Nets Analysis with TINA in Third International Conference on the Quantitative Evaluation of Systems[END_REF][START_REF] Lime | Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches in 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems[END_REF]. TiPNet [START_REF] Liu | TiPNet: a graphical tool for timed Petri nets[END_REF] is a tool supporting the analysis of Timed Petri Nets to simulate discrete systems. TINA (TIme Petri Net Analyzer) 3 [START_REF] Vernadat | Time Petri Nets Analysis with TINA in Third International Conference on the Quantitative Evaluation of Systems[END_REF] allows editing, simulation, and building state space abstractions for time Petri nets. Roméo is the tool used in our research work [START_REF] Lime | Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches in 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems[END_REF], and it allows the analysis of time Petri Nets with different extensions. Its representation is given in Section 4.5.

Timed model with stopwatches

Timed models can be extended with stopwatches instead of clocks to model the temporal interruption of actions and subsequent resumption. Indeed, for timed automata (TA) and time Petri nets (TPN), time elapses at the same speed for all system components. Hence they cannot abstract preemptive scheduling policies where the execution of a task can be suspended and later resumed at the same point.

Several extensions of these models have been proposed to express the suspension and resumption of actions by adding the stopwatch notion [START_REF] Cassez | The Impressive Power of Stopwatches in CONCUR 2000 -Concurrency Theory[END_REF][START_REF] Roux | A T-time Petri net extension for real time-task scheduling modeling[END_REF][START_REF] Lime | Expressiveness and analysis of scheduling extended time Petri nets[END_REF][START_REF] Bucci | Time state space analysis of real-time preemptive systems[END_REF][START_REF] Roux | Formal Semantics and State Space Computation in Applications and Theory of Petri Nets[END_REF]. Stopwatch automata [START_REF] Cassez | The Impressive Power of Stopwatches in CONCUR 2000 -Concurrency Theory[END_REF] is an extension that allows modeling preemptive real-time tasks. For TPNs, several extensions are proposed: Scheduling-TPN [START_REF] Roux | A T-time Petri net extension for real time-task scheduling modeling[END_REF][START_REF] Lime | Expressiveness and analysis of scheduling extended time Petri nets[END_REF], Preemptive-TPN [START_REF] Bucci | Time state space analysis of real-time preemptive systems[END_REF], and Time Petri nets with inhibitor hyperarcs (IHTPN) [START_REF] Roux | Formal Semantics and State Space Computation in Applications and Theory of Petri Nets[END_REF]. The first extension [START_REF] Roux | A T-time Petri net extension for real time-task scheduling modeling[END_REF] is based on adding two new attributes associated with places: the allocation of the processor or resource and the priority of the modeled task. The scheduling policy considered is preemptive with fixed priorities. Preemptive time Petri nets [START_REF] Bucci | Time state space analysis of real-time preemptive systems[END_REF] rely on a resource assignment mechanism determining timer progress. IHTPN proposed in [START_REF] Roux | Formal Semantics and State Space Computation in Applications and Theory of Petri Nets[END_REF] controls stopwatches associated with transitions using classical arcs and branch inhibitor hyperarcs. However, modeling a real-time system with preemptive scheduling using timed automata, especially in a multi-core context, is not always simple. It requires an automaton per core, and the application is described by an automata product. Extended Petri nets with stopwatches include a semantic of the behavior of real-time schedulers and can represent parallel or concurrent systems.

Scheduling studies based on timed models

The time verification of real-time systems consists in proving that the system will always be able to react according to its time constraints. Timing validation is, therefore, a decision process that concerns task scheduling sequences. Many scheduling studies are based on a representation by timed automata [START_REF] Behrmann | Optimal scheduling using priced timed automata[END_REF][START_REF] Zaharia | Formal verification and implementation of real time operating system based applications in[END_REF][START_REF] Waszniowski | Formal Verification of Multitasking Applications Based on Timed Automata Model[END_REF][START_REF] Pimkote | Simulation of Preemptive Scheduling of the Independent Tasks Using Timed Automata in[END_REF] or TPNs [START_REF] Grolleau | Scheduling Real-Time Systems by Means of Petri Nets[END_REF][START_REF] Xu | Compositional schedulability analysis of real-time systems using time Petri nets[END_REF][START_REF] Lime | Formal Verification of Real-time Systems with Preemptive Scheduling[END_REF].

Timed automata and scheduling

Several studies use timed automata for the realtime system's verification context and consider scheduling analysis. G. Behrmann et al.

propose in [START_REF] Behrmann | Optimal scheduling using priced timed automata[END_REF] a model of timed automata called Priced Timed Automata (PTA). Its semantics is defined by associating to each transition and location a non-negative realvalued cost. Their analysis consists in seeking optimal offline scheduling with minimal cost using UPPAAL's model-checker. The authors in [START_REF] Waszniowski | Formal Verification of Multitasking Applications Based on Timed Automata Model[END_REF] focuse on modeling multitasking applications to verify the worst time execution of the tasks using timed automata. The modeled applications considered non-preemptive tasks and routine service interrupts. The temporal and logical properties of these applications are verified in the UPPAAL model-checker. T. Zaharia and P. Haller [START_REF] Zaharia | Formal verification and implementation of real time operating system based applications in[END_REF] present a framework for modeling and verification of embedded microsystems. The mini real-time applications running under a multitasking kernel are described through networks of timed automata, and the properties are specified in UPPAAL's CTL subset. They focused on preemptive and non-preemptive scheduling tasks with different priorities. Besides, source code is automatically generated. The study presented by the authors in [START_REF] Pimkote | Simulation of Preemptive Scheduling of the Independent Tasks Using Timed Automata in[END_REF] proposes an approach to simulate preemptive scheduling using UPPAAL. They associate temporal diagrams with timed automata by mapping rules to check the time constraints and the deadlock.

Time Petri nets and scheduling Several studies proposed modeling with time Petri to verify complex real-time systems and analyze schedulability. E. Grolleau and A.

Choquet-Geniet present in [START_REF] Grolleau | Scheduling Real-Time Systems by Means of Petri Nets[END_REF] the modeling of complex systems with concurrent actions using colored PNs [START_REF] Jensen | Coloured petri nets and the invariant-method[END_REF]. Their works, however, do not consider online schedulers, and the PN generates an offline sequence to execute. The work proposed by the authors in [START_REF] Lime | Formal Verification of Real-time Systems with Preemptive Scheduling[END_REF] shows a formal verification approach for real-time systems with a preemptive scheduling policy, including Fixed Priority and Earliest Deadline First, with the possibility to use Round-Robin for tasks with the same priority. The modeling is done with scheduling time Petri nets and also allows the verification of temporal properties for other scheduling policies. Dianxiang et al. analyze in [START_REF] Xu | Compositional schedulability analysis of real-time systems using time Petri nets[END_REF] the scheduling of real-time systems using time Petri nets. Behavioral properties are separated from temporal properties during verification. Behavioral specifications are verified by reachability properties, and temporal analysis is conducted based on absolute and relative trigger domains.

Formal methods for operating systems verification

Formal verification of real-time operating systems is helpful to guarantee the correctness of the system and to provide proof that the system is well implemented. This is possible nowadays thanks to several tools that have been developed in recent years. Several works have been performed in this context that we mention in the following. The list is not exhaustive, and other studies not discussed in our work may exist. Some are based on formal methods to verify the same objectives as those we have for verifying operating systems compliant with OSEK/VDX and AUTOSAR standards. Among the studies, some do not focus on temporal verification when checking the OS and consider other aspects of correction, such as the absence of deadlock or compliance with standards. Other research works are more interested in verifying temporal properties and schedulability analysis considering the RTOS.

Deductive methods for operating systems verification Existing formal techniques have been utilized in a number of research studies for operating system software using deductive methods. The authors in [START_REF] Hohmuth | The VFiasco approach for a verified operating system in 2nd PLOS[END_REF][START_REF] Klein | SeL4: Formal Verification of an OS Kernel[END_REF][START_REF] Espinosa | Formal verification of a real-time operating system[END_REF][START_REF] Xu | A Practical Verification Framework for Preemptive OS Kernels in Computer Aided Verification[END_REF][START_REF] Gu | Building Certified Concurrent OS Kernels[END_REF] use proof assistants to verify formally a realtime operating system. M. Hohmuth and H. Tews in [START_REF] Hohmuth | The VFiasco approach for a verified operating system in 2nd PLOS[END_REF] propose a verification project of the L4 compatible Fiasco microkernel. The verification of the C++ sources of Fiasco is performed by the general-purpose theorem prover PVS. Their approach handles typecorrectness and safety proof. The verification of seL4 microkernel in [START_REF] Klein | SeL4: Formal Verification of an OS Kernel[END_REF] is done inside Isabelle/HOL. A complete verification process is performed independently of the application, from the high-level specification of the kernel behavior to its safe execution. Their proof, however, is limited to the validation of assumptions about the proper functioning of the hardware and compiler. In [START_REF] Espinosa | Formal verification of a real-time operating system[END_REF], the Coq proof assistant is applied to the formalized specification description of FreeRTOS -to verify the correctness of significant properties expressed in Separation Logic. In [START_REF] Xu | Towards Fault-Tolerant Real-Time Scheduling in the seL4 Microkernel[END_REF], authors implemented an Earliest Deadline First (EDF) real-time scheduling policy in seL4 microkernel and provided the time management and periodic task model. Fengwei et al. [START_REF] Xu | A Practical Verification Framework for Preemptive OS Kernels in Computer Aided Verification[END_REF] propose a verification framework for preemptive operating system kernels. The framework allows the definition of the model by a specification language and its verification by program logic. All proofs are in Coq, and the verification of the functional correctness of the kernel is performed. Gu et al. [START_REF] Gu | Building Certified Concurrent OS Kernels[END_REF] develop a certified concurrent OS kernel mC2 using CertiKOS and Coq proof assistant. They verify its correctness and system-call specification. AUTOSAR operating systems verification AUTOSAR OS verification was the subject of numerous studies [START_REF] Fang | Formal Model-Based Test for AU-TOSAR Multicore RTOS in[END_REF][START_REF] Peng | Modeling and Verification of AUTOSAR OS and EMS Application in International Symposium on Theoretical Aspects of Software Engineering[END_REF][START_REF] Trinh | Formalization and Verification of AUTOSAR OS Standard's Memory Protection[END_REF][START_REF] Yan | Timing Modeling and Analysis for AUTOSAR Schedule Tables[END_REF]. The authors in [START_REF] Fang | Formal Model-Based Test for AU-TOSAR Multicore RTOS in[END_REF] show a formal model-based approach to improve the test coverage for AUTOSAR multi-core RTOS. They first defined the concrete formal model conforming the requirement of AUTOSAR RTOS in PROMELA.

OSEK/VDX operating systems verification

Then, with the model, they proposed a test program generator. Finally, they calculated the optimal test sequence for every test case and translated it into an execution program. Peng et al. in [START_REF] Peng | Modeling and Verification of AUTOSAR OS and EMS Application in International Symposium on Theoretical Aspects of Software Engineering[END_REF] use timed CSP to model AUTOSAR OS and the engine management system (EMS) application. They verify some safety properties through Process Analysis Toolkit (PAT). The authors in [START_REF] Trinh | Formalization and Verification of AUTOSAR OS Standard's Memory Protection[END_REF] propose a formalization of the AUTOSAR OS memory protection specification. They use the Event-B specification language and verify the consistency. Yan et al. in [START_REF] Yan | Timing Modeling and Analysis for AUTOSAR Schedule Tables[END_REF] focus on the AUTOSAR schedule table mechanism. They formally model a schedule table using a transition system and analyze the schedulability.

Trampoline operating system verification Several works are done on the Trampoline RTOS [START_REF] Tigori | Formal Model-Based Synthesis of Application-Specific Static RTOS[END_REF][START_REF] Choi | Safety Analysis of Trampoline OS Using Model Checking: An Experience Report in[END_REF][START_REF] Choi | Model Checking an OSEK/VDX-Based Operating System for Automobile Safety Analysis[END_REF][START_REF] Boukir | Requirement Specification and Model-Checking of a Real-Time Scheduler Implementation[END_REF]. In [START_REF] Choi | Safety Analysis of Trampoline OS Using Model Checking: An Experience Report in[END_REF], the authors show an approach that converts the kernel source code of the RTOS Trampoline to a formal model in PROMELA, the modeling language of SPIN. The objective of this work is to verify the safety properties and the exactness of the kernel model. Using model-checking, they were able to identify some possible safety violation scenarios. The performance of this study is enhanced by Yunja in [START_REF] Choi | Model Checking an OSEK/VDX-Based Operating System for Automobile Safety Analysis[END_REF] using embeddedC constructs in PROMELA. The number of states and transitions is reduced, which leads to an improvement in verification costs. The authors in [START_REF] Tigori | Formal Model-Based Synthesis of Application-Specific Static RTOS[END_REF] propose a complete model of the RTOS Trampoline in its mono-core version us-ing extended and timed automata with the UPPAAL tool. This model includes all the functions and services of the OS. They perform a reachability analysis on the application and OS model states to eliminate infeasible paths, and prune the model appropriately. From the pruned model, a source code configured for the application can be produced. Based on the Trampoline formal model done by Tigori et al. in [START_REF] Tigori | Formal Model-Based Synthesis of Application-Specific Static RTOS[END_REF], Boukir et al. [START_REF] Boukir | Requirement Specification and Model-Checking of a Real-Time Scheduler Implementation[END_REF] integrate the model of the global EDF scheduling and verify the scheduler implementation. The conformity of the scheduler implementation is then checked for a set of properties using synthetic application models. These models generate all possible scheduler excitation scenarios. However, the Tigori model does not represent the accurate time aspect. Indeed, the execution time is discrete, expressed with invariant and clock variables.

Conclusion

Many studies have been done on the formal verification of operating systems. The works cited in this chapter come close to our verification approach. Our objective remains mainly different since we seek to propose a verification approach that aims to verify the OS's conformity to the AUTOSAR multi-core standard, the multi-core synchronization mechanisms, and the application schedulability, considering their interaction with the multi-core RTOS. Among the studies, some do not focus on the temporal aspects of OS verification. It is because some operating systems do not satisfy user requirements in real time. For example, the SeL4 microkernel is based on a round-robin with 256 priority levels, and the threads have no time attributes such as budget, period, or deadline. For some works, the proofs cover neither application-specific properties nor the interaction of applications with the operating system. Other studies focus on verifying the correctness properties and compliance verification. However, research works on the formal verification of multi-core AUTOSAR RTOS are limited. Chapter 3

TRAMPOLINE REAL-TIME OPERATING SYSTEM

Introduction

In this chapter, we first introduce the automotive standards OSEK/VDX and AUTOSAR for implementing real-time operating systems. Then, we present the Trampoline realtime executive on which our thesis work is based. This RTOS respects the OSEK/VDX and AUTOSAR standards. We describe its mono-core and multi-core architecture and present examples of operating system calls in both versions.

The OSEK/VDX standard

OSEK (Offene Systeme und deren Schnittstellen für die Elektronik im Kraftfahrzeug) stands for "Open Systems and their corresponding Interfaces for the Electronics in Motor Vehicles". The standard was created in 1993 by a German automotive company consortium (BMW, Bosch, DaimlerChrysler, Opel, Siemens, and Volkswagen Group) and a department at the University of Karlsruhe. In 1994, the French car manufacturers Renault and PSA joined the consortium, developing a similar project called VDX (Vehicle Distributed eXecutive). OSEK/VDX is widely recognized in the automotive industry, and several parts are proposed for the standard. The architecture shown in Figure 3.1, page 36, shows the three elements in the list related to the code that runs on targets: • Communication stack and data exchange between control units. This Interaction layer provides communication services for the transfer of application messages;

• Real-time operating system.

We will present the mono-core OSEK/VDX real-time operating system in the following.

The OSEK/VDX OS

The OSEK real-time operating system specification is a support that helps real-time applications and the embedded software used by electronic control units meet their execution requirements. It is a mono-processor operating system for distributed automotive control units. Its specification [START_REF] Group | OSEK/VDX Operating System Specification tech[END_REF] describes a uniform environment for the electronic control unit software application to efficiently use resources. The OSEK operating system offers various services, processing levels, and conformance classes for the portability of software applications and the reduction of development costs. For the same purpose, OSEK defines an OSEK Implementation Language (OIL) for standardized configuration information. This language allows a portable description of all OSEK-specific objects such as tasks, alarms, events, etc.

Operating system services

OSEK-OS offers several services that are statically defined at the compilation phase. The task management and interrupt handling services are detailed below.

Task management

The task manager handles the activation, scheduling, and synchronization in addition to the termination of the application's tasks. In OSEK, two types of tasks can be defined: basic and extended.

Basic tasks

The basic tasks release the processor in two cases: When they complete their execution or if they are pre-empted by other higher priority tasks. Thus, basic tasks have three states: suspended, ready, and running, as shown in the state model in Figure 3.2, page 38:

• Suspended: This is the task's passive state where it can be activated;

• Ready: Activated or preempted tasks are ready to run and waiting for processor allocation. The scheduler chooses which task to execute;

• Running: Only one task can be in this state, executing its instructions.

Extended tasks

The execution of an extended task can be waiting for an event when using the operating system call WaitEvent. An event is an object defined by the application and assigned to the extended tasks to communicate binary information or synchronize tasks. The event mechanism induces the states of tasks to and from the waiting state, as represented in Figure 3.3, page 38. That distinguishes extended from basic tasks. Thus, when the state of the calling task is set to waiting, the task releases the CPU and awaits an event. It can also wait for a resource or use a blocking instruction.

Task priority

The priority of a task is defined by a numeric value, with 0 representing the lowest priority and greater values representing higher priorities. Different tasks can share the same priority level; in this case, they can start considering their activation FIFO order, and the oldest task on the same priority list is the first to be processed. on the task's priority, the scheduler selects the next task to be processed and decides which ready task will become running.

Scheduling policy

The OSEK standard defines a fixed priority scheduling policy. The tasks can be preemptive, non-preemptive, or belong to a task group; a task group is a set of tasks that are non-preemptable by each other but can be preemptable by higher priority tasks in the application. Tasks in the group can share a common internal resource. An internal resource is a resource that is automatically taken by a task when it enters the running state, except if it has already taken the resource, and is released when the task terminates. Priorities and preemption of tasks are statically assigned as attributes of tasks. Therefore, the type of scheduling depends on the preemption attribute, regardless of the task type (basic or extended). Three possible scheduling types are defined in OSEK.

• Full preemptive scheduling: The scheduler can preempt a running task to allocate the CPU to a higher priority task;

• Non preemptive scheduling: The running task must complete its execution or be waiting for an event to allow a higher priority ready task to start its execution;

• Mixed preemptive scheduling: Scheduling can be both preemptive and non-preemptive. It depends on whether the task is defined as preemptable or non-preemptable.

API services

The OSEK operating system provides several services; here are some services grouped by category: Some of these OSEK operating system services ensure task management, such as:

• ActivateTask is used to activate a suspended or new task, setting its state to READY;

• TerminateTask allows terminating the running task, and its state is changed from Running to Suspended;

• ChainTask activates a task after the termination of the calling task;

• Schedule permits the execution of the ready task with the highest priority. If the calling task uses an internal resource, a rescheduling1 , occurs.

Interrupt handling

Interrupt processing is performed by an Interrupt Service Routine (ISR), which is scheduled by the hardware and classified into two categories:

• ISR category 1: These interrupt service routines do not use any operating system services, except services that enable or disable interrupts. The interrupt does not influence task management. The program processing resumes at the instruction where the interrupt occurred once the ISR is completed;

• ISR category 2: This ISR category can call operating system services with restrictions on their use. After the ISR category 2 has been terminated, rescheduling is performed if a preemptable task has been interrupted and no other interrupt is active.

Processing levels

OSEK-OS defines three levels of processing: (i) interrupts, (ii) scheduler, and (iii) tasks.

The processing of interrupts has the highest priority, and the scheduler, defined as a logical level, has a higher priority than the tasks. At the task level, tasks are scheduled according to the user's statically assigned priority and the interrupt processing can consist of several interrupt priority levels.

Conformance classes

The Conformance Classes (CC) define multiple real-time executive versions to meet application requirements. The OSEK operating system has four conformance classes that allow it to be compatible with diverse applications and hardware. They depend on the multiple requests of task activation, task types (basic or extended), and the number of tasks per priority. The following are the four distinct levels:

• BCC1: This class contains only basic tasks with one task per priority and one activation request per task;

• BCC2: Like BCC1, it allows multiple task activations and the possibility of more than one task per priority level;

• ECC1: Like BCC1, it also supports extended tasks;

• ECC2: Like ECC1, it is possible to have multiple activations of a task and multiple tasks per priority level.

The AUTOSAR standard

AUTOSAR(AUtomotive Open System ARchitecture) is an industrial standard for automotive software architecture, created in 2003. The objectives include scalability to different vehicles, software portability, and the product's lifecycle maintainability. AUTOSAR is an evolution of OSEK/VDX standard for the specification of operating systems [START_REF] Autosar Gbr | Specification of operating system[END_REF]. Unlike OSEK/VDX, it defines a multi-core design that implements a partitioned scheduling policy with fixed priority. Partitioning is obtained by assigning the objects managed by the OS (tasks, ISR, alarms, schedule tables, events, resources, ...) to an OS-Application2 , and the operating system module schedules processor resources for OS-Applications bounded to cores. Partitioned scheduling involves statically allocating tasks to a ready list per core before being scheduled and cannot migrate.

AUTOSAR architecture

The architecture proposed by AUTOSAR consists of three software layers that are executed on a microcontroller, as shown in Figure 3.5, page 43:

• Application Layer: This layer includes the various software components of the application that interact with the runtime environment and contain the functions to be executed;

• Runtime Environment: It is a middleware that supports abstract communication between the different application software components and between the Basic Software and the applications;

• Basic Software Layer: It provides the necessary services to the upper software layer and consists of several sublayers. The service layer is the highest sublayer and contains various functions such as the Autosar OS, vehicle network communications, and management memory service. The Microcontroller Abstraction Layer (MCAL) accesses the peripheral modules of the hardware. The ECU Abstraction Layer is an interface to the MCAL and provides access to peripherals and devices. The complex Drivers layer can access the microcontroller directly, and are used mainly for complex functions not found on other layers. language with some parts, like context switching, written in assembly language because they depend on the Instruction Set Architecture (ISA) of the microcontroller. The source code is over 20,000 lines long and includes 180 functions for the targetindependent part. The operating system occupies few resources, both memory and CPU, and is suitable for both 8-bit and 32-bit targets. It offers the classic services:

Trampoline RTOS

• Management and scheduling of tasks according to a fixed priority scheduling policy;

• Synchronization between tasks via signaling (events) and mutual exclusion (resources) mechanisms;

• Periodic execution of tasks or setting of events (alarms and schedule tables);

• Communication between tasks on the same Electronics Control Unit (ECU) or running on different ECUs;

• Interrupt Service Routines (ISR) management. The OSEK/VDX and AUTOSAR OS are configured according to the application. The objects necessary for the application, tasks, ISRs, alarms, ... are described with their relations in the dedicated language OIL for OSEK/VDX and in XML for AUTOSAR. A dedicated compiler called GOIL reads this description and, using templates described in a Goil template language (GTL), produces C data structures (task descriptors, alarms, etc.) and code that is then compiled and linked with the OS and application code, as shown in Figure 3.6, page 44.

Mono-core Trampoline architecture

The mono-core architecture of Trampoline consists of three components, as shown in Figure 3.7, page 45, which are as follows:

1. The API (Application Programming Interface) includes the services defined by OSEK/VDX and AUTOSAR standards. AUTOSAR OS adds services to OSEK/VDX, limiting some configurations. The operating system manages several types of objects: tasks, Interrupt Service Routines (ISR), resources that are used to implement critical sections using the IPCP protocol, a variant of PCP [START_REF] Sha | Priority inheritance protocols: an approach to real-time synchronization[END_REF], or alarms that are used to implement periodic tasks or to set an event;

2. The Kernel contains all the low-level functions on which the API services are based. These C-language-implemented functions allow the management of tasks and their scheduling and ensure the handling of counters and treatment of interrupts;

3. The BSP (Board Support Package) is the low-level function part of the Trampoline that depends on the target machine. It contains modules that handle calls to API services and context switch of tasks, implemented in assembler. In addition, there is a component to handle interrupts from external sources like a timer and a memory protection module to manage access rights to the operating system memory.

Start-up

The OS starts with the StartOS service call in the AppModeID application mode. The operating system first performs some hardware-specific and application initializations. Some tasks can be defined as AUTOSTART; if they exist, they are activated. Autostart tasks are ready to be executed after the operating system's start-up. Then Trampoline calls the scheduler, and the CPU will be allocated to the autostart task with the highest priority. If no task is available, a particular idle task runs. Its priority is set to 0 (i.e. the lowest priority in the system), while the application tasks have a priority greater than or equal to 1.

Scheduling

In OSEK/VDX, the scheduling policy uses a static priority assigned to each task which can be in 4 states: suspended, waiting (if extended), ready, and running. In Trampoline, two extra states are used for internal management: Autostart and ready_and_new. An autostart task is automatically activated when StartOS is called. The ready_and_new state is used for a ready task, but its context is uninitialized. That occurs when the task has just been activated for the first time.

The scheduler of Trampoline manages a ready task queue dynamically during the execution of the application according to their priority and whether they are preemptable or not. This queue is a FIFO list table, as shown in Figure 3.4, page 39, where the tasks are ordered by priority or activation order if their priorities are equal. The priority and the preemptability of a task are set in the OIL task description using the PRIORITY and the SCHEDULE attributes, respectively. The scheduler uses functions to handle the ready list of tasks, such as tpl_put_new_proc, which puts a new process in a ready list, tpl_put_preempted_proc to put a preempted process in a ready list, and tpl_remove_proc for removing all the process instances in the ready queue.

The scheduler also manages a data structure called tpl_kern. This implemented structure contains all the data about a task during its execution. It points to the static and dynamic task descriptors represented in the C data structure file (Listing 3.1, page 46), storing all the information describing the task in memory (identifier, priority, type, state, etc.). The static descriptor contains the data that is not susceptible to vary and stored in the ROM (Read-Only Memory). The dynamic descriptor contains information that is updated during execution and which can be stored in RAM (Random Access Memory). tpl_kern thus gathers several pieces of information: the currently running task, the task that has been selected to replace the currently running task (if any) after a rescheduling, a flag indicating if a rescheduling shall be done (need_schedule), a flag indicating if a context switch shall be done (need_switch) and, finally, a flag indicating if a context save shall be done (need_save). The stored information is detailed below: The scheduler allows the manipulation of state transitions (Figure 3.3, page 38) via the following functions:

• 𝑡 𝑝𝑙_𝑠𝑡𝑎𝑟𝑡 (): Start the highest priority ready job at the top of the ready list. Its information is copied into the elected attributes of the 𝑡 𝑝𝑙_𝑘𝑒𝑟𝑛 structure.

• 𝑡 𝑝𝑙_𝑝𝑟𝑒𝑒𝑚 𝑝𝑡 (): Preempt the running process, and its state is switched from the running state to the ready state.

• 𝑡 𝑝𝑙_𝑟𝑢𝑛_𝑒𝑙𝑒𝑐𝑡𝑒𝑑 (): The elected process becomes the running process, and the running process is preempted. This function copies the elected attributes of 𝑡 𝑝𝑙_𝑘𝑒𝑟𝑛 into the running attributes.

All the above functions that manipulate the task states are called by the 𝑡 𝑝𝑙_𝑠𝑐ℎ𝑒𝑑𝑢𝑙𝑒_𝑠𝑒𝑟𝑣𝑖𝑐𝑒 function, which calls the principle scheduling function 𝑡 𝑝𝑙_𝑠𝑐ℎ𝑒𝑑𝑢𝑙𝑒_ 𝑓 𝑟𝑜𝑚_𝑟𝑢𝑛𝑛𝑖𝑛𝑔 3and then performs a context switch to run the elected process.

Context switch

The context switch is performed when the scheduler indicates that it is necessary through the need_switch flag of the tpl_kern data structure. For example, the context switch is performed when a task is preempted, its context is saved, and the elected task's context is restored. The scheduler updates the elected task in the tpl_kern structure. In task termination, it is necessary to perform a context switch without saving its context. Thus, the need_switch field takes the value NO_NEED_SWITCH when no context switch is required and the NEED_SWITCH value when it is necessary to perform a context switch. NEED_SAVE indicates the need to save the context of the process that loses the CPU and restore the elected one. The context switch is done between the running and the elected task when they are different. The elected attributes of the tpl_kern structure are copied to the running ones in the tpl_run_elected function called at the context switch.

Calling operating system services

In Trampoline, the call to an OS service is made in a wrapping function through a dedicated instruction of the microcontroller4 which, acting as a software interrupt, transfers the execution to a system call handler in supervisor mode. The latter is in charge of calling the corresponding kernel function. In the process, the interrupts are masked. That prevents an interrupt routine calling the OS from running simultaneously and the internal data structures of the operating system from being corrupted. The execution of service without a context switch in the mono-core implementation is shown in Figure 3.8, page 49. The execution of service when there is a context switch to a newly activated task in the mono-core implementation is given in Figure 3.9, page 49. sc is the service call in the PowerPC instruction set and rfe is the return.

Two data structures are used to manage rescheduling and context switching: the list of ready tasks and the tpl_kern structure. tpl_kern gathers several pieces of information represented in Listing 3.1, and its flags are reset in the system call handler before calling the kernel function in the call sequence shown in Figure 3.9, page 49. If the kernel function performs an operation that adds a task to the list of ready tasks or if the task being executed ends (TerminateTask or ChainTask services), need_schedule is set, and the kernel function ends by performing a rescheduling. If the rescheduling leads to a context switch, the need_switch flag is set, and the context switch is performed at the end of the system call handler just before returning to the newly scheduled task.

Multi-core Trampoline architecture

The multi-core version of the Trampoline presents an extension of its mono-core architecture shown in Figure 3.10, page 50. Lock services and an inter-core interrupt handler have been added to deal with the simultaneous execution of the kernel and services on two or more different cores, as well as inter-core interactions and communication. The IOC module provides communication between OS-Applications and transmits data based on the RunTime Environment (RTE) configuration information.

Multi-Core start-up

In the multi-core configuration of Trampoline, the cores are distinguished by their identifier and start with the master-slave system. The master core is activated first, and then the slave cores are started. All cores are synchronized through two barriers with the StartOS service call. The first synchronization point occurs before the operating system is initialized, and the OS-application-specific StartupHooks are executed on the core to which they are bound. The second barrier is after the end of StartupHooks and before the scheduler starts.

The global lock

In the multi-core implementation, interrupt masking is not enough. Indeed, it is necessary to prevent the OS kernel from running simultaneously on two or more cores if the called service can access data structures of the OS that are common to the cores. For this purpose, the kernel can be executed on two different cores with sequential access through a global lock. This lock protocol is called the Biglock in Trampoline. The kernel is locked during a system call, preventing more than one core from entering the kernel mode or handling interrupts simultaneously. When a core calls a service, it acquires the Biglock and only returns it at the end of its execution before leaving kernel mode. Thus, the other cores wait for the lock to be released. Nevertheless, spinlocks and startup services can run in parallel and simultaneously on several cores with no Biglock.

Scheduling Trampoline implements a partitioned scheduling policy with fixed priorities for its multi-core version. The tasks are statically allocated to each core that has its ready list. This ready list is represented by a binary heap where each entry has a key for sorting and the process ID. The key is the concatenation of the job 5 priority and the job rank. The heap size is computed with the sum of the process activations. The head of the queue contains the highest priority job. Thus the tpl_put_new_proc function inserts a newly activated job into the heap according to its calculated priority (i.e., static priority and activation rank), unlike the mono-core version where the job is placed at the end of the FIFO list corresponding to its priority. Scheduling is performed on the core where it is triggered and can lead to preemption and context switching on another core. To better separate the information for each core, the data structure tpl_kern (Listing 3.1), managed by the scheduler, is duplicated according to the core number.

Executing a multi-core service call

The entry in the multi-core critical section protected by the Biglock is made at the beginning, and then the exit at the end of the system call handler.

When a service is called and results in a rescheduling, for example, if one task activates another, the rescheduling is performed on the core where the service call occurs. Thus, when a task running on core 0 activates a task assigned to core 1, the task ac-5. Each activation of a process is a job. tivation service is performed on core 0 and modifies the list of ready tasks of core 1. Additionnally, when this activation requires a context switch on core 1, it must necessarily be performed on core 1 as well. To trigger this context switch, core 0 therefore sends an inter-core interrupt request to core 1, and the interrupt routine which will execute on core 1 will perform the context switch. This sequence is illustrated in Figure 3.11, page 52:

1. In A , a rescheduling is performed by core 0 for core 1; 2. In B , an inter-core interrupt is sent to notify core 1 that it must make a context switch;

3. The interrupt is handled by core 1, which blocks on an active wait for the release of the Biglock in C ; 4. Core 0 releases the Biglock in D . The release of the Biglock allows core 1 to take it and to enter the critical multi-core section;

5. Finally core 1 performs the context switch from task 𝜏 1 to task 𝜏 Having simultaneous service calls in parallel on several cores leads to a more complex scheme, especially if a core is the target of an inter-core interrupt while executing a service call that leads to a rescheduling. We can thus extend the example presented in Figure 3.11, page 52, with task 𝜏 1 making a service call on core 1, e.g. TerminateTask, just after ActivateTask has been called by task 𝜏 0 on core 0. This scenario is presented in Figure 3.12, page 54:

1. In A , a rescheduling is performed by core 0 for core 1 and in parallel, core 1 waits for the Biglock in B ;

2. An inter-core interrupt is sent in C to notify core 1 that it must make a context switch, but since the interrupts are masked on core 1, it remains pending;

3. Core 0 releases the Biglock by D . The release of the Biglock allows core 1 to take it and to execute the TerminateTask() service;

4. The context switch to the 𝜏 2 task is carried out, the Biglock is released, and core 1 returns to user mode to immediately take into account the inter-core interrupt by E ;

5. The execution of this inter-core interrupt consists essentially in acknowledging the interrupt and does not lead to a context switch because 𝜏 2 is the highest priority task on core 1;

6. We finally return to the execution of 𝜏 2 .

Conclusion

In this chapter, we first presented the two automotive standards, OSEK/VDX and AUTOSAR, on which the Trampoline real-time operating system is based. Then, we presented the mono-core and multi-core architectures of Trampoline, explaining the execution of the operating system service calls in both versions. In the next chapter, we will present the modeling formalism used to describe the Trampoline operating system in order to apply our formal verification approach.

HIGH-LEVEL COLORED TIME PETRI NETS FOR MULTI-CORE CONCURRENCY

Introduction

Implementing multi-core real-time systems requires concurrent access in true parallelism to shared resources. Time Petri nets do not capture these features directly and are unsuitable for modeling systems where data affects the system's behavior. Highlevel Petri nets [START_REF] Hillah | PN Standardisation: A Survey in Formal Techniques for Networked and Distributed Systems -FORTE[END_REF] have been proposed for modeling scientific problems with complex structures allowing the description of both system data and control. We propose extending time Petri nets with color and high-level functionality in this chapter. We present in detail the High-level Colored Time Petri Nets (HCTPN) used to describe the Trampoline real-time operating system. HCTPN with stopwatches are used to model preemptive real-time systems.

Informal presentation

Petri nets

Petri nets are a mathematical formalism and one of the many modeling languages used to describe distributed concurrent systems. A Petri net is a directed bipartite graph whose vertices are places and transitions. A place can contain any number of tokens. A marking 𝑀 of a Petri Net is a vector representing the number of tokens of each place. A transition is enabled (it may fire) in 𝑀 if there are enough tokens in its input places for the consumption to be possible. Firing a transition from a marking 𝑀 consumes tokens from each of its input places and produces tokens in each of its output places.

High-level Petri nets

Petri nets can be classified into two classes: ordinary Petri nets and high-level Petri nets. High-level Petri nets [START_REF] Hillah | PN Standardisation: A Survey in Formal Techniques for Networked and Distributed Systems -FORTE[END_REF] are proposed for modeling scientific problems with complex structures and manipulating different types of expressions made up of variables and written in terms of a predefined syntax. In high-level nets, each token can carry complex information which, e. g., may describe the entire state of a process or a database and handle different expressions and data structures.

The precondition (guard) and postcondition (update) over a set of variables (𝑋) are associated with transitions. A transition is enabled (it may fire) if there are enough tokens in its input places and if the guard is true. When the transition fires, the corresponding updates are executed, modifying the values of the variables. The variables take their values in a finite state (such as bounded integer or enumerate type...), guards are boolean expressions over 𝑋, and updates can be described as a sequence of imperative code expressed in a programming language but whose execution is atomic from the transition firing point of view.

Colored Petri nets

The colored extension of Petri nets allows the distinction between tokens.

Although the set 𝑋 of High-level Petri nets presented in the previous paragraph can be of arbitrarily complex type, places in colored Petri nets contain tokens of one type. This type noted 𝐶 is called the color set of the place.

An arc from a place to a transition (PT) specifies the color(s) that enabled the transition, and its firing will consume it. An arc from a transition to a place (TP) specifies the token color produced in that place by the firing of the transition. A particular color called any indicates in a PT arc that any color enabled the transition, and in a TP arc that the color consumed in the input place will be the one produced in the output place.

A marking M of a colored Petri Net represents not only the number of tokens in each place but also their respective colors. That is represented either by a multiset or by a matrix.

Time Petri Nets

Time Petri nets (TPN) extend Petri nets with temporal intervals (such as [𝛼, 𝛽] or [𝛼, +∞[) associated with transitions, specifying firing delay ranges for the transitions. Assuming transition 𝑡 became last enabled at time 𝑑 and the endpoints of its firing interval are 𝛼 and 𝛽, then 𝑡 cannot fire earlier than 𝑑+𝛼 and must fire no later than 𝑑+𝛽 unless disabled by the firing of another transition. Firing a transition takes no time.

To describe the semantics of TPN, we usually consider that a clock is associated with each transition. This clock is set to zero when the transition is newly enabled, and the transition fires when the value of the clock is in the firing interval.

Colored Time Petri Nets

For real parallelism or with interleaving semantics of timed systems, the notion of multiple enableness is needed. It refers to the fact that a transition is enabled at least twice in the same state, which implies a dynamic number of timers. Multiple enableness in time Petri nets is a natural way for modeling paradigms like multiple servers and multiple instances of codes [START_REF] Boyer | Multiple Enabledness of Transitions in Petri Nets with Time[END_REF].

For Colored Time Petri Nets, multiple enableness occurs when several combinations of colors enable a transition at a given time. In this case, there can be at most one clock per color and per transition.

Time Petri Nets with stopwatches

Time Petri nets with stopwatches, extend TPN by adding the notion of stopwatch: instead of the clocks, a stopwatch is associated with each transition. The time derivative of the stopwatch of a transition is in the set of rate {0, 1} and is given by a function from Markings. Hence the time associated with a transition can be suspended and later resumed at the same point. Moreover, transition with a 0 time derivative can not fired.

Since the clocks are replaced by stopwatches, in the case of Colored Time Petri Nets with stopwatches, there is at most one stopwatch per color and per transition.

Formal definition

We consider a Petri Nets model which encompasses both colors, high-level functionalities and stopwatches. We now give the formal definition.

High-level Colored Time Petri Net

Notations The sets N, Q ≥0 , and R ≥0 are respectively the sets of natural, non-negative rational, and non-negative real numbers. An interval 𝐼 of R ≥0 is a Q-interval iff its left endpoint ↑ 𝐼 belongs to Q ≥0 and its right endpoint 𝐼 ↓ belongs to Q ≥0 ∪ {∞}. We denote by

I (Q ≥0 ) the set of Q-intervals of R ≥0 .
𝐵 𝐴 stands for the set of mappings from 𝐴 to 𝐵. If 𝐴 is finite and | 𝐴| = 𝑛, an element of 𝐵 𝐴 is also a vector in 𝐵 𝑛 . The usual operators +, -, < and = are used on vectors of 𝐴 𝑛 with 𝐴 = N, Q, R and are the point-wise extensions of their counterparts in 𝐴.

Definition and semantics

Colored Petri nets allow tokens to have a data value called the token color. In the applications we are considering, the color of a token actually represents the processor on which the code is executed. We therefore consider token of integer type that designates the processor number. Moreover we add a special color called any to specify that any color can be used for enabling and firing a transition.

We consider a set 𝐶 of colors. An arc is either associated with a color of 𝐶 or can take on the particular color called any. For the firing of a transition, all its arcs associated with the any color must match to instantiate any at the same color taken from 𝐶.

If several values of any allow its enabling, the transition is multi-enabled, and in this case, several clocks (one per color) are associated with the transition, allowing several firing dates depending on the enabling date and the time interval.

The formal definition is as follows.

Definition 1 (High-level Colored Time Petri Net) A High-level Colored Time Petri Net

(HCTPN) is a tuple N = (𝑃, 𝑇, 𝑋, 𝐶, pre, post, (𝑚 0 , 𝑥 0 ), 𝑔𝑢𝑎𝑟𝑑, 𝑢 𝑝𝑑𝑎𝑡𝑒, 𝐼) where

• 𝑃 is a finite non-empty set of places,

• 𝑇 is a finite set of transitions such that 𝑇 ∩ 𝑃 = ∅,

• 𝑋 is a finite set of variables taking their value in the finite set X (such as bounded integer),

• 𝐶 is a finite set of colors and 𝐶 𝑎𝑛𝑦 = 𝐶 ∪ {𝑎𝑛𝑦} where any is a variable that can be instantiated to any value of 𝐶,

• pre : 𝑃 × 𝑇 → N 𝐶 𝑎𝑛𝑦 is the backward incidence mapping,

• post : 𝑃 × 𝑇 → N 𝐶 𝑎𝑛𝑦 is the forward incidence mapping,

• 𝑔𝑢𝑎𝑟 𝑑 : 𝑇 × 𝑋 × 𝑃 × 𝐶 • → {𝑡𝑟𝑢𝑒, 𝑓 𝑎𝑙𝑠𝑒} is the guard function with 𝐶 • = 𝐶 ∪ {•} where
• denotes the fact that no color is specified,

• 𝑢 𝑝𝑑𝑎𝑡𝑒 : 𝑇 × 𝑋 × 𝑃 × 𝐶 • → X 𝑋 × N 𝑃×𝐶 is the update function,
• (𝑚 0 , 𝑥 0 ) ∈ N 𝑃×𝐶 × X 𝑋 → is the initial values 𝑚 0 of the marking and 𝑥 0 of the variables,

• 𝐼 : 𝑇 → I (Q ≥0 ) is the static firing interval function.

Discrete behavior

For a marking 𝑚 ∈ N 𝑃×𝐶 , 𝑚( 𝑝) is a vector in N 𝐶 , and 𝑚( 𝑝) [𝑐] represents the number of tokens of color 𝑐 ∈ 𝐶 in place 𝑝 ∈ 𝑃. A valuation of the set of variables 𝑋 is noted 𝑥 ∈ X 𝑋 . (𝑚, 𝑥) is a discrete state of HCTPN.

Enabling a transition.

Informally, an arc is associated either with a color 𝑐 ∈ 𝐶 or with a particular color called any. To enable transition 𝑡, a place 𝑝 with an arc from 𝑝 to 𝑡 must have enough tokens with the arc's color. Moreover, all the arcs of 𝑡 associated with any must agree on the color given to any. Therefore, we forbid an arc to be associated with both any and a color 𝑐 ∈ 𝐶.

An arc pre( 𝑝, 𝑡) ∈ N 𝐶 𝑎𝑛𝑦 is a vector such that pre( 𝑝, 𝑡) [𝑐] is the number of tokens of color 𝑐 ∈ 𝐶 in place 𝑝 needed to enable the transition 𝑡 and pre( 𝑝, 𝑡) [𝑎𝑛𝑦] > 0 represents the fact that any color can enable the transition. Let 𝑇 𝑎𝑛𝑦 ∈ 𝑇 the set of transitions that can be enabled by 𝑎𝑛𝑦 color: i.e. 𝑇 𝑎𝑛𝑦 = {𝑡 ∈ 𝑇, ∃𝑝 ∈ 𝑃, s.t. pre( 𝑝, 𝑡) [𝑎𝑛𝑦] > 0 }. Moreover, we define the set 𝑇 𝑎𝑛𝑦 = 𝑇 \ 𝑇 𝑎𝑛𝑦 .

A transition 𝑡 ∈ 𝑇 is said to be enabled by a given marking 𝑚 ∈ N 𝑃×𝐶 in two cases depending on whether 𝑡 ∈ 𝑇 𝑎𝑛𝑦 or not: We have pre(𝑇 1 ) =

• if 𝑡 ∈ 𝑇 𝑎𝑛𝑦 ,
𝑟𝑒𝑑 𝑏𝑙𝑢𝑒 𝑎𝑛𝑦 𝑃 1 0 1 0 𝑃 2 1 0 0 𝑃 3 0 1 0 𝑃 4 0 0 0 . The initial marking is 𝑚 0 = 𝑟𝑒𝑑 𝑏𝑙𝑢𝑒 𝑃 1 1 1 𝑃 2 1 0 𝑃 3 0 1
𝑃 4 0 0 that enables the transition 𝑇 1 and en(𝑚 0 , 𝑇 1 ) = 𝑡𝑟𝑢𝑒. We denote by newen((𝑚, 𝑥), 𝑡, 𝑐) the set of transitions that are newly enabled by the firing of 𝑡 from (𝑚, 𝑥) with the color

𝑃 1 𝑃 2 𝑃 3 𝑇 1 [2, 3] blue red blue •• • • 𝑃 1 𝑃 2 𝑃 3 𝑇 1 [2, 3]
𝑐 (𝑐 = • if 𝑡 ∈ 𝑇 𝑎𝑛𝑦 ).
Let us go back to the HCTPN of

𝑃 2 0 0 𝑃 3 0 0 𝑃 4 1 0 . It is noted 𝑚 0 (𝑇 1 ,𝑟𝑒𝑑) ------→ 𝑚 2 .
If place 𝑃 2 had two tokens with one blue and one red color, 𝑇 1 is multi-enabled, and the firing of 𝑇 1 ∈ 𝑇 𝑎𝑛𝑦 is possible for 𝑎𝑛𝑦 = 𝑟𝑒𝑑 or 𝑎𝑛𝑦 = 𝑏𝑙𝑢𝑒. For 𝑎𝑛𝑦 = 𝑏𝑙𝑢𝑒, it leads to the following marking 𝑚 3 from this new initial marking

𝑚 ′ 0 . 𝑚 ′ 0 = 𝑟𝑒𝑑 𝑏𝑙𝑢𝑒 𝑃 1 1 1 𝑃 2 1 1 𝑃 3 0 1 𝑃 4 0 0 (𝑇 1 ,𝑏𝑙𝑢𝑒) -------→ 𝑚 3 = 𝑟𝑒𝑑 𝑏𝑙𝑢𝑒 𝑃 1 1 0 𝑃 2 1 0 𝑃 3 0 0 𝑃 4 0 1
.

High-level functionalities

We now illustrate the high-level functionalities. In the Figures, the guards are in green, and the updates are in purple. The model in Figure 4.2 is an HCTPNwith a set of three colors 𝐶 = {𝑏𝑙𝑢𝑒, 𝑟𝑒𝑑, 𝑏𝑙𝑎𝑐𝑘 }. Several combinations of color usage, on guards and in updates, via the $𝑎𝑛𝑦 variable are presented 1 . Transition 𝑇 1 ∈ 𝑇 𝑎𝑛𝑦 since at least one arc is associated with the color 𝑎𝑛𝑦. A firing of this transition produces a blue token in 𝑃 3 and produce a token in 𝑃 2 with the color ($𝑎𝑛𝑦) used for the firing. Moreover, the value of $𝑎𝑛𝑦 is used in the precondition (guard) and the postcondition (update). Hence transition 𝑇 1 is not enabled by blue token because of the guard $any ≥ 1. Moreover, the firing of 𝑇 1 leads to the execution of the update cpt[$any]=f($any,cpt). Then the transition 𝑇 1 will be fired twice respectively with a red and a black tokens leading to a marking with a red and a black tokens in 𝑃 2 and 2 blue tokens in 𝑃 3 . It remains a blue token in 𝑃 1 and the final value of cpt is {2,4,4}.

𝑃 1 $any ≥ 1 T 1 [8, 8] cpt[$any]=f($any,cpt) 𝑃 2 𝑃 3 blue ••• typedef color { blue = 0 , red = 1 , black = 2}; int [3] cpt = {2 ,2 ,5}; int f ( int firedColor , int [3] c ) { if ( firedColor == red ) { return c [ firedColor ]*2; } else { return c [ firedColor ] -1 ; } }

Time behavior

Definition 2 (Semantics of a HCTPN)

The semantics of a HCTPN is a timed transition system (𝑄, 𝑄 0 , →) where:

• 𝑄 ⊆ N 𝑃×𝐶 × X 𝑋 × R ≥0 𝑇×𝐶 • 𝑄 0 = ((𝑚 0 , 𝑥 0 ), 0) • →∈ 𝑄 × ((𝑇 × 𝐶 ∪ {•}) ∪ R ≥0 ) × 𝑄 consists

of two types of transitions:

discrete transitions (firing 𝑡 from ((𝑚, 𝑥), 𝑣)) iff: * ((𝑚, 𝑥), 𝑣)

(𝑡∈𝑇 𝑎𝑛𝑦 ,•) --------→ ((𝑚 ′ , 𝑥 ′ ), 𝑣 ′ ) with
• en(𝑚, 𝑡) = 𝑡𝑟𝑢𝑒 and 𝑣(𝑡) ∈ 𝐼 (𝑡),

• 𝑚 ′ = firing(𝑚, 𝑡, •) * ((𝑚, 𝑥), 𝑣)

(𝑡∈𝑇 𝑎𝑛𝑦 ,𝑐) -------→ ((𝑚 ′ , 𝑥 ′ ), 𝑣 ′ ) with
• 𝑐 ∈ colorSet any (𝑚, 𝑡) and 𝑣(𝑡, 𝑐) ∈ 𝐼 (𝑡),

• 𝑚 ′ = firing(𝑚, 𝑡, 𝑐) * 𝑔𝑢𝑎𝑟𝑑 (𝑡, 𝑥) = 𝑡𝑟𝑢𝑒 and 𝑥 ′ = 𝑢 𝑝𝑑𝑎𝑡𝑒(𝑡, 𝑥)

* ∀𝑡 ′ ∈ 𝑇 𝑎𝑛𝑦 s.t. en(𝑚 ′ , 𝑡 ′ ) = 𝑡𝑟𝑢𝑒 • 𝑣 ′ (𝑡 ′ , •) = 𝑣(𝑡 ′ , •) if 𝑡 ′ ∉ newen((𝑚, 𝑥), 𝑡, •),
• 𝑣 ′ (𝑡 ′ , •) = 0 otherwise * ∀𝑡 ′ ∈ 𝑇 𝑎𝑛𝑦 and ∀𝑐 ∈ colorSet any (𝑚 ′ , 𝑡 ′ )

• 𝑣 ′ (𝑡 ′ , 𝑐) = 𝑣(𝑡 ′ , 𝑐) if 𝑡 ′ ∉ newen((𝑚, 𝑥), 𝑡, 𝑐), • 𝑣 ′ (𝑡 ′ , 𝑐) = 0 otherwise -time transitions: ((𝑚, 𝑥), 𝑣) 𝑑∈R ≥0 -----→ ((𝑚, 𝑥), 𝑣 ′ ), iff: * ∀𝑡 ∈ 𝑇 𝑎𝑛𝑦 s.t. en(𝑚, 𝑡) = 𝑡𝑟𝑢𝑒, • 𝑣 ′ (𝑡, •) ≤ 𝐼 (𝑡) ↓ • 𝑣 ′ (𝑡, •) = 𝑣(𝑡, •) + 𝑑 * ∀𝑡 ∈ 𝑇 𝑎𝑛𝑦 and ∀𝑐 ∈ colorSet any (𝑚, 𝑡), • 𝑣 ′ (𝑡, 𝑐) ≤ 𝐼 (𝑡) ↓ • 𝑣 ′ (𝑡, 𝑐) = 𝑣(𝑡, 𝑐) + 𝑑
We now illustrate the main features of HCTPN in an example. The guards are in green in the Figures and the update . Since the set of variables is 𝑋 = {𝑐 𝑝𝑡}, we note a state 𝑠 = (𝑚, 𝑐 𝑝𝑡, 𝑣).

The initial state is 𝑞 0 = (𝑚 0 , {2, 2, 5}, 𝑣 0 ). The transition 𝑇 1 is enabled twice and can fire after elapsing 8 time units for both enabling. After 8 time units 𝑇 1 fires with either the red or the black colors and then can fire again with the other one. Assume that we first fire with the red color, the corresponding run is as follows: 𝑚 0 , {2, 2, 5},

• 𝑏𝑙𝑢𝑒 𝑟𝑒𝑑 𝑏𝑙𝑎𝑐𝑘 0 0 8 - → 𝑚 0 , {2, 2, 5},
• 𝑏𝑙𝑢𝑒 𝑟𝑒𝑑 𝑏𝑙𝑎𝑐𝑘 8 8

(𝑇 1 ,𝑟 𝑒𝑑) -------→ 𝑏𝑙𝑢𝑒 𝑟𝑒𝑑 𝑏𝑙𝑎𝑐𝑘 𝑃 1 1 0 1 𝑃 2 0 1 0 𝑃 3 1 0 0 , {2, 4, 5},
• 𝑏𝑙𝑢𝑒 𝑟𝑒𝑑 𝑏𝑙𝑎𝑐𝑘

8 (𝑇 1 ,𝑏𝑙𝑎𝑐𝑘 ) ---------→ 𝑏𝑙𝑢𝑒 𝑟𝑒𝑑 𝑏𝑙𝑎𝑐𝑘 𝑃 1 1 0 0 𝑃 2 0 1 1 𝑃 3 2 0 0 , {2, 4, 4},
• 𝑏𝑙𝑢𝑒 𝑟𝑒𝑑 𝑏𝑙𝑎𝑐𝑘 .

Example 2

The HCTPN given in Figure 4.3, page 66, illustrates time behavior and high-level manipulation of variables. This HCTPN has only one color and a single variable 𝑐 𝑝𝑡, and is part of a larger HCTPN. We assume that g() returns an integer between 1 and 10, handled by the other part of the net.

𝑃 1 T 1 [5, 7] 𝑐 𝑝𝑡 = 𝑔() 𝑃 2 𝑐 𝑝𝑡 <= 5 T 2 [2, 3] 𝑐 𝑝𝑡 = 0 𝑐 𝑝𝑡 > 5 T 3 [4, 6] 𝑐 𝑝𝑡 = 𝑓 (𝑐 𝑝𝑡) 𝑃3 • int cpt =0; int f ( int x ) { return 2* x -1; } Figure 4

.3: HCTPN illustrating high-level manipulation of variables

A marking is written by the matrix (|𝑃|, |𝐶 |). Since there is only one color, the marking is a vector and the initial marking is then

𝑚 0 = 𝑃 1 1 𝑃 2 0 𝑃 3 0
and enables the transi-tion 𝑇 1 . The valuations of the clocks are given by the matrix (here a vector) such that the initial valuation is

𝑣 0 = 𝑇 1 0 𝑇 2 0 𝑇 3 0
. Since the set of variables is 𝑋 = {𝑐 𝑝𝑡}, we note a state 𝑠 = (𝑚, 𝑐 𝑝𝑡, 𝑣). The initial state is 𝑞 0 = (𝑚 0 , 0, 𝑣 0 ). The transition 𝑇 1 can fire after elapsing 5 time units. We now consider the run where the function g() called by the update of the firing of 𝑇 1 returned the value 7. Then the transition's guard 𝑇 2 is false, and the transition 𝑇 3 is enabled. We assume that the transition 𝑇 3 took 4.6 time units for this run. The firing of the transition 𝑇 3 executes the corresponding update and calls the function 𝑓 that returns 13. The corresponding run is as follows:

1 0 0 , 0, 0 0 0 5 - → 1 0 0 , 0, 5 0 0 (𝑇 1 ,•) -----→ 0 1 0 , 7, 0 0 0 4.6 --→ 0 1 0 , 7, 0 0 4.6 (𝑇 3 ,•) -----→ 0 0 1 , 13, 0 0 0
Example 3 The model given in Figure 4.4, page 67, is a HCTPN with a set of two colors 𝐶 = {𝑟𝑒𝑑, 𝑏𝑙𝑢𝑒}. Several combinations of color usage, on guards and in updates, via the $𝑎𝑛𝑦 variable are presented. The valuations of the clocks are given by the matrix such that the initial valuation is

𝑃 1 T 1 [8, 8] cpt[$any]==2 cpt[$any]=f($any,cpt) 𝑒𝑛𝑑 T 2 [5, 5] 𝑃 2 blue red • • 𝑃 3 • T 3 [6, 6] cpt[1]=2 blue typedef color { red = 0 , blue = 1}; int [2] cpt = {2 , 1}; int f ( int color , int [2] c ) { if ( color == blue ) { return c [ color ] + 1; } else if ( color == red ) { return c [ color ] * 2; } }
𝑣 0 = • 𝑟𝑒𝑑 𝑏𝑙𝑢𝑒 𝑇 1 0 0 𝑇 2 0 𝑇 3 0
(We omit the insignificant values). We note a state 𝑠 = (𝑚, 𝑥, 𝑣).

The initial state is 𝑞 0 = (𝑚 0 , 𝑥 0 , 𝑣 0 ). Since the time intervals are points, we have an unique run:

1 0 1 0 0 1 0 0 , 2 1 , 0 0 0 0 5 - → 1 0 1 0 0 1 0 0 , 2 1 , 5 0 5 5 (𝑇2,•) -----→ 1 1 0 0 0 1 0 0 , 2 1 , 5 0 0 5 1 - → 1 1 0 0 0 1 0 0 , 2 1 , 6 0 0 6 (𝑇3,•) -----→ 1 1 0 0 0 0 0 0 , 2 2 , 6 0 0 0 2 - → 1 1 0 0 0 0 0 0 , 2 2 , 8 2 0 0 (𝑇1,𝑟 𝑒𝑑) -------→ 0 1 0 0 0 0 1 0 , 4 2 , 0 2 0 0 6 - → 0 1 0 0 0 0 1 0 , 4 2 , 0 8 0 0 (𝑇1,𝑏𝑙𝑢𝑒) --------→ 0 0 0 0 0 0 1 1 , 4 3 , 0 0 0 0
The time elapses from the initial marking until reaching date 5. 𝑇 2 is fired, and a blue token is dropped in the place 𝑃 1 . The clock of 𝑇 1 associated with the red color has reached the value 5. The clock of 𝑇 1 associated with the blue color cannot start yet because the guard is false for this color. At date 6, 𝑇 3 is fired, causing a change in the variable cpt that makes the guard of 𝑇 1 true for the blue color. The clock associated with the blue color for 𝑇 1 can therefore start. Both colors enable the transition 𝑇 1 , and the corresponding clocks give the time from the two enabling. After two more time units, 𝑇 1 is fired for the red color; at this moment, the clock of 𝑇 1 for the blue color has reached 2. Finally, after 6-time units, 𝑇 1 is fired for the blue color, ending the run.

Atomicity An update can be described as a sequence of imperative code expressed in a programming language such as C. This code is evaluated sequentially w.r.t. the semantics of the C language; however, its execution is considered atomic from the HCTPN point of view.

Hence, if 𝑥 and 𝑥 ′ are respectively the values of the variables before and after the execution of the code of an update of a transition 𝑡 from 𝑥, the firing of 𝑡 leads atomically to 𝑥 ′ = 𝑢 𝑝𝑑𝑎𝑡𝑒(𝑡, 𝑥).

High-level Colored Time Petri Net with stopwatches

We now consider stopwatches instead of clocks. Hence, for Colored Time Petri Nets with stopwatches, there is at most one stopwatch per color and per transition.

When using stopwatches with the HCTPN formalism, the temporal behavior differs and depends on the time derivative function 𝑣(𝑡, •) when transitions 𝑡 ∈ 𝑇 𝑎𝑛𝑦 and 𝑣(𝑡, 𝑐) for 𝑡 ∈ 𝑇 𝑎𝑛𝑦 .

The time associated with a transition can be suspended and later resumed at the same point. Moreover, transition with a 0-time derivative can not be fired. The time derivative of a stopwatch is in the rate set {0, 1} and is given by a function from Markings.

Definition 3 (High-level Colored Time Petri Net with stopwatches)

A High-level Colored Time Petri Net with stopwatches is a tuple N = (𝑃, 𝑇, pre(.), post(.), 𝑚 0 , 𝑔𝑢𝑎𝑟𝑑, 𝑢 𝑝𝑑𝑎𝑡𝑒, 𝐼, 𝑣) where (𝑃, 𝑇, pre(.), post(.), 𝑚 0 , 𝑔𝑢𝑎𝑟𝑑, 𝑢 𝑝𝑑𝑎𝑡𝑒, 𝐼) is defined in Definition 1 and 𝑣 : 𝑇 × N 𝑃×𝐶 × X 𝑋 → {0, 1} is the time derivative function.

Semantics

For the discrete transition of the semantics, the only difference with HCTPN is that a transition cannot be fired if its time derivative is not 1. For the time transition, the value of a stopwatch evolves according to its derivative as follows.

Definition 4 (Semantics of a HCTPN with stopwatches ) The semantics of a HCTPN with stopwatches is a timed transition system (𝑄, 𝑄 0 , →) where:

• 𝑄 ⊆ N 𝑃×𝐶 × X 𝑋 × R ≥0 𝑇×𝐶 • 𝑄 0 = ((𝑚 0 , 𝑥 0 ), 0) • →∈ 𝑄 × ((𝑇 × 𝐶 ∪ {•}) ∪ R ≥0 ) × 𝑄 consists

of two types of transitions:

discrete transitions (firing 𝑡 from ((𝑚, 𝑥), 𝑣)), as presented in Definition 2 with

𝑣(𝑡) = 1 -time transitions: ((𝑚, 𝑥), 𝑣) 𝑑∈R ≥0 -----→ ((𝑚, 𝑥), 𝑣 ′ ), iff: * ∀𝑡 ∈ 𝑇 𝑎𝑛𝑦 s.t. en(𝑚, 𝑡) = 𝑡𝑟𝑢𝑒, • 𝑣 ′ (𝑡, •) ≤ 𝐼 (𝑡) ↓ • 𝑣 ′ (𝑡, •) = 𝑣(𝑡, •) + 𝑑 if 𝑣(𝑡, •) = 1 otherwise 𝑣 ′ (𝑡, •) = 𝑣(𝑡, •) * ∀𝑡 ∈ 𝑇 𝑎𝑛𝑦 s.t. en(𝑚, 𝑡) = 𝑓 𝑎𝑙𝑠𝑒,
• 𝑣 ′ (𝑡, •) = 0 * ∀𝑡 ∈ 𝑇 𝑎𝑛𝑦 and ∀𝑐 ∈ colorSet any (𝑚, 𝑡),

• 𝑣 ′ (𝑡, 𝑐) ≤ 𝐼 (𝑡) ↓ • 𝑣 ′ (𝑡, 𝑐) = 𝑣(𝑡, 𝑐) + 𝑑 if 𝑣(𝑡, 𝑐) = 1 otherwise 𝑣 ′ (𝑡, 𝑐) = 𝑣(𝑡, 𝑐) * ∀𝑡 ∈ 𝑇 𝑎𝑛𝑦 and ∀𝑐 ∉ colorSet any (𝑚, 𝑡), • 𝑣 ′ (𝑡, 𝑐) = 0
We now illustrate the main features of HCTPN with stopwatches on an example.

Example of HCTPN with stopwatches

This example is the modeling of the preemptive scheduling of two tasks. The first task 𝑡𝑎𝑠𝑘 1 is a periodic task running on core 0, assigned to blue color. The second task 𝑡𝑎𝑠𝑘 2 is also periodic but is executed only 10 times on core 1, assigned to red color. The particular color any is used for enabling and firing all transitions. For the first two executions of 𝑡𝑎𝑠𝑘 2 , the priority of 𝑡𝑎𝑠𝑘 1 is higher than 𝑡𝑎𝑠𝑘 2 priority, after which it becomes the opposite.

The model in Figure 4.5 is a HCTPN with stopwatches and has a single shared variable 𝑐 𝑝𝑡 and two colors. The initial value of 𝑐 𝑝𝑡 is zero. Only the transition 𝑇 2 has a guard and an update that manipulate the 𝑐 𝑝𝑡 variable. Hence the transition 𝑇 2 is enabled if there is a token in its input place 𝑡𝑎𝑠𝑘 2 and if 𝑐 𝑝𝑡 < 10 modeling the fact that the task 𝑡𝑎𝑠𝑘 2 is executed only 10 times. The update that increments the value of 𝑐 𝑝𝑡 is executed each time the transition 𝑇 2 is fired.

The scheduling is captured by the derivative function of the stopwatches associated with 𝐶 In the sequel, a marking is written by the matrix 𝑚 = (|𝑃|, |𝐶 |). The initial marking enables the transitions 𝑇 1 and 𝑇 2 . The valuations of the stopwatches are given by the Since all the transitions are in 𝑇 𝑎𝑛𝑦 , the bullet column of the stopwatch valuations is not used. We will therefore omit it in the states of this example in order to simplify the notation.

𝑇 𝑎𝑠𝑘 1 T 1 [10, 10] 𝑅𝑒𝑎𝑑𝑦 1 C 1 [4, 6] 𝑇 𝑎𝑠𝑘 2 𝑐 𝑝𝑡 < 10 T 2 [15, 15] 𝑐 𝑝𝑡 = 𝑐 𝑝𝑡 + 1 𝑅𝑒𝑎𝑑𝑦 2 C 2 [1, 3] • • 𝑣 = 1 𝑣 = 1 𝑣 = 𝑖𝑠𝑅𝑢𝑛𝑛𝑖𝑛𝑔(𝑡𝑎𝑠𝑘 1 ) 𝑣 = 𝑖𝑠𝑅𝑢𝑛𝑛𝑖𝑛𝑔(𝑡𝑎𝑠𝑘 2 ) typedef enum { task1 , task2 } id ; int cpt = 0; int isRunning ( id task ) { if ( task == task1 ) { if (( m ( Ready2 )==1) && ( cpt >2)) return 0; else return 1; } else if ( task == task2 ) { if (( m ( Ready1 )==1) && ( cpt <3
We note a state 𝑠 = (𝑚, 𝑐 𝑝𝑡, 𝑣) and the initial state is 𝑞 0 = (𝑚 0 , 0, 𝑣 0 ), where:

𝑚 0 = 𝑟𝑒𝑑 𝑏𝑙𝑢𝑒 𝑇 𝑎𝑠𝑘 1 0 1 𝑇 𝑎𝑠𝑘 2 1 0 𝑅𝑒𝑎𝑑𝑦 1 0 0 𝑅𝑒𝑎𝑑𝑦 2 0 0
, and 𝑣 0 =

• 𝑟𝑒𝑑 𝑏𝑙𝑢𝑒 𝑇 1 0 0 0

𝑇 2 0 0 0 𝐶 1 0 0 0 𝐶 2 0 0 0 simply denoted 𝑣 0 = 𝑟𝑒𝑑 𝑏𝑙𝑢𝑒 𝑇 1 0 0 𝑇 2 0 0 𝐶 1 0 0 𝐶 2 0 0 .
Assume that the execution times of the two tasks 𝑡𝑎𝑠𝑘 1 and 𝑡𝑎𝑠𝑘 2 are respectively 5.3 and 2.4. It means that the transitions 𝐶 1 and 𝐶 2 fire when their stopwatches reach these values. Let us develop the corresponding run:

𝑞 0 = 0 1 1 0 0 0 0 0 , 0 , 0 0 0 0 0 0 0 0 10 --→ 0 1 1 0 0 0 0 0 , 0 , 0 10 10 0 0 0 0 0 (𝑇 1 ,𝑏𝑙𝑢𝑒) -------→ 𝑞 1 = 0 1 1 0 0 1 0 0 , 0 , 0 0 10 0 0 0 0 0 In 𝑞 1 , we have 𝑣(𝐶 1 , 𝑏𝑙𝑢𝑒) = 1 then 𝑞 1 5 - → 𝑞 2 = 0 1 1 0 0 1 0 0 , 0 , 0 5 15 0 0 5 0 0 (𝑇 2 ,𝑟 𝑒𝑑) -------→ 𝑞 3 = 0 1 1 0 0 1 1 0 , 1 , 0 5 0 0 0 5 0 0
In 𝑞 3 , we have 𝑣(𝐶 1 , 𝑏𝑙𝑢𝑒) = 1 and 𝑣(𝐶 2 , 𝑟𝑒𝑑) = 0 meaning that 𝑡𝑎𝑠𝑘 2 is preempted by 𝑡𝑎𝑠𝑘 1 . Then 𝑣(𝐶 2 , 𝑟𝑒𝑑) will keep its value 0 until the firing of 𝐶 1 that will change

𝑣(𝐶 2 , 𝑟𝑒𝑑). 𝑞 3 0.3 --→ 𝑞 4 = 0 1 1 0 0 1 1 0 , 1 , 0 5.3 0.3 0 0 5.3 0 0 (𝐶 1 ,𝑏𝑙𝑢𝑒) --------→ 𝑞 5 = 0 1 1 0 0 0 1 0 , 1 , 0 5.3 0.3 0 0 0 0 0 In 𝑞 5 , we have 𝑣(𝐶 2 , 𝑟𝑒𝑑) = 1 hence 𝑞 5 2.4 --→ 𝑞 6 = 0 1 1 0 0 0 1 0 , 1 , 0 7.7 2.7 0 0 0 2.4 0 (𝐶 2 ,𝑟 𝑒𝑑) -------→ 𝑞 7 = 0 1 1 0 0 0 0 0 , 1 , 0 7.7 2.7 0 0 0 0 0
For the sake of conciseness, we do not detail the following run from 𝑞 7

𝑞 7 2.3 --→ (𝑇 1 ,𝑏𝑙𝑢𝑒) -------→ 6 - → (𝐶 1 ,𝑏𝑙𝑢𝑒) --------→ 4 - → (𝑇 1 ,𝑏𝑙𝑢𝑒) -------→ (𝑇 2 ,𝑟 𝑒𝑑) -------→ 6 - → (𝐶 1 ,𝑏𝑙𝑢𝑒) --------→ 3 - → (𝐶 2 ,𝑟 𝑒𝑑) -------→ 1 - → (𝑇 1 ,𝑏𝑙𝑢𝑒) -------→ 5 - → (𝑇 2 ,𝑟 𝑒𝑑) -------→ 𝑞 13
It leads to a state 𝑞 13 that has exactly the same marking and the same value of stopwatches than 𝑞 3 but with 𝑐 𝑝𝑡 = 3.

𝑞 13 = 0 1 1 0 0 1 1 0
, 3 , 0 5 0 0 0 5 0 0 then we have 𝑣(𝐶 1 , 𝑏𝑙𝑢𝑒) = 0 and 𝑣(𝐶 2 , 𝑟𝑒𝑑) = 1 meaning that the task 𝑡𝑎𝑠𝑘 2 is not preempted by the task 𝑡𝑎𝑠𝑘 1 .

Hence we have :

𝑞 13 2.4 --→ 𝑞 14 = 0 1 1 0 0 1 1 0 , 3 , 0 7.4 2.4 0 0 5 2.4 0 (𝐶 2 ,𝑟 𝑒𝑑) -------→ 𝑞 15 = 0 1 1 0 0 1 0 0 , 3 , 0 7.4 2.4 0 0 5 0 0 .

Decidability, complexity and state space computation

Let us recall that a High-level Colored Time Petri Net (HCTPN) is a tuple N = (𝑃, 𝑇, 𝑋, 𝐶, pre, post, (𝑚 0 , 𝑥 0 ), 𝑔𝑢𝑎𝑟𝑑, 𝑢 𝑝𝑑𝑎𝑡𝑒, 𝐼) such that the set 𝐶 of colors is finite and 𝑋 is a finite set of variables taking their value in a finite set X.

Theorem 1 Reachability problem for bounded High-level Colored Time Petri Net is decidable

Proof: From HCTPN semantics, a transition can be multi-enabled a maximum of |𝐶 | times at a given time. Hence, firing domains can be symbolically abstracted with state classes using Difference Bound Matrix (DBM) over |𝐶 | × 𝑇 variables. As in [START_REF] Berthomieu | Modeling and Verification of Time Dependent Systems Using Time Petri Nets[END_REF][START_REF] Berthomieu | An Enumerative Approach for Analyzing Time Petri Nets in Information Processing[END_REF], the number of DBM is finite. Moreover, the number of markings of a k-bounded Petri net is bounded by (𝑘 + 1) |𝑃| then the number of discrete states of a k-bounded HCTPN is bounded by (𝑘 +1) |𝑃| ×X 𝑋 . Hence, computable finite abstractions of the state space exist, and the reachability problem is decidable. □

State Space Computation

A discrete state of the net N is a tuple ((𝑚, 𝑥), 𝑣) in N 𝑃×𝐶 × X 𝑋 × R ≥0
𝑇×𝐶 , where: 𝑚 is a marking, 𝑥 is a variable valuation and 𝑣 is a valuation of the clocks. Roméo computes the state-class graph (SCG) that preserve LTL properties of bounded nets [START_REF] Berthomieu | Modeling and Verification of Time Dependent Systems Using Time Petri Nets[END_REF]. It performs translations from HCTPNs to Timed Automata (TAs) that preserve the behavioural semantics (timed bisimilarity) of HCTPNs. Two distinct methods are implemented: The state-class graph [START_REF] Berthomieu | Modeling and Verification of Time Dependent Systems Using Time Petri Nets[END_REF] and the zone-based graph [START_REF] Gardey | State Space Computation and Analysis of Time Petri Nets[END_REF].

The zone-based graph method is derived from the TA framework [START_REF] Gardey | State Space Computation and Analysis of Time Petri Nets[END_REF], while the stateclass graph method is based on the classical state class graph approach [START_REF] Lime | State class Timed Automaton of a Time Petri Net in The 10th International Workshop on Petri Nets and Performance Models[END_REF]. Temporal logics were introduced by Pnueli [START_REF] Pnueli | The Temporal Logic of Programs in 18th Annual Symposium on Foundations of Computer Science[END_REF] as specification languages to express the behaviors of sequential and concurrent systems and TCTL (Timed Computation Tree Logic), introduced in [START_REF] Alur | Model-Checking in Dense Real-time[END_REF], is a real-time extension of the branching-time temporal logic CTL (Computation Tree Logic).

We can prove, as in [START_REF] Boucheneb | TCTL model checking of Time Petri Nets[END_REF] for bounded Time Petri Nets, that the theoretical complexity of TCTL model-checking for bounded High-level Colored Time Petri Nets is PSPACEcomplete. However, as for Timed Automata and Time Petri Nets, no effective PSPACE algorithm exists in practice, and real implementations are with exponential algorithms.

In practice, on-the-fly TCTL model-checking for bounded High-level Colored Time Petri Nets is proposed in the Roméo tool, used to model the Trampoline RTOS and the application in Section 4.6, page 74.

Moreover, as shown in the previous section, HCTPN can be extended with stopwatches allowing the modeling of preemptive scheduling. In the stopwatch setting, the reachability problem is undecidable but efficient semi-algorithms are implemented in Roméo [START_REF] Lime | Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches in 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems[END_REF] that converges for almost all practical cases.

Roméo tool

The Roméo tool [START_REF] Gardey | Romeo: A Tool for Analyzing Time Petri Nets in Computer Aided Verification[END_REF] is a free and open-source software developed by the real-time systems team of LS2N at École Centrale de Nantes. It allows the modeling of complex and preemptive real-time systems using the HCTPN formalism with stopwatches. It consists of a Graphical User Interface GUI (written in TCL/Tk) to edit and design TPNs and computation modules (written in C++). Roméo provides a variable 𝑎𝑛𝑦 that gives the integer value of the color used for the transition firing. The requirements in Roméo are expressed in a subclass of TCTL temporal logic [START_REF] Alur | Model-Checking in Dense Real-time[END_REF] and verified with an on-thefly efficient algorithm over bounded HCTPN. It includes parameter synthesis for the model-checking [START_REF] Lime | Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches in 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems[END_REF], allowing the computing of parameter values that guarantee the satisfaction of the property and the addition of linear constraints on the parameters to limit their domain. Roméo implements on-line simulation and reachability modelchecking of HCTPN with stopwatches.

Roméo has been used to model and analyze several interesting problems [START_REF] Andreychenko | Analyzing resilience properties in oscillatory biological systems using parametric model checking[END_REF][START_REF] Parquier | Applying Parametric Model-Checking Techniques for Reusing Real-Time Critical Systems in Formal Techniques for Safety-Critical Systems[END_REF][START_REF] Coullon | Integrated Model-Checking for the Design of Safe and Efficient Distributed Software Commissioning in Integrated Formal Methods[END_REF]. The authors in [START_REF] Andreychenko | Analyzing resilience properties in oscillatory biological systems using parametric model checking[END_REF] used parametric time model-checking to verify the time behavior of biological oscillatory systems. They focused on resilience properties which they formalized in the TCTL logic and applied to the oscillatory system of the mammalian circadian clock. Their verification is done in the Roméo tool where the properties are represented using observers modeled as parametric time Petri nets.

Application

The application chosen as an example is the modeling of the spinlocks mechanism present in the PowerPC MPC5643L dual-core microcontroller from NXP [START_REF]MPC5643L Microcontroller Reference Manual NXP[END_REF] and used to build critical sections for parallel program executions. This mechanism is based on a hardware unit, the SEMA4 for Semaphore Unit. For the software, this unit is materialized as an array of 16 registers implementing 16 locks. The exclusive access to the bus regulates the concurrent accesses to one of these registers. If a register contains the value 0, the lock is available, and it is possible to write to it. If the value contained is different from 0, the lock is occupied, and it is only possible to write the value 0 to it, and writing any other value has no effect. Therefore, getting a lock consists in writing a value different from 0 and releasing it consists in writing 0. Thus, using this unit requires respect of a protocol, and an example of implementation is given on page 1322 of [START_REF]MPC5643L Microcontroller Reference Manual NXP[END_REF]. Algorithm 1 reproduces it.

Algorithm 1 Lock acquisition protocol. 𝑔𝑎𝑡𝑒 is one of the hardware registers of the SEMA4 unit.

𝑐𝑛 ← core_number ⊲ (1 .. N) do 𝑙𝑜𝑐𝑘 ← 𝑔𝑎𝑡𝑒 while 𝑙𝑜𝑐𝑘 ≠ 0 do 𝑔𝑎𝑡𝑒 ← 𝑐𝑛 𝑙𝑜𝑐𝑘 ← 𝑔𝑎𝑡𝑒 while 𝑙𝑜𝑐𝑘 ≠ 𝑐𝑛

Modeling the spinlocks mechanism

The modeling takes advantage of the possibilities of the HCTPN. The hardware part, which by virtue of the exclusive access to the bus allows operations that are intrinsically atomic, is modeled using functions. To simplify the presentation, only one register of the SEMA4 unit, gate, is modeled but the model could just as well use an array to accurately model the hardware. The listing 4.1, page 76, shows this part of the model. gate is initialized to the UNLOCKED state (line 2) and is accessible through three functions. lock (line 4) mimics the behavior of the hardware by only allowing writing to gate if its value is UNLOCKED. The core number corresponding to a color and a color among N being coded by an integer from 0 to N-1, a core locks by writing 𝑐𝑜𝑙𝑜𝑟 + 1 in gate. unlock (line 10) simply writes the value UNLOCKED into gate. isLocked (line 14 returns 1 if the gate is locked, 0 otherwise). Finally, isLockedBy (line 22) returns 1 if core holds the lock and returns 0 otherwise.

Each function of the software is modeled by an HCTPN reproducing the control flow graph of the function. Two HCTPNs model the functions GetSpinLock and RelSpinLock (see Figure 4.6, page 77). GetSpinLock corresponds to the algorithm 1, page 74, and $any allows to represent on which core the function is executed. The call of a function modeled by a HCTPN is done by dropping a token of the core color in the initial place. Thus, "calling" the function GetSpinLock is performed by the update GetSpinLock[color ] = 1 on a transition of the HCTPN of the calling function. This is identical to drawing an arc of the corresponding color between the transition and the initial place of GetSpinLock. The function return requires a synchronization. This one is implemented by a variable of type array and of size equal to the number of colors and indexed by the color, i.e. the core on which the function call is made. We have therefore for our two function models the two variables endOfGSL and endOfRSL, see listing 4.2, page 77.

Verification of the system

The spinlock model is completed by an application model. Two tasks, 𝜏 0 , running on core 0 (red color) and 𝜏 1 , running on core 1 (blue color), are modeled as shown in Figure 4.7, page 78. The task 𝜏 0 takes then releases the spinlock while the task 𝜏 1 has the possibility to take it, as 𝜏 0 does, or to reach the final state without taking the spinlock. We want to check that 𝜏 0 and 𝜏 1 cannot occupy simultaneously and respectively the places P 12 and P 22 by the CTL formula 𝐴□(¬(P 12 [0] == 1∧P 22 [ denotes the marking of P 12 for the red color and P 22 [START_REF]Avionics Application Software Standard Interface, Part 1[END_REF] denotes the marking of P 22 for the blue color. Roméo answers true for this CTL formula.

Conclusion

This chapter has presented High-level Colored Time Petri Nets. This formalism allows to model complex systems and is well adapted to multi-core hardware and software modeling, as shown in the case study. The high-level features allow the modeling of the software, the timed transitions model the execution times, the colors specify the hardware where the software is executed, and preemption is supported by means of stopwatches. A timed transition enabled by more than one color allows true concurrency modeling. The model-checking of this extended formalism is implemented in the Roméo tool. The next chapter focuses on using this formalism to model the RTOS.

MODELING WITH HIGH LEVEL COLORED PETRI NETS

Introduction

This chapter presents the Trampoline model built in its multi-core version with fixed priority partitioned scheduling for the tasks. The model consists of the same variables and data structures found in the Trampoline source code as well as a HCTPN representing the control flow. The source code that includes 180 functions for the targetindependent part is modeled by a systematic approach based on the HCTPN translation rules in Roméo tool 4.5. The model contains 115 Petri sub-networks that form a single one. It includes 600 transitions, 550 places, 162 constants, and other data structures and variables generated automatically in the GOIL compilation phase, as shown in figure 3.6, page 44, using a developed Goil Template Language (GTL) module.

Modeling rules

We apply the following modeling principles:

• Each Petri subnet describes a function of the operating system and faithfully describes its control flow;

• The variables and structures used in the model are the same as those of the operating system;

• Actions and conditions on variables in the model are those of the operating system control;

• The Petri net transitions include the same assignment instructions and other imperative operations as those present in the source code;

• Pointers are replaced by arrays in the model;

• The processor cores are represented one-to-one by the token colors in the model;

• All kernel transitions are fired in a time interval [0, 0] because (i) the time is not necessary for the modeling of the kernel, (ii) the knowledge of the time would apply only to a precise hardware target, and the genericity of the model would be lost, (iii) it is necessary to capture all the possible interleavings and some of them could be cancelled by real-time constraints;

• The application model is described by API function calls;

• Functions that do not require fine-grained modeling checking instruction by instruction (e.g., functions that initialize or increment variables or results and error comparison functions) are written in the C-like Roméo language and are associated with single transitions in the model.

Function call

The function call synchronization is done by tokens deposited in places, indexed by the variable 𝑎𝑛𝑦 representing the core identifier on which the call is made. The calling function drops a token in the initial place of the Petri subnet modeling the called function. A guard on the token blocks the execution of the calling Petri subnet.

Once the called Petri subnet completes its execution, the calling Petri subnet is released.

The token is finally consumed to avoid accumulation in the last place, causing an unbounded Petri net. The Figure 5.1 presents the mechanism. Without changing the semantics of HCTPN, it is possible to update the number of tokens in a place without explicitly drawing an arc between a transition and a place. This feature is used to lighten the design of the model. The model is thus drawn in the form of Petri subnets which appear independent but which, in reality, form only one.

Atomic modeling

The code associated with a transition in a HCTPN is executed sequentially and considered atomic in the state space, i.e., if several variables are updated on a transition, the intermediate state(s) are not present. This code can be one or a sequence of instructions, and it can also be a function call written in the C-like Roméo language. In the modeling step, the association of an instruction sequence or a C-like function call to a transition reduces the state space. The execution of the function call associated with a transition is also considered atomic in the modeling. An update can is locked during its execution → the global lock is then taken to prevent competitive situations between the cores in the kernel. All the services of the API layer are modeled with HCTPNs in the same manner. The first transition of the model describes that when an API function is called to execute the requested service, the core switches from user mode to kernel mode using the 𝑘𝑒𝑟𝑛𝑒𝑙_𝑚𝑜𝑑𝑒 array. This passage is local to this core, hence the array 𝑘𝑒𝑟𝑛𝑒𝑙_𝑚𝑜𝑑𝑒 is indexed by $𝑎𝑛𝑦. The variable $𝑎𝑛𝑦 gives the value of the color used for the transition firing. Thus, the transition firing can be performed simultaneously for different cores. The global lock variable 𝑙𝑜𝑐𝑘_𝑘𝑒𝑟𝑛𝑒𝑙 is a shared variable that prevents simultaneous service calls by different cores. When the API function completes its execution, it unlocks the kernel (𝑙𝑜𝑐𝑘_𝑘𝑒𝑟𝑛𝑒𝑙 = 0), and another service can then be called → it finally leaves the kernel mode (𝑘𝑒𝑟𝑛𝑒𝑙_𝑚𝑜𝑑𝑒[$𝑎𝑛𝑦] = 0). Let us consider the API GetAlarmBase and ActivateTask services as examples.

GetAlarmBase service This service allows to obtain the requested information on the alarm base and store it in a global variable. An error is returned if the alarm identifier is invalid. This service call model is shown in Figure 5. ActivateTask service This API service allows the activation of a task. Figure 5.3 shows its modeling. The Petri subnet's first place represents the function's initial location, and each transition describes the execution state of the function. Upon calling this Petri subnet, it calls the kernel function tpl_activate_task_service to execute the requested service. tpl_activate_task_service function is itself modeled by a Petri subnet.

Kernel modeling

The Kernel contains all the low-level functions on which the Trampoline services are based as represented in 3.5.2. It ensures the start and shutdown of the OS and allows the activation of tasks, their scheduling, and their synchronization. The kernel model

Task manager

The task manager contains the function models that manage the application tasks' activation, synchronization, and termination. They also perform scheduling and context switches if necessary. All the functions contained in the task manager are modeled. It includes the function models tpl_activate_task_service and tpl_terminate_task_service, responsible for activating and terminating a task and setting its state, respectively. To terminate the running task, the function tpl_terminate_task_service first performs some checks about interrupts, spinlocks, the task's level, and resource, then decrements the activation count, calls the kernel function tpl_terminate_task, performs the rescheduling and context switch and finally ends the task being executed.

The modeling of the task manager function tpl_terminate is shown in Figure 5.4. This kernel function performs a release of the internal resource held by the task by calling the tpl_release_internal_resource function. A guard on the activation counter allows the running task state to be set either to READY_AND_NEW2 or SUSPENDED state. Also, the events associated with the extended tasks are initialized. Scheduler The scheduler model is the core module of the kernel; it is based on the one proposed by the OSEK/VDX and AUTOSAR standards. The multi-core version of Trampoline implements a fixed priority partitioned scheduler. The scheduler uses functions to handle the list of ready tasks and ISRs of category 2. Among the functions, we can highlight the tpl_put_new_proc function, explained in 3.5.2. Its model is presented in Figure 5.5. The function starts its execution by calling some initialization functions written in the Roméo language. GET_PROC_CORE_ID (Figure 5.6) initializes the variable core_id_var with the core_id assigned to the process passed as an argument. The core_id is obtained from the process static descriptor stored in a table. GET_CORE_READY_LIST initializes the ready_list belonging to the core core_id. The structure ready_list is a binary heap. Each element has two fields, the dynamic process priority (key) and the process identifier (id). The key is the concatenation of the priority and the rank of the job. Finally, GET_TAIL_FOR_PRIO initializes the tail_for_prio with the rank table of core core_id. tail_for_prio stores the last rank used to store a process. The variable $𝑎𝑛𝑦 represents the core_id of the running core. The second transition represents the dynamic priority calculation, obtained by concatenating the static priority and an order number per priority level. PRIORITY_SHIFT is used to shift the key part used to store its priority and RANK_MASK to get the part of the key used to store its rank. Then the new entry is added at the end of the ready list, and the tpl_bubble_up 3 subnet is called to bubble the entry at the index place up in a heap.

Interrupt dispatcher

The model of this component is built with a subnet, allowing the management of software and hardware interrupts. To notify an interruption, a token with a color corresponding to the target core is put in the tpl_it_handler first place, represented in Figure 5.7. Then interrupts are masked on the core (kernel_mode[$any]=1), the global lock is taken if possible (lock_kernel=1). The different requests from the interrupts are not considered until the called services leave the kernel mode. The counter manager is called when the interrupt source is the counter tick. The inter-core interrupt manager is called to handle the interactions and communication between the cores. The central interrupt handler is called to manage the ISR. Next, the interrupt handler interacts with the scheduler and the context switch manager if the triggered interrupt causes the running task to lose the processor. Finally, the global lock is released, and the core returns to user mode, unmasking interrupt consequently.

Counter manager

The counter manager model handles any interruptions coming from the timer. When an interrupt occurs, the action related to the set of expiring alarms is 3. The tpl_bubble_up function compares the added element with its parent; if they are in the correct order, the operation stops. If not, the element is swapped with its parent, and the operation returned to the previous comparison step. executed. The action of the alarm can correspond to the activation of a task, an event, or a call-back function. The interrupt can also cause a rescheduling. Alarms and counters are defined statically according to the OSEK/VDX and AUTOSAR standards. In the model, tpl_call_counter_tick increments the counter tick and checks the next alarm date. tpl_raise_alarm model describes when an alarm time object is raised.

Alarm base information can be obtained through the tpl_get_alarm_base_service kernel function called by the GetAlarmBase API service (Figure 5.2). Figure 5.8 presents this HCTPN model that provides information on the alarm base. The Petri subnet also checks if the interrupts are not disabled by the user when calling an API service and that the alarm_id is a valid alarm identifier using function calls written in the Roméo language.

uninterruptible code executed in kernel mode in null time. Hence, the state space of the complete model abstracts the state space of the kernel. We then have the following proposition: Proposition 1: Modulo atomicity, the formal model N and the RTOS kernel have the same state space over the RTOS variables. It means that as in [START_REF] Tigori | Formal Model-Based Synthesis of Application-Specific Static RTOS[END_REF], for any application, N contains all the paths that might be traversed during the execution of the operating system program. It is important to note that for another version of the OS kernel without global lock, it would be necessary to ensure that the reading and writing of a global variable are not on the same transition. Property 1: The model N of the kernel is bounded. Proof: The variables manipulated by the kernel (and then by the model N ) take their values in a finite set, i.e., either bounded integers (such as the value of task priority) or enumerated types (such as the state of a task). Moreover, the program pointers have a finite number of values; hence the markings are bounded and then also the model N . □

Application modeling

To perform verifications, it is necessary to add an application model to the RTOS model. An application contains a concurrent set of tasks that interact with the operating system through system calls such as ActivateTask() or TerminateTask(), interspersed with execution times given as an interval [𝐵𝐶𝐸𝑇, 𝑊𝐶𝐸𝑇]4 . Its model consists of two parts. The first part is the set of data structures corresponding to the descriptors of the different objects that appear in the application: task, alarms, spinlocks, etc. The attributes of the objects constitute part of the model variables. These data structures are transposed from the C language to Roméo's language, the model-checker that we use, which in its syntax is very close to the C language. The pointers sometimes used in these structures are translated into indexes in arrays. In practice, we added a module to the Trampoline OIL compiler to automatically generate the structures used by Roméo from the OIL description of the application, as shown in Figure 5

𝑖𝑠𝑅𝑢𝑛𝑛𝑖𝑛𝑔(𝑡𝑎𝑠𝑘 𝑖

) of the stopwatches associated with the transitions representing the execution of the tasks between services calls. When the task 𝑡𝑎𝑠𝑘 𝑖 is scheduled, and the OS is not running, then the function 𝑖𝑠𝑅𝑢𝑛𝑛𝑖𝑛𝑔(𝑡𝑎𝑠𝑘 𝑖 ) returns 1, allowing the time to elapse; otherwise, it returns 0 and blocks the elapse of time.

The GTL module

Goil compiler includes a template interpreter for file generation. Figure 5.9 shows templates with the extension .𝑔𝑜𝑖𝑙𝑇 𝑒𝑚 𝑝𝑙𝑎𝑡𝑒. These template files are created in the Goil Template Language (GTL), which allows the application's configuration data to be combined with text to generate files. GTL supports types (struct, boolean, list, integer, and string) and has readers to get variable information. The syntax of this language is detailed in the Trampoline OS documentation in the git 5 . The added GTL module is a set of template files that produces the Roméo file. A piece of code from the GTL module and the generated output file tpl_init_romeo.c after compilation are shown in Figure 5.10. The % character is used to switch from literal text mode to program mode. The module comprises descriptors templates in its root that output the C-like Roméo file. The write statement defines the output of the template processing in the specified file. Thus, we automatically extract the data structures and constants generated from the OIL description of the application and translate these structures into C-like language. Once the configuration file is defined, we model the application's source code by a Petri subnet which describes all the system calls performed.

Modeling examples

An example of modeling an application task is shown in Figure 5.11. The task calls the GetAlarmBase service, which provides information on the alarm base. The 𝐼𝑠𝑅𝑒𝑎𝑑𝑦(𝑡𝑎𝑠𝑘 𝑖 ) guards on Act 𝑡𝑎𝑠𝑘 𝑖 means that the task model is ready for execution. The 𝐼𝑠𝑅𝑢𝑛𝑛𝑖𝑛𝑔() derivative function associated with transitions returns 1 when the task 𝑡𝑎𝑠𝑘 𝑖 is scheduled on the assigned core, and we are in the user mode (kernel_mode==0). The transitions with intervals of the form [𝐵𝐶𝐸𝑇, 𝑊𝐶𝐸𝑇] allows checking the application schedulability and temporal properties, as we will explain in chapter 7. Figure 5.12 shows a modeling example of a two-tasks application. It represents a task activation on another core. 𝑡𝑎𝑠𝑘 1 is automatically activated and runs on core 0, associated with the red color. 𝑡𝑎𝑠𝑘 2 runs on core 1, which is associated with the blue color. Applications are modeled with the same approach. The IsRunning() derivative function checks that the task passed in the parameter is running in user mode, and its boolean return allows the elapse of time when it is equal to 1; otherwise, it's blocked. 𝑡𝑎𝑠𝑘 1 is running on core 0 and after a time in the range [START_REF] Group | OSEK/VDX Operating System Specification tech[END_REF]4], 𝑡𝑎𝑠𝑘 1 activates 𝑡𝑎𝑠𝑘 2 on core 1. In this case, the Biglock is taken by core 0 when the ActivateTask service is called, and core 1 waits actively for its release to take over the interrupt and make the context switch. In the model, handling the concurrency of service calls in parallel on different cores is represented by the lock_kernel variable. It is set to 1 and reset to 0 at the end of the execution of each service call. Since the interrupts are masked and can not run concurrently, a kernel_mode table is used, allowing simultaneous access through the $any variable.

Conclusion

At the end of our modeling work, we have a model of the Trampoline multi-core RTOS that we can complement with an application model. This model is described by HCTPNs and Roméo functions written in a syntax similar to the C language. The model is struc-

𝑇 𝑎𝑠𝑘 1 Run 11 𝑣 = 𝐼𝑠𝑅𝑢𝑛𝑛𝑖𝑛𝑔(𝑡𝑎𝑠𝑘 1 ) [2, 4] Run 12 𝑣 = 𝐼𝑠𝑅𝑢𝑛𝑛𝑖𝑛𝑔(𝑡𝑎𝑠𝑘 1 ) [0, 0] ActivateTask[$𝑎𝑛𝑦]::P1++ task_var[$𝑎𝑛𝑦]=task2_descriptor caller_var[$𝑎𝑛𝑦]=task1_descriptor Run 13 𝑣 = 𝐼𝑠𝑅𝑢𝑛𝑛𝑖𝑛𝑔(𝑡𝑎𝑠𝑘 1 ) [1, 1] Run 14 𝑣 = 𝐼𝑠𝑅𝑢𝑛𝑛𝑖𝑛𝑔(𝑡𝑎𝑠𝑘 1 ) [0, 0] TerminateTask[$𝑎𝑛𝑦]::P1++ caller_var[$𝑎𝑛𝑦]=task1_descriptor IsReady(𝑡𝑎𝑠𝑘 1 ) Act 𝑡 𝑎𝑠𝑘 1 [0, 0] • 𝑇 𝑎𝑠𝑘 2 Run 21 [1, 2] 𝑣 = 𝐼𝑠𝑅𝑢𝑛𝑛𝑖𝑛𝑔(𝑡𝑎𝑠𝑘 2 ) Run 22 [0, 0] TerminateTask[$𝑎𝑛𝑦]::P1++ caller_var[$𝑎𝑛𝑦]=task2_descriptor 𝑣 = 𝐼𝑠𝑅𝑢𝑛𝑛𝑖𝑛𝑔(𝑡𝑎𝑠𝑘 2 ) IsReady(𝑡𝑎𝑠𝑘 2 ) Act 𝑡 𝑎𝑠𝑘 2 [0, 0] • Figure 5
.12: Application model. tured to avoid state explosion with parts corresponding to a sequential code execution treated as an atomic transition w.r.t. the higher-level net. The entire model will be used in our verification approach presented in the following chapters.

Complete system model

RTOS model

Application model

Model-checker TCTL properties

Satisfied properties

Unsatisfied properties

Counter-example Observer models parameters, leading to nested properties where one property is defined inside another. The Roméo tool does not support this kind of formula, which motivates our choice to use observers. Indeed, the expression of the requirements is systematically performed through an observer. The verification is therefore achieved by a reachability test on a given observer state. Observers are read-only processes that keep track of some invariants in the execution of the Petri Net, and do not modify the system state. The AUTOSAR requirements are thus translated into observers describing the expected behavior. Then, with the help of reachability properties written in TCTL logic, we can verify by the model-checker their satisfaction or generate, on the contrary case, a counter-example trace.

AUTOSAR OS tests

The operating system compliance with the AUTOSAR standard is determined at the end of the test suite that comprises a set of applications. The application is a test sequence containing a set of service calls, and each service call represents a test case. When all test cases succeed, the test sequence is verified. Similarly, all test sequences completed correctly lead to the success of the test suite, thus checking the conformance. We rely on the set of multi-core test cases developed by the Trampoline project to verify the OS compliance with the AUTOSAR standard. The project is available in the Trampoline repository 1 , and it contains 75 OS-specific tests, of which 18 are dedicated to multi- core. These included test sequences have been run on several hardware targets showing Trampoline RTOS compliance. We illustrate the first AUTOSAR test sequence of the Trampoline repository, 𝑚𝑐_𝑎𝑙𝑎𝑟𝑚_𝑠1, in Figure 6.2. This example contains a set of three tasks 𝜏 = {𝑡1, 𝑡2, 𝑠ℎ𝑜𝑢𝑙𝑑_𝑛𝑜𝑡_𝑟𝑢𝑛} to be executed on two cores (Core 0 and Core 1), and three alarms assigned to Core 0, Λ= {𝑎𝑐𝑡𝑖𝑣𝑎𝑡𝑒_𝑡𝑎𝑠𝑘_𝑎𝑐𝑐𝑟𝑜𝑠𝑠_𝑐𝑜𝑟𝑒𝑠, 𝑠𝑒𝑡_𝑒𝑣𝑒𝑛𝑡_𝑎𝑐𝑐𝑟𝑜𝑠𝑠_𝑐𝑜𝑟𝑒𝑠, 𝑠ℎ𝑜𝑢𝑙𝑑_𝑛𝑜𝑡_𝑒𝑥 𝑝𝑖𝑟𝑒}. Since the 𝑠ℎ𝑜𝑢𝑙𝑑_𝑛𝑜𝑡_𝑟𝑢𝑛 task does not run, it is not shown on the figure 6.2. This sequence was developed to verify the AUTOSAR requirements from 𝑆𝑊 𝑆_𝑂𝑠_00632 to 𝑆𝑊 𝑆_𝑂𝑠_00640 in Table A.1, shown on page 147. We detail our verification approach on this application in 6.3.1.

AUTOSAR requirements observers

According to our approach, each AUTOSAR requirement is formalized by an observer able to assess its compliance; therefore, the AUTOSAR specifications are individually verified by model-checking on an application. The observer is modeled by a Petri net that evolves according to the operating system evolution without altering its behavior. The reachability of the observer's states is examined to verify the satisfaction of the trampoline/tree/master/tests/functional requirement.

How an observer works in the model? The observer relies on functions written in Roméo language, returning a boolean according to the satisfaction of the conditions forming the requirement. The observer waits in its initial state containing a token until the condition becomes true to evolve and fire its transitions. Thus, each requirement is translated by a test function that returns 𝑡𝑟𝑢𝑒 for each satisfied condition. If the first condition is true, the observer model moves to the next state to check the second condition until reaching the final state. These functions are called in the RTOS model at locations updating the data structures involved in the verification. Correct verification of future states is ensured by resetting the rest of the conditions once the first one is true.

Requirement observer model Let's consider the observer model of the 𝑆𝑊 𝑆_𝑂𝑠_00639 requirement (Figure 6.3), which verifies that the 𝐺𝑒𝑡 𝐴𝑙𝑎𝑟𝑚𝐵𝑎𝑠𝑒 service shall also work on an alarm that is bound to another core. This requirement is checked using two conditions during the service call. First, we check whether the core to which the alarm is statically assigned differs from the core identifier on which the service is executed. Then, we verify that the service call finalized its execution and exited the kernel mode. Thus, the test function is called at the beginning and end of the service call using 𝑎𝑛𝑦 that represents the 𝑐𝑜𝑟𝑒_𝑖𝑑. The final state of the observer is reached only if both conditions are satisfied. All the observers used are based on the same structure. They contain only committed transitions that are transitions with a priority to guarantee they are fired before all the other system transitions. Thus, if there are several fireable transitions at a given state of execution, the committed ones are fired first before all the others.

Model-checking with Roméo

Model-checking allows the exploration of the system's state space from its initial state, taking as input a logic formula to be verified. Requirement in Roméo are expressed in a subclass of TCTL temporal logics [START_REF] Alur | Model-Checking in Dense Real-time[END_REF] and verified with an on-the-fly efficient algorithm as represented in 4.5. An execution trace is automatically generated as a counterexample if the property violation is detected. The AUTOSAR requirement verification is performed using the logical formula 𝐴𝐺 ( 𝑝) implies 𝐴𝐹 (𝑞), expressed by the syntax (p)->(q). The formula (p)->(q) holds if and only if whenever p holds, eventually q will hold. Thus, based on the observer model of the 𝑆𝑊 𝑆_𝑂𝑠_00639 requirement (Figure 6.3), the corresponding verification formula is as follows:

(SWS_Os_00639[0])->(Kernel_exit[0]
). The token in the initial place of the model triggers the observer once the guard condition is satisfied.

Compliance of the AUTOSAR Trampoline OS

The enriched model with observers allows checking AUTOSAR requirements on any application, as each observer represents a specification. We focus on the set of multicore test sequences proposed by the Trampoline project to conduct a formal verification with the Roméo model-checker. The observers are modeled following the procedure detailed in the previous section. We illustrates the application of our formal verification approach on the two applications 𝑚𝑐_𝑎𝑙𝑎𝑟𝑚_𝑠1 and 𝑚𝑐_𝑠𝑝𝑖𝑛𝑙𝑜𝑐𝑘_𝑠1 of the Trampoline AUTOSAR test repository with the verification results obtained. These examples include several test cases that verify the satisfaction of a set of requirements related to alarms and spinlocks. The application model is constructed for each test sequence to verify the whole multi-core requirements.

mc_alarm_s1 application

This part focuses on the first multi-core test sequence of the Trampoline repository, 𝑚𝑐_𝑎𝑙𝑎𝑟𝑚_𝑠1, represented in Figure 6.2. Tasks are partitioned such that 𝑡2 runs on Core 1, while 𝑡1 and 𝑠ℎ𝑜𝑢𝑙𝑑_𝑛𝑜𝑡_𝑟𝑢𝑛 run on Core 0 and task 𝑡1 has a lower priority than task 𝑠ℎ𝑜𝑢𝑙𝑑_𝑛𝑜𝑡_𝑟𝑢𝑛.

Initially, 𝑡1 is an autostart task that runs on Core 0 in the RTOS startup phase. This task calls the API service 𝑆𝑒𝑡 𝐴𝑏𝑠𝐴𝑙𝑎𝑟𝑚 and 𝑆𝑒𝑡 𝑅𝑒𝑙 𝐴𝑙𝑎𝑟𝑚. 𝑆𝑒𝑡 𝐴𝑏𝑠𝐴𝑙𝑎𝑟𝑚( 𝐴𝑙𝑎𝑟𝑚𝐼 𝐷, 𝑠𝑡𝑎𝑟𝑡, 𝑐𝑦𝑐𝑙𝑒) activates the task 𝑡2 assigned to alarm 𝑎𝑐𝑡𝑖𝑣𝑎𝑡𝑒_𝑡𝑎𝑠𝑘_𝑎𝑐𝑟𝑜𝑠𝑠_𝑐𝑜𝑟𝑒𝑠 when its absolute value in 𝑠𝑡𝑎𝑟𝑡 ticks is reached. If the alarm is single, 𝑐𝑦𝑐𝑙𝑒 is equal to zero; otherwise, the 𝑐𝑦𝑐𝑙𝑒 value is greater than 0 in the case of a cyclic alarm. Core 0 must then acquire the kernel lock and set alarm 𝑎𝑐𝑡𝑖𝑣𝑎𝑡𝑒_𝑡𝑎𝑠𝑘_𝑎𝑐𝑟𝑜𝑠𝑠_𝑐𝑜𝑟𝑒𝑠. When it expires, the rescheduling is done for Core 1, and as a result, a context switch notification is sent with an inter-core interrupt to execute task 𝑡2. The 𝑆𝑒𝑡 𝐴𝑏𝑠𝐴𝑙𝑎𝑟𝑚 service call will verify the 𝑆𝑊 𝑆_𝑂𝑠_00632 requirement, checking if an alarm can activate a task on a different kernel. The 𝑠𝑒𝑡_𝑒𝑣𝑒𝑛𝑡_𝑎𝑐𝑟𝑜𝑠𝑠_𝑐𝑜𝑟𝑒𝑠 alarm activates the assigned event for task 𝑡2 considered as an extended task with the 𝑆𝑒𝑡 𝑅𝑒𝑙 𝐴𝑙𝑎𝑟𝑚( 𝐴𝑙𝑎𝑟𝑚𝐼 𝐷, 𝑖𝑛𝑐𝑟𝑒𝑚𝑒𝑛𝑡, 𝑐𝑦𝑐𝑙𝑒) service call, after 𝑖𝑛𝑐𝑟𝑒𝑚𝑒𝑛𝑡 ticks have elapsed. Once the interrupt sent by Core 0 is considered, task 𝑡2 starts executing and calls the following services for the 𝑠ℎ𝑜𝑢𝑙𝑑_𝑛𝑜𝑡_𝑒𝑥 𝑝𝑖𝑟𝑒 alarm:

𝑆𝑒𝑡 𝐴𝑏𝑠 𝐴𝑙𝑎𝑟𝑚, 𝐶𝑎𝑛𝑐𝑒𝑙 𝐴𝑙𝑎𝑟𝑚, 𝑆𝑒𝑡 𝑅𝑒𝑙 𝐴𝑙𝑎𝑟𝑚, and 𝐺𝑒𝑡 𝐴𝑙𝑎𝑟𝑚𝐵𝑎𝑠𝑒 (Figure 5.2), ending with the event waiting. Task 𝑠ℎ𝑜𝑢𝑙𝑑_𝑛𝑜𝑡_𝑟𝑢𝑛 assigned to alarm 𝑠ℎ𝑜𝑢𝑙𝑑_𝑛𝑜𝑡_𝑒𝑥 𝑝𝑖𝑟𝑒 will never be executed on Core 1 as the alarm is canceled at the end of the test sequence. This service calls set ensures that they work when an alarm occurs on a different core.

Application model

The developed application model precisely describes the life cycle of each task through the performed system calls. Figure 6.4 shows the test sequence of task 𝑡1. This task allows activating 𝑡2 through the expiration of alarm 𝑎𝑐𝑡𝑖𝑣𝑎𝑡𝑒_𝑡𝑎𝑠𝑘_𝑎𝑐𝑟𝑜𝑠𝑠_𝑐𝑜𝑟𝑒𝑠 and setting its event by alarm 𝑠𝑒𝑡_𝑒𝑣𝑒𝑛𝑡_𝑎𝑐𝑟𝑜𝑠𝑠_𝑐𝑜𝑟𝑒𝑠. Alarm 𝑎𝑐𝑡𝑖𝑣𝑎𝑡𝑒_𝑡𝑎𝑠𝑘_𝑎𝑐𝑟𝑜𝑠𝑠_𝑐𝑜𝑟𝑒𝑠 is enabled by the 𝑆𝑒𝑡 𝐴𝑏𝑠𝐴𝑙𝑎𝑟𝑚 system call, taking as parameters the required alarm and the expected absolute value to reach for expiry through the alarm_var and start_var variables, respectively. The 𝑡2 test sequence is modeled similarly based on the called services.

Verification results

We apply our verification approach to check the requirements covered by this example. We formalize each requirement by an observer model as presented in 6.2.2. For example, the first requirement 𝑆𝑊 𝑆_𝑂𝑠_00632 is represented by the observer model in Figure 6.5. It verifies that an alarm can activate a task on a different core. Thus, we must check that alarm 𝑎𝑐𝑡𝑖𝑣𝑎𝑡𝑒_𝑡𝑎𝑠𝑘_𝑎𝑐𝑟𝑜𝑠𝑠_𝑐𝑜𝑟𝑒𝑠 assigned to core 0 can activate task 𝑡2 on Core 1. This alarm is set by the service 𝑆𝑒𝑡 𝐴𝑏𝑠𝐴𝑙𝑎𝑟𝑚 that task 𝑡1 calls, as shown in the model in Figure 6.4. We first verify that the alarm core ID and the task core ID are distinct, then we ensure that the task is correctly activated on Core 1. Two states are observed by the function: the ready state when the task is elected and the running state when it is in execution. Finally, the kernel-mode exit condition is verified after the activation of the task. Table 6.1 shows the verification results of the requirements covered by this application, listed in Table A.1. The column 𝑡𝑖𝑚𝑒 (s) refers to the time needed to obtain the model-checker's response. The 𝑚𝑒𝑚𝑜𝑟 𝑦 (MB) column is the memory consumed when checking the property (p)->(q) of the observer corresponding to a requirement. The result column shows that the property is satisfied by the model. The requirements verification is performed in a similar time and memory. For all verifications, the result is true.

mc_spinlock_s1 application

The AUTOSAR standard defines the spinlock mechanism for tasks and ISR2s with several locking methods. For example, with the method 𝐿𝑂𝐶𝐾_𝑊 𝐼𝑇 𝐻_𝑅𝐸 𝑆_𝑆𝐶𝐻𝐸 𝐷𝑈 𝐿𝐸 𝑅, the specific pre-declared resource 𝑅𝐸 𝑆_𝑆𝐶𝐻𝐸 𝐷𝑈 𝐿𝐸 𝑅 is obtained, and all other processes will be prevented from preempting for the time that the resource is held. Following the methods 𝐿𝑂𝐶𝐾_𝐴𝐿𝐿_𝐼 𝑁𝑇 𝐸 𝑅𝑅𝑈𝑃𝑇 𝑆 or 𝐿𝑂𝐶𝐾_𝐶 𝐴𝑇2_𝐼 𝑁𝑇 𝐸 𝑅𝑅𝑈𝑃𝑇 𝑆, all interrupts or OS interrupts are suspended, respectively. Tasks and ISR2s can simultaneously access the kernel by calling spinlock services on different cores. Only one core can acquire a specific spinlock with the 𝐺𝑒𝑡𝑆 𝑝𝑖𝑛𝑙𝑜𝑐𝑘 or 𝑇𝑟 𝑦𝑇 𝑜𝐺𝑒𝑡𝑆 𝑝𝑖𝑛𝑙𝑜𝑐𝑘 API services.

𝐺𝑒𝑡𝑆 𝑝𝑖𝑛𝑙𝑜𝑐𝑘 (𝑆 𝑝𝑖𝑛𝑙𝑜𝑐𝑘 𝐼𝑑) allows the spinlock to be occupied by the calling core. If another core had already taken the spinlock, the tasks or ISR2s wait in a loop, repeatedly checking for the shared lock to become free. 𝑇𝑟 𝑦𝑇 𝑜𝐺𝑒𝑡𝑆 𝑝𝑖𝑛𝑙𝑜𝑐𝑘 (𝑆 𝑝𝑖𝑛𝑙𝑜𝑐𝑘 𝐼𝑑, 𝑠𝑢𝑐𝑐𝑒𝑠𝑠) is similar to 𝐺𝑒𝑡𝑆𝑃𝑖𝑛𝑙𝑜𝑐𝑘, except the busy-waiting if a different core acquires the spinlock. Thus, TryToGetSpinlock returns without waiting for the spinlock release, setting its return variable 𝑠𝑢𝑐𝑐𝑒𝑠𝑠 to 𝑇 𝑅𝑌𝑇𝑂𝐺𝐸𝑇 𝑆𝑃𝐼 𝑁 𝐿𝑂𝐶𝐾_𝑁𝑂𝑆𝑈𝐶𝐶𝐸 𝑆𝑆. The spinlock previously taken by the 𝐺𝑒𝑡𝑆 𝑝𝑖𝑛𝑙𝑜𝑐𝑘 and 𝑇𝑟 𝑦𝑇 𝑜𝐺𝑒𝑡𝑆 𝑝𝑖𝑛𝑙𝑜𝑐𝑘 services is released using the 𝑅𝑒𝑙𝑒𝑎𝑠𝑒𝑆 𝑝𝑖𝑛𝑙𝑜𝑐𝑘 (𝑆 𝑝𝑖𝑛𝑙𝑜𝑐𝑘 𝐼𝑑) service. We present in Figure 6.6 the 𝑚𝑐_𝑠𝑝𝑖𝑛𝑙𝑜𝑐𝑘_𝑠1 multi-core test sequence of the Trampoline repository. The application contains four spinlocks handled by the services mentioned concurrent events are enumerated in the state space, which makes its size vary exponentially. If this size exceeds the amount of computer memory, the exhaustive verification fails. The response time of the model-checker represents the time needed to explore the set of state spaces and check the property. All AUTOSAR multi-core operating system specifications were met for the modeled test applications2 , and the verification time is between 2.7 and 11 seconds consuming between 100 and 600 MB of memory. Several factors helped prevent the exponential computation time or memory size explosion. Among them are the model atomicity, the sequential access to the kernel through a global lock, except for the spinlock services where the cores can access simultaneously, the complexity of the application, and its small number of cores. The approach is efficient for AUTOSAR compliance testing.

Formal verification of concurrency in multi-core implementation

This section presents the formal verification of the Trampoline multi-core RTOS in concurrent situations using the model-checker Roméo. Since the test sequences derived from the AUTOSAR requirements for Trampoline do not allow the testing of concurrency situations, they cannot be used as is. Indeed, the multi-core system call lets us suppose that a problem could occur when services are called simultaneously on two or more cores (3.5.2). We can verify that it is probably not enough to protect access to the OS data structures (the list of ready tasks and the structure tpl_kern) through the Biglock. Indeed, the structure tpl_kern allows communication between the core where the rescheduling is performed and the core where the context switch is performed, and the example of Figure 3.12 suggests that a problem could occur when services are called concurrently on two or more cores. We thus propose to use model-checking to verify the communication and synchronization mechanisms involved in the concurrent execution of OS services by an application: concurrent accesses to OS data structures, multi-core scheduling, and inter-core interrupt handling. The application can implement, for example, a cruise control system in the vehicle. This system consists of several runnables responsible for data acquisition, diagnostics, and vehicle speed control. A task comprises runnables that must be performed according to a priority level. Its non-termination can cause severe consequences and should be avoided even in rare situations. Our goal is now to study situations with simultaneous service calls in parallel on several cores that are almost impossible to test on real implementation but that we will be able to obtain by our model-checking approach. Therefore, in order to prove that concurrent execution of services is error-free, we have designed several case studies. In the following, we present two of them that led us to identify two errors in the multi-core implementation of Trampoline.

Case study 1

To check for concurrent system calls on cores, we consider the system in Figure 6.9 which includes all possible interleaving by setting all transitions in the interval [0, 0]. It represents an activation of a higher priority task 𝑃𝑟𝑖𝑜(𝑡𝑎𝑠𝑘 1 ) < 𝑃𝑟𝑖𝑜(𝑡𝑎𝑠𝑘 3 ) < 𝑃𝑟𝑖𝑜(𝑡𝑎𝑠𝑘 2 ).

Once the autostart 𝑡𝑎𝑠𝑘 1 is started on core 0 at system start-up time, it activates 𝑡𝑎𝑠𝑘 on core 1, and terminates afterwards. Core 0 is associated with the red color. 𝑡𝑎𝑠𝑘 2 and 𝑡𝑎𝑠𝑘 3 run on core 1, which is associated with the blue color. The purpose is to check that tasks will run and terminate their execution on cores, whatever the interleaving. 𝑡𝑎𝑠𝑘 3 , which is an autostart task with a lower priority than 𝑡𝑎𝑠𝑘 2 , is assumed to be preempted by 𝑡𝑎𝑠𝑘 2 .

Formal analysis

We run a complete analysis of the system, the application, and the RTOS, using Roméo. We check that all the application's tasks complete their execution in a concurrent context. We verify that the places 𝑇 𝑒𝑟𝑚𝑖𝑛𝑎𝑡𝑒𝑇 𝑎𝑠𝑘 𝑖 [𝑡𝑎𝑠𝑘 𝑖 .𝑐𝑜𝑟𝑒_𝑖𝑑] are always marked by a token with the property:

𝐴𝐹 (𝑇 𝑒𝑟𝑚𝑖𝑛𝑎𝑡𝑒𝑇 𝑎𝑠𝑘 1 [0] > 0 𝑎𝑛𝑑 𝑇 𝑒𝑟𝑚𝑖𝑛𝑎𝑡𝑒𝑇 𝑎𝑠𝑘 2 [1] > 0 𝑎𝑛𝑑 𝑇 𝑒𝑟𝑚𝑖𝑛𝑎𝑡𝑒𝑇 𝑎𝑠𝑘 3 [1] > 0)
. Roméo model-checker replies that the property is not satisfied, and a counter-example execution trace is generated, proving that 𝑡𝑎𝑠𝑘 2 never ends its execution and the place 𝑇 𝑒𝑟𝑚𝑖𝑛𝑎𝑡𝑒𝑇 𝑎𝑠𝑘 2 [START_REF]Avionics Application Software Standard Interface, Part 1[END_REF] is never reached in a given case. The trace provided by the Roméo model-checker gives the following execution order:

1. StartOS: We start the operating system in the application mode. It first makes some initializations, activates the autostart tasks and alarms, performs scheduling, and executes the highest priority task. Thus, the autostart 𝑡𝑎𝑠𝑘 1 and 𝑡𝑎𝑠𝑘 3 are run in this startup phase; 2. ActivateTask: The service is called by 𝑡𝑎𝑠𝑘 1 running on core 0 in order to activate 𝑡𝑎𝑠𝑘 2 on core 1. The rescheduling for core 1 is performed on core 0, where the service call occurs. Core 0 sends an inter-core interrupt request to core 1 by setting the variable it_flag. 3. TerminateTask: The service is called by 𝑡𝑎𝑠𝑘 3 running on core 1. 𝑡𝑎𝑠𝑘 3 completes its execution on core 1 and the context switch is performed to the 𝑖𝑑𝑙𝑒 task;

4. Handler: Core 1 enters the kernel to execute the inter-core interrupt and perform the context switch (Figure 5.7). Since the need_switch flag of the tpl_kern structure is set to NO_NEED_SWITCH after the execution of the idle task on core 1, the context switch is not achieved. Thus, we return to the execution of the 𝑖𝑑𝑙𝑒 task;

5. TerminateTask: The service is called by 𝑡𝑎𝑠𝑘 1 running on core 0; 𝑡𝑎𝑠𝑘 1 ends its execution and the context switch is performed to the 𝑖𝑑𝑙𝑒 on this core.

The rescheduling performed by core 0 for core 1 in step 2, elects 𝑡𝑎𝑠𝑘 2 and extracts it from the ready_list. When the inter-core interrupt is executed, the context switch is performed to the task extracted from the ready_list if the need_switch flag is true. By calling the TerminateTask service in step 3 before executing the interruption, the first element of the ready_list is extracted, which is the 𝑖𝑑𝑙𝑒 task. Thus the problem occurs, and the context switch is made to 𝑖𝑑𝑙𝑒 task instead of 𝑡𝑎𝑠𝑘 2 . In other words, the activation of 𝑡𝑎𝑠𝑘 2 on core 1 is lost because the termination of task 𝑡𝑎𝑠𝑘 3 on core 1 elects task 𝑖𝑑𝑙𝑒 without checking that the already elected task (𝑡𝑎𝑠𝑘 2 ) has a higher priority. This scenario is obtained thanks to the model-checking. In the process, the other possible paths in this concurrent situation are also verified and the model-checker finds that the property hold for these other paths.

Correction of the error

The ready list is modified when the executing OS call service leads to a rescheduling.

To fix the problem of this case study, we have to test before the extraction of the task at the front of the ready list that it has a higher priority than the already elected one. If this elected task has a priority equal to or higher than the one of the first task in the ready list, then the rescheduling is correct, and the extraction is useless. This modification guarantees a context switch to either the already elected task or the newly elected task with the highest priority.

Computing time Table 6.3 shows the computing time and the amount of memory used in this analysis. The second column gives the data for the application model shown in Figure 6.9. The third column corresponds to an application running on three cores. It is obtained by duplicating 𝑡𝑎𝑠𝑘 3 and assigning it to the third core to evaluate the model-checking computation time when increasing state space. Table 6.4 represents the computing time after fixing the error in the model. The verification time is longer because all possible interleavings are considered.

Case study 2

Let us consider a modification of the application presented in figure 6.9 and obtained by replacing the call to the TerminateTask service with a call to the GetTaskID service in 𝑡𝑎𝑠𝑘 3 . GetTaskID writes in the TaskID variable the identifier of the task currently running. If no task is running, for example if GetTaskID was called from an ISR (Interrupt Service Routine), INVALID_TASK is returned. We want to verify if the Biglock is enough to protect the OS data structures access when we have concurrent calls to ActivateTask and GetTaskID services. Since GetTaskID is not a service that causes rescheduling, calling it should have no influence.

Formal analysis

In Trampoline, a system call handler performs the operating system service call as explained in 3.5.1. During this process, the need_switch and need_save fields of the tpl_kern data structure belonging to the core on which the service is performed are reset before calling the kernel function.

We conduct the same reachability verification with the Roméo model-checker leading to the detection of the following problem: When the GetTaskID service call is made in concurrence with the execution of the inter-core interrupt on core 1, the need_switch and need_save flags are reset by the system call handler. The information is therefore lost for the inter-core interrupt handler. The trace provided by the Roméo model-checker is as follows:

1. StartOS: We start the operating system in the application mode, and the autostart 𝑡𝑎𝑠𝑘 1 , 𝑡𝑎𝑠𝑘 3 and 𝑡𝑎𝑠𝑘 4 are run;

2. ActivateTask: The service is called by 𝑡𝑎𝑠𝑘 1 on core 0 to activate 𝑡𝑎𝑠𝑘 2 on core 1. Core 0 sends an inter-core interrupt request to core 1 after the rescheduling;

3. GetTaskID: The service is called by 𝑡𝑎𝑠𝑘 3 on core 1. The need_switch and need_save flags of the tpl_kern structure are reset (tpl_kern [START_REF]Avionics Application Software Standard Interface, Part 1[END_REF].need_switch=0);

4. Handler: The inter-core IT handler is called (Figure 5.7) to execute the inter-core interrupt on core 1 and effect the context switch. The context switch is not performed since the need_switch and need_save flags of the tpl_kern structure are reset after the execution of the GetTaskID on core 1. Thus, 𝑡𝑎𝑠𝑘 2 is never executed on core 1.

Correction of the error

The error found here holds for any application, independently of the number of tasks on two or more cores, as the system call handler always resets the kernel data structure before calling the corresponding kernel function, resulting in a loss of information.

The solution we adopted is to move, inside the sc_handler, the reset of the need_switch and need_save flag. Instead of resetting them before the kernel function is called, they are reset when they are taken into account to perform the context switch. In this way, services that do not cause a context switch leave need_switch and need_save unchanged, and the information is not lost to the inter-core interrupt. This change was modeled, and verification was performed by Roméo. It showed that the property is now satisfied. This way, the right value is preserved in the concurrent cases, and the problem is solved.

Computing time

The computation time and the amount of memory used in this analysis are given in Table 6.5. As in Case Study 1, the three-core system is obtained by duplicating Task 3 and assigning it to a 3rd core. After error correction, property checking requires exploring the entire state space, which involves more computing time, as shown in Table 6.6.

Scalability

The scalability of the approach is based on the number of cores, the number of tasks and their time interval, and the number of system calls that can be simultaneous. All these factors can increase the computation time during verification. Additional verifications with four cores, more than what is currently found in automotive embedded systems, each executing a task making concurrent system calls, run in 1124.8 seconds with 1141.3 MB of used memory and show that the approach scales to realistic automotive systems.

Conclusion

This chapter presented an approach that determines the compliance of the AUTOSAR multi-core real-time operating system (RTOS) from its formal model. The application models constructed represent the AUTOSAR multi-core test sequences developed by the Trampoline project. The Trampoline RTOS and the application models form a complete model that allows performing verification. For each test sequence, the conformity of the operating system is verified according to the AUTOSAR specifications. Each specification is formalized with an observer connected to the model that proves the satisfaction of its conditions. When its final state is reached, the specification they translate is well respected by the operating system during its execution. Reachability verification is thus performed through model-checking by exhaustively exploring the system's state space from its initial state. AUTOSAR test cases do not test the kernel in concurrency situations and are therefore unsuitable as a basis for verifying the correctness of the kernel's mutual exclusion and communication mechanisms. Consequently, we checked the rescheduling performed by the cores and the inter-core interrupt, considering case studies with simultaneous service calls on the cores. We found that the rescheduling and the context switching in concurrent situations are not functional. The model-checker provided counter-example traces. The problems have been reported to the developers, and solutions are proposed to fix them formally in the model. Verification showed the property satisfaction. A complete research door is opened to find implementation errors with several multi-core concurrent examples based on the verification approach.

Real-time schedulability analysis

The analysis of real-time systems seeks to ensure their temporal constraints. This means that the tasks that compose the system must respect the temporal deadlines according to the criticality, classified into different categories (hard real-time systems, soft realtime systems, firm real-time systems). These tasks can interact and share one or more resources. They can be:

• Periodic and be activated regularly with a fixed period;

• Sporadic and be started irregularly with a minimum duration between two task's instance (job) activations;

• Aperiodic and be activated irregularly.

Liu and Layland present the first model of periodic tasks [START_REF] Liu | Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment[END_REF] and describe a task using the parameters (𝐶, 𝑇) shown in Figure 7.1, page 118. 𝐴 is the activation date of the task's job. 𝐶 corresponds to the 𝑊𝐶𝐸𝑇, which is the worst-case execution time. It is the duration considered the most in real-time scheduling analyses; in this study, we also consider the Best Case Execution Time (𝐵𝐶𝐸𝑇) and the dependencies between tasks in a multi-core context. 𝑇 represents its arrival period, and its deadline 𝐷 can be implicit (𝐷 = 𝑇). Thus, a periodic task executes for 𝐶 time units every 𝑇 time units without missing the deadline 𝐷. The response time is defined as the duration between the arrival time of the task's job and its completion.

In multi-processor real-time system scheduling, tasks are scheduled on each processor with a scheduling policy that defines the rules that choose the order and tasks to be executed. These scheduling decisions can be made online or offline, i.e., during or before execution. Since the founding work of Liu and Layland in 1973 [START_REF] Liu | Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment[END_REF], various multi-processor (multi-core) scheduling policies have been proposed in three principal categories [START_REF] Chéramy | Algorithmes pour l'ordonnancement temps réel multiprocesseur[END_REF]: partitioned, global, and hybrid. Scheduling multi-core systems is a two-dimensional problem, with a temporal organization on each core and a spatial one that ensures the job is executed on which core. Partitioned scheduling consists in treating each of the two dimensions separately. Thus the tasks assigned to a core are scheduled with a mono-core scheduling policy and are not allowed to migrate to a different core. Global scheduling treats both the temporal and spatial dimensions together. It then applies single scheduling for the whole multi-core system. Finally, hybrid scheduling combines partitioned and global scheduling and allows better control of tasks' migration.

Several research works have well-studied scheduling analyses in mono-core systems [START_REF] Atlas | Statistical rate monotonic scheduling[END_REF][START_REF] Palencia | Schedulability analysis for tasks with static and dynamic offsets[END_REF][START_REF] Marti | On real-time control tasks schedulability in[END_REF], and many studies illustrate the lack of guarantees for their analytical results by finding flaws [100-102]. In the multi-core systems, the existing methods for the schedulability analysis are studied in different research works [103-105]. As multi-core systems are more complicated, the schedulability analysis is affected by significant complexity and pessimism, especially for global multi-core fixed priority analysis [106,107]. This motivates the use of formal methods to provide confidence in these scheduling analyses.

Most real-time operating systems in the multi-core case are based on partitioned schedulers with fixed priorities, even though several scheduling policies exist in theory. Indeed, scheduling policies are based on simplified assumptions and are sometimes described abstractly. However, the real multi-core context considers several aspects, such as parallelism, interrupt management, and possible interleaving due to concurrency.

It would be interesting to study and verify other scheduling policies considering the RTOS. Model-checking is well adapted for verifying a scheduler within the RTOS that needs to consider all these aspects to check its policy or eventually implement it. However, model-checking using the HCTPN formalism with stopwatches is limited to partitioned scheduling where the temporal and spatial organization is separated. Indeed, if a task is preempted, the time associated with its stopwatch is frozen. Modeling the migration of this task to another core would lead to the color change and the stopwatch's reset, which explains the limitation of global and hybrid preemptive scheduling. We only consider in this work the preemptive partitioned scheduling.

Formal verification of schedulability analysis

Formal verification with models for schedulability analysis of real-time systems has been studied for several years, as presented in Section 2.3.4. This section presents our method for verifying quantitative temporal properties for real-time applications with preemptive scheduling based on the complete RTOS model built with HCTPN(Chapter 5). The defined scheduling policy of the AUTOSAR multi-core RTOS is based on a partitioned scheduling policy with fixed priorities. Each task is statically assigned to a core, can be preempted, and resumed at the same point later.

In our work, we propose a verification chain that includes the steps presented in Figure 6.1, page 96. The requirement expression can be simple through an observer modeled by an additional HCTPN associated in a non-intrusive way with the original model without altering its behavior. The satisfaction of the requirement is thus verified by a reachability property of a particular state. We illustrate the observer model associated with each task to check its respect or missing deadline. This process will be detailed in the following for the schedulability analysis.

Schedulability observer

A classical method for schedulability analysis is to rely on the use of observers [108], allowing to reduce the verification problem to a simpler model-checking problem such as a simple reachability property. It is then necessary that every trace that contradicts the schedulability property can be detected by the observer but also that the observer is innocuous, meaning that it cannot interfere with the system under observation.

To analyze the schedulability of tasks, we use the classical observer represented in yellow in Figure 7.2, page 121 linked to each task model. The delay 𝐷 𝑖 represents the deadline of the task. The firing of transition 𝑜𝑘 𝑖 means that the task terminates before its deadline. The firing of transition 𝑑𝑒𝑎𝑑𝑙𝑖𝑛𝑒 𝑖 means 𝑡𝑎𝑠𝑘 𝑖 does not respect its deadline. Hence the task meets its deadline iff for all state of the state space, there is no token in place 𝑂𝑏𝑠 𝑖 . The place 𝑂𝑏𝑠 𝑖 is emptied by transition 𝑒𝑚 𝑝𝑡𝑦 𝑖 to avoid the accumulation of tokens that leads to an unbounded system. The schedulability property is then written for this observer by the CTL logic formula 𝐴𝐺 (𝑂𝑏𝑠 𝑖 < 1); if it is not satisfied, a counter-example execution trace is generated.

Application of the scheduling analysis approach

To illustrate the approach presented above, let us consider the system of Figure 7.3, page 123, with the characteristics of Table 7.1, page 122. The example contains three task models considering time intervals of runnable between [𝐵𝐶𝐸𝑇, 𝑊𝐶𝐸𝑇]. 𝑡𝑎𝑠𝑘 1 is executed between 8 and 11-time units, activates 𝑡𝑎𝑠𝑘 2 then runs for 2 time units before terminating. We consider the following priority relationship: 𝑡𝑎𝑠𝑘 2 has the highest priority, followed by 𝑡𝑎𝑠𝑘 1 and finally 𝑡𝑎𝑠𝑘 3 . At start 𝑡𝑎𝑠𝑘 1 and 𝑡𝑎𝑠𝑘 3 are automatically activated and run on core 0 and core 1 respectively. Core 0 is associated with the red color. 𝑡𝑎𝑠𝑘 2 is activated by 𝑡𝑎𝑠𝑘 1 and runs on core 1, which is associated with the blue color. Priorities and assignment of cores are done statically. Considering the execution time of the first part of 𝑡𝑎𝑠𝑘 1 is its WCET (i.e. 𝑊𝐶𝐸𝑇 11 = 11), we got the chronogram presented in Figure 7.4, page 124. In this case, the tasks meet their deadlines, and 𝑡𝑎𝑠𝑘 2 starts its execution, whereas the first job of 𝑡𝑎𝑠𝑘 3 is terminated on core 1. But we now ask for the whole execution time interval of 𝑡𝑎𝑠𝑘 1 . Therefore, we apply our verification approach to check the schedulability of the application over the whole time interval [START_REF] Béchennec | Trampoline an open source implementation of the OSEK/VDX RTOS specification in Emerging Technologies and Factory Automation[END_REF][START_REF] Roux | Roméo: formal verification and synthesis for timed systems[END_REF]. We run a full analysis of the application with the RTOS, performed in the first time using no parameters to verify schedulability and in the second time with parameter synthesis to find the execution time interval of 𝑡𝑎𝑠𝑘 1 . Verification approach with observers Based on the application modeling approach presented in Figure 5.4, page 90, we construct the task models of Figure 7.3, page 123 with the timing values of Table 7.1, page 122. We add one observer per task, as shown in Figure 7.2, page 121. The schedulability analysis is conducted on the whole system containing the application and RTOS models with Roméo. We check that the place 𝑂𝑏𝑠 𝑖 are never marked by a token with the property: 𝐴𝐺 (𝑂𝑏𝑠 1 < 1 𝑎𝑛𝑑 𝑂𝑏𝑠 2 < 1 𝑎𝑛𝑑 𝑂𝑏𝑠 3 < 1). A counter-example execution trace is generated, proving this property is not satisfied, and 𝑡𝑎𝑠𝑘 3 may miss its deadline. Indeed, if the execution time of 𝑡𝑎𝑠𝑘 1 is its BCET (i.e. 𝐵𝐶𝐸𝑇 11 = 8), 𝑡𝑎𝑠𝑘 3 , running on core 1 does not have the time to finish before its deadline as shown in Figure 7.5, page 124. The task 𝑡𝑎𝑠𝑘 1 activates 𝑡𝑎𝑠𝑘 2 at time 8, since 𝑡𝑎𝑠𝑘 2 has a higher priority, 𝑡𝑎𝑠𝑘 3 running on the same core as 𝑡𝑎𝑠𝑘 2 is preempted. Then 𝑡𝑎𝑠𝑘 2 terminates its execution at time 16, the deadline of 𝑡𝑎𝑠𝑘 3 . The tasks set is, therefore, not schedulable under the partitioned fixed priority scheduling policy and the worst temporal behavior of the system happens with the BCET of 𝑡𝑎𝑠𝑘 1 .

Task parameters synthesis

To synthesize the 𝑡𝑎𝑠𝑘 1 execution time interval that allows the tasks system to meet their deadlines and then to be schedulable, we set the first execution part (𝑅𝑢𝑛 11 ) in the parametric interval [𝑎,𝑏], and we bound 𝑏 by 11. Checking the property 𝐴𝐺 (𝑂𝑏𝑠 1 < 1 𝑎𝑛𝑑 𝑂𝑏𝑠 2 < 1 𝑎𝑛𝑑 𝑂𝑏𝑠 3 < 1) leads the parameter synthesis.

Ad-hoc scheduling system

The scheduler within Trampoline is kernel-based, which means there is no separation between the kernel and scheduler codes. Therefore, modifying its implementation requires expertise to identify the parts of the kernel that need to be replaced. Our main idea of this work is to show the possibility of efficiently verifying new scheduling policies within the multi-core RTOS, considering parallelism, concurrency, and preemption in compact time. To study the feasibility of this schedulability verification, we define an ad-hoc scheduler and modify the fixed priority partitioned scheduling of the Trampoline RTOS model. In principle, the scheduler should be called when an event occurs and requires rescheduling, for example, a task that activates another or terminates, as shown in Figure 3.12, page 54. This allowed us to determine the scheduler parts to change and perform a schedulability check on the system, considering the stopwatches. This section presents the specifications of the chosen ad-hoc scheduler, its implementation in the model, and the conducted verification using parameters synthesis.

Ad-hoc scheduler specifications

The scheduling policy consists of a four-tasks application: 𝑡𝑎𝑠𝑘 1 , 𝑡𝑎𝑠𝑘 2 , 𝑡𝑎𝑠𝑘 3 , and 𝑡𝑎𝑠𝑘 4 , statically assigned to two cores, as shown below:

tion is modeled based on the task model shown in Figure 7.2, page 121, linked with the observer.

tpl_start We extend the model of this function with the modification of tasks' dynamic priorities of core 1 according to the task currently elected on core 0. This means that after electing a task on core 0 and copying its information into the elected attributes of the 𝑡 𝑝𝑙_𝑘𝑒𝑟𝑛 structure, we rely on the identifier of this new elected task to compute the new dynamic priorities of 𝑡𝑎𝑠𝑘 2 and 𝑡𝑎𝑠𝑘 3 assigned to core 1. The dynamic priority concatenates the base priority and the activation order number as explained in the scheduling paragraph 3.5.2, page 51. The 𝑟𝑒𝑎𝑑𝑦_𝑙𝑖𝑠𝑡 of core 1 is then updated with the new priorities, and the 𝑛𝑒𝑒𝑑_𝑠𝑐ℎ𝑒𝑑𝑢𝑙𝑒 flag is set to 1.

tpl_schedule_from_running This function invokes the scheduler only on one core.

Since the scheduling decision on core 1 depends on the task running on core 0, we need to call the 𝑡 𝑝𝑙_𝑠𝑐ℎ𝑒𝑑𝑢𝑙𝑒_ 𝑓 𝑟𝑜𝑚_𝑟𝑢𝑛𝑛𝑖𝑛𝑔 function for core 1. We replace it with the 𝑡 𝑝𝑙_𝑚𝑢𝑙𝑡𝑖_𝑠𝑐ℎ𝑒𝑑𝑢𝑙𝑒 function, which loops its call over the cores. 𝑡 𝑝𝑙_𝑚𝑢𝑙𝑡𝑖_𝑠𝑐ℎ𝑒𝑑𝑢𝑙𝑒 performs several rescheduling when many tasks may be activated on multiple cores, indicated by the 𝑛𝑒𝑒𝑑_𝑠𝑐ℎ𝑒𝑑𝑢𝑙𝑒 flag of the core. Therefore, the rescheduling of core 1 from core 0 can be done, and if needed, core 0 sends an inter-core interrupt request to core 1 to trigger the context switch and execute the task.

tpl_terminate_task_service In the case of task termination on core 0, the rescheduling of core 1 from core 0 must be added explicitly by modifying the function 𝑡 𝑝𝑙_𝑡𝑒𝑟𝑚𝑖𝑛𝑎𝑡𝑒_𝑡𝑎𝑠𝑘_𝑠𝑒𝑟𝑣𝑖𝑐𝑒. For that, 𝑡 𝑝𝑙_𝑠𝑐ℎ𝑒𝑑𝑢𝑙𝑒_ 𝑓 𝑟𝑜𝑚_𝑟𝑢𝑛𝑛𝑖𝑛𝑔 is called by core 0 to perform rescheduling for core 1, followed by a context switch to send the inter-core interrupt to core 1 and execute the elected task.

Task parameters synthesis

Let us consider this ad-hoc scheduling system with the characteristics of Table 7.3, page 128. The goal now is to synthesize the tasks execution time interval such that the tasks meet their deadlines. We replace the interval bound [𝐵𝐶𝐸𝑇, 𝑊𝐶𝐸𝑇] of the model 𝑡𝑎𝑠𝑘 3 , respectively 𝑡𝑎𝑠𝑘 4 , by the parametric interval [3,𝑏], respectively [𝑎,𝑎] (Table 7.3, page 128). We bound the parameters 𝑎 and 𝑏 in the interval [START_REF] Autosar Gbr | Specification of operating system[END_REF][START_REF]OSEK/VDX OS Test Plan Version 2[END_REF]. We use the non- To test these results, we use the simulator of Roméo tool that allows to run timed traces (i.e. chronograms). The first result is verified with the chronogram of Figure 7.7, page 129, with the execution time of the 𝑡𝑎𝑠𝑘 3 and 𝑡𝑎𝑠𝑘 4 in the interval [3, 3] (i.e. 𝐵𝐶𝐸𝑇 3 = 3). In this case, 𝑡𝑎𝑠𝑘 2 terminates its execution, whereas the first job of 𝑡𝑎𝑠𝑘 3 is terminated.

Assuming that 𝑎 and 𝑏 are bounded in the parameter constraints in the interval [START_REF] Autosar Gbr | Specification of operating system[END_REF][START_REF]OSEK/VDX OS Test Plan Version 2[END_REF].

The second result provides a relationship between 𝑎 and 𝑏 in this interval such that 𝑎 > 𝑏 -1.This property is satisfied with 𝑎 = 𝑏 = 5.5. We thus set the intervals of 𝑡𝑎𝑠𝑘 3 and 𝑡𝑎𝑠𝑘 4 models in [5.5, 5.5]; the extracted timed trace is presented in the Figure 7.8, page 129. The tasks set is, therefore, schedulable.

Response time analysis

The response time analysis allows calculating the response time, which represents the duration between the arrival time of the task's instance (job) and its completion. This analysis is performed using parameters in the same task-related observer, taking into account the dependency between the tasks. To automatically compute the response time of a 𝑡𝑎𝑠𝑘 𝑖 , we just replace 𝐷 𝑖 with a parameter 𝑑 𝑖 in its observer. Then the verification of the property 𝐴𝐺 (𝑂𝑏𝑠 𝑖 < 1) will synthesize all the values of 𝑑 𝑖 such that the task terminates before 𝑎 time units i.e. the time between the job activation and the end of its execution. The smaller value of 𝑑 𝑖 is the response time of 𝑡𝑎𝑠𝑘 𝑖 .

Based on the same system characteristics of Table 7.3, page 128, we instantiate the task execution time with time intervals, and replace 𝐷 𝑖 with a parameter 𝑑 𝑖 in the task observers. Roméo synthesizes the values of the parameter 𝑑 𝑖 and analyzes the response time of 𝑡𝑎𝑠𝑘 𝑖 . Table 7.4, page 130, provides the results obtained by Roméo modelchecker with time computing and memory use. We instantiate the 𝐷 𝑖 with their values (see the deadline values in Table 7.3, page 128) in the observers, and we verify the property ( 𝐴𝐺𝑂𝑏𝑠 𝑖 < 1). Roméo replies that the property is not satisfied and automatically generates a timed trace as a counter-example represented by the chronogram in Figure 7.9, page 131. In this case, 𝑅 3 > 𝐷 3 , and 𝑡𝑎𝑠𝑘 3 is preempted twice by 𝑡𝑎𝑠𝑘 2 . The 𝑡𝑎𝑠𝑘 3 misses its deadline when its execution time is the WCET (i.e. 𝑊𝐶𝐸𝑇 3 = 6).

Conclusion

This chapter presented a method for efficiently analyzing real-time applications running on an RTOS with preemptive scheduling using the Roméo tool. Thanks to the capabilities of stopwatches, the application models include the possibility to block the runnable's elapsed time and to model the preemption. The complete model linked to observers is used to check the schedulability of an application. The parameterized version calculates the execution times required to guarantee schedulability or response times.

We have also presented the possibility of changing the scheduling policy and efficiently verifying the temporal properties of dependent and preemptive tasks. We detailed the modifications required to support an ad-hoc scheduler and its verification with the same approach.

CONCLUSION AND PERSPECTIVES

Conclusion

Multi-core real-time embedded systems must respect several constraints, and their verification must consider real-time and concurrency aspects to guarantee an error-free system. Testing and simulation are methods to identify errors in software programs. However, they are not exhaustive and do not guarantee the elimination of all errors. Formal verification is a solution that uses a set of mathematical techniques to verify the correctness of the system behavior. To apply this method to multi-core Real-Time Operating Systems (RTOS), we focused on the model-checking approach, an automatic process that exhaustively checks if the model respects specific properties. Two questions are asked: The first one is how to ensure that the behavior of the multi-core RTOS conforms to its standard and requirements, taking into account concurrency and parallelism aspects. The second one concerns verifying the scheduling of a real-time application running on the RTOS, considering the preemptive aspect.

The thesis work proposed in this manuscript tries to answer these questions. First, we have defined the model of High-level Colored Time Petri nets (HCTPN) in which we can use temporal parameters on the transitions and consider parallelism and concurrency of cores. This formalism was used for modeling the multi-core RTOS, and the colors specify the hardware where the software is executed. Preemption is supported through stopwatches associated with timed transitions that can be activated by more than one color, thus allowing true concurrency modeling. Then, we proposed a formal verification approach where the RTOS model and the application are built with HCTPN based on a number of translation rules. The model-checking of the HCTPN formalism is implemented in the Roméo tool where we performed this approach. From the elaborated model, the verification of the properties has been performed using external observers modeled by an additional HCTPN associated in a non-intrusive way to the model without altering its behavior. This approach has been applied to the Trampoline operating system, a multi-core RTOS compliant with OSEK/VDX and AUTOSAR standards used in automotive embedded systems. It allowed us to verify with the model-checking of the extended formalism in Roméo:

• The multi-core RTOS conformity to the AUTOSAR standard;

• The inter-core synchronization mechanism involved in concurrent OS service execution;

• The schedulability of real-time applications with dependent preemptive tasks.

These obtained results showed the feasibility of our approach and the power of RTOS verification. It allowed the automatic identification of two possible OS errors in concurrent execution, considering simultaneous service calls on the cores. These errors illustrated that the rescheduling and the context switching in concurrent situations are not functional. Thus, the data protection is insufficient, and the synchronization of the cores is defective. The parametric analysis of the HCTPNs has also shown its effectiveness in synthesizing the parameter values that satisfy the property. It allowed calculating the necessary execution times to guarantee the scheduling or the response times. However, some points remain to be discussed:

• The modeling work requires expertise and remains a heavy task that takes considerable time and effort;

• The combinatorial explosion problem can limit the verification of complex examples.

It, therefore, leads to perspectives on future works that we explore in what follows.

Perspectives

After the proposed multi-core RTOS verification approach with extended time Petri nets, one perspective of this work is to model the multi-core version that allows executing the kernel code on different cores in parallel and handling interrupts simultaneously. The current approach considers a global lock that prevents this parallel execution. Thanks to the formalism of HCTPN implemented in Roméo, modeling can be done using colors. The kernel can be executed simultaneously by the different cores, such as one color corresponding to one core. However, the combinatorial explosion problem must be examined as adding parallelism at the kernel level will considerably increase the number of system states. One solution to this problem could be the abstraction of the OS model with a new model that preserves the behavior as much as possible and merges its states to reduce their number. This model abstraction must satisfy the same properties of the initial model we want to conserve. Thus, additional verification can be performed using a proof assistant, for example, and the approach would combine the two formal verification methods.

A second perspective is to implement a Domain Specific Language (DSL) to facilitate the modeling of the operating system and the construction of the model for several levels of abstraction. The DSL will automatically build a model of the operating system in HCTPN from its source code based on the rules proposed in Section 5.2, page 79.

We can also apply these rules in reverse to generate a verified OS code by applying a reachability analysis on the model. The models built in Roméo are represented in XML files; therefore, an XML parser and a code translator are needed to elaborate the DSL. Finally, a third perspective would be verifying several scheduling policies based on the RTOS model. A first approach would be to separate the scheduler code from the kernel by adding an intermediate model. Thus, instead of having the scheduler code distributed in the kernel, the scheduler model will be isolated while communicating with the system components. That will facilitate the modification of the scheduling policies for their verification, minimizing the changes within the kernel. The implementation of the DSL can also cover this perspective and describe the scheduler's implementation following a high-level-based approach. The DSL will allow the description of its behavior and the specification of the scheduler objects and parameters. Thus the language can generate its code to be integrated within the OS. Abstract: Formal verification is a solution to increase the system's implementation reliability. In our thesis work, we are interested in using these methods to verify multi-core RTOS. We propose a model-checking approach using time Petri nets extended with colored transitions and high-level features. We use this formalism to model the Trampoline multi-core OS, compliant with the OSEK/VDX and AUTOSAR standards. We first define this formalism and show its suitability for modeling real-time concurrent systems. We then use this formalism to model the Trampoline multi-core RTOS and verify by model-checking its conformity with the AUTOSAR standard.

From this model, we can verify properties of both the OS and the application, such as the schedulability of a real-time system and the synchronization mechanisms: concurrent access to the data structures of the OS, multicore scheduling, and inter-core interrupt handling. As an illustration, this method allowed the automatic identification of two possible errors of the Trampoline OS in concurrent execution, showing insufficient data protection and faulty synchronization.

Figure 1 . 1 :

 11 Figure 1.1: Real-Time System (RTS)

Figure 1 . 2 :

 12 Figure 1.2: Formal verification approach

Figure 2 . 1 :

 21 Figure 2.1: Model-checking approach.

Figure 3 . 1 :

 31 Figure 3.1: The three modules of the OSEK/VDX standard.

Figure 3 . 4 :

 34 Figure 3.4: Tasks priority.

Figure 3 . 5 :

 35 Figure 3.5: AUTOSAR architecture.

Figure 3 . 6 :

 36 Figure 3.6: Trampoline application configuration.

Figure 3 . 7 :

 37 Figure 3.7: Mono-core Trampoline architecture.

Figure 3 . 10 :

 310 Figure 3.10: Multi-core Trampoline architecture.

Figure 3 . 11 :

 311 Figure 3.11: The activation of a task 𝜏 2 on core 1 by a task 𝜏 0 running on core 0.

Figure 3 . 12 :

 312 Figure3.12: The activation of a task 𝜏 2 on core 1 by a task 𝜏 0 running on core 0 in parallel with the termination of the task 𝜏 1 on core 1.

  (𝑚, 𝑡) = ∅ and 𝑔𝑢𝑎𝑟𝑑 (𝑚, 𝑡, 𝑥, •) = 𝑡𝑟𝑢𝑒 or ∃𝑐 𝑎 ∈ colorSet any (𝑚, 𝑡) ≠ ∅ and 𝑔𝑢𝑎𝑟𝑑 (𝑚, 𝑡, 𝑥, 𝑐 𝑎 ) = 𝑡𝑟𝑢𝑒 . We illustrate the enabling condition with two examples with two colors 𝐶 = {𝑏𝑙𝑢𝑒, 𝑟𝑒𝑑} For the HCTPN given in Figure 4.1.a, the transition 𝑇 1 ∈ 𝑇 𝑎𝑛𝑦 .

.4. 3 . 1 . 2 . 2

 3122 Figure 4.1: Enabling transition

.

  Figure 4.1.a, the firing of 𝑇 1 ∈ 𝑇 𝑎𝑛𝑦 from 𝑚 0 leads to the marking 𝑚 1 = It is noted 𝑚 0 (𝑇 1 ,•) ----→ 𝑚 1 . Let us now consider the HCTPN of Figure 4.1.b, the firing of 𝑇 1 ∈ 𝑇 𝑎𝑛𝑦 is possible only for 𝑎𝑛𝑦 = 𝑟𝑒𝑑 and leads to the marking 𝑚 2 =

Figure 4 . 2 :

 42 Figure 4.2: High-level manipulation of variables.

For

  any 𝑡 ∈ 𝑇 𝑎𝑛𝑦 , 𝑣(𝑡, 𝑐) is the valuation of the clock associated with 𝑡 and the color 𝑐 ∈ 𝐶. i.e., it is the time elapsed since the transition 𝑡 has been newly enabled by 𝑚 with 𝑐 ∈ colorSet any (𝑚, 𝑡). For other transitions 𝑡 ∈ 𝑇 𝑎𝑛𝑦 , 𝑣(𝑡, •) is the valuation of the clock associated with 𝑡. 0 is the initial valuation with ∀𝑡 ∈ 𝑇, ∀𝑐 ∈ 𝐶 ∪ {•}, 0(𝑡, 𝑐) = 0. As an example, if we keep only the useful clocks, the initial valuation of the HCTPN of Figure 4.1, is 𝑣 0 = state of the net N is a tuple ((𝑚, 𝑥), 𝑣) in N 𝑃×𝐶 ×X 𝑋 ×R ≥0 𝑇×𝐶 , where: 𝑚 is a marking, 𝑥 is a variable valuation and 𝑣 is a valuation of the clocks.

Example 1 𝑇 1 .•

 11 in purple.4.3.1.5 Examples of HCTPNWe give three examples. The first two examples illustrate the high-level functionalities, and the third illustrates the notion of color and multi-enableness. Let's go back to the HCTPN given in Figure4.2, page 63.The initial marking 𝑚 0 = The valuations of the clocks are given by the matrix such that the initial valuation is 𝑣 0 =

Figure 4

 4 Figure 4.4: HCTPN model illustrating colored multi-enableness

  1 and 𝐶 2 whose values are given by a function called isRunning shown in Figure 4.5.

  Figure 4.5: HCTPN model with stopwatches of two-task scheduling.

Figure 4 . 6 :

 46 Figure 4.6: The GetSpinLock and RelSpinLock function models

Listing 4. 2 :

 2 Figure 4.7: The tasks models

2 .

 2 GetAlarmBase calls the kernel function tpl_get_alarm_base_service model 1 , represented in details in 5.3.2 (Figure 5.8).

Figure 5 . 2 :

 52 Figure 5.2: GetAlarmBase service model.

Figure 5 . 3 :

 53 Figure 5.3: Example of the ActivateTask service modeling.

  𝑎𝑛𝑦].running. activate_count > 0 [0, 0] tpl_kern[$𝑎𝑛𝑦].running.state = READY_AND_NEW !(tpl_kern[$𝑎𝑛𝑦].running.activate_count > 0) [0, 0] tpl_kern[$𝑎𝑛𝑦].running.state = SUSPENDED tpl_kern[$𝑎𝑛𝑦].running_id < EXTENDED_TASK_COUNT [0, 0] tpl_task_events_table[tpl_kern[$𝑎𝑛𝑦].running_id].evt_set =0 tpl_task_events_table[tpl_kern[$𝑎𝑛𝑦].running_id].evt_wait=0 !(tpl_kern[$𝑎𝑛𝑦].running_id < EXTENDED_TASK_COUNT) [0, 0]

Figure 5 . 4 :

 54 Figure 5.4: The kernel function tpl_terminate.

Figure 5 . 5 :

 55 Figure 5.5: tpl_put_new_proc model.

Figure 5 . 9 :

 59 Figure 5.9: Trampoline application configuration with the added GTL module.

Figure 5 . 10 :

 510 Figure 5.10: GTL module and the C-like output file.

Figure 5 . 11 :

 511 Figure 5.11: Application task model.

Figure 6 . 1 :

 61 Figure 6.1: Verification approach.

Figure 6 . 2 :

 62 Figure 6.2: mc_alarm_s1 test sequence. • represents the success of the system service call and × the canceling of the alarm.

Figure 6 . 9 :

 69 Figure 6.9: Three-tasks application model.

Figure 5 .

 5 7 represents the interrupt handler model. The core 1 blocks on an active wait for the release of the local and global lock;

Figure 7 . 1 :

 71 Figure 7.1: Task model.

Figure 7 . 3 :

 73 Figure 7.3: Three-tasks application model considering time intervals and observers.

Figure 7 . 6 :

 76 Figure 7.6: Model part to modify for the ad-hoc scheduler implementation. The symbol -> indicates a function call.

Titre:

  Modélisation et vérification formelles d'un RTOS multicoeur conforme à AUTOSAR Mot clés : Vérification formelle, Model-checking, Réseaux de Petri colorés de haut niveau, Systèmes d'exploitation temps réel, Exécution multi-coeurs, Vérification d'OS AUTOSAR. Résumé : La vérification formelle est une solution pour augmenter la fiabilité de l'implémentation du système. Dans notre travail de thèse, nous nous intéressons à l'utilisation de ces méthodes pour la vérification des systèmes d'exploitation multi-coeurs temps réel. Nous proposons une approche de model-checking utilisant les réseaux de Petri temporels, étendus avec des transitions colorées et des fonctionnalités de haut niveau. Nous utilisons ce formalisme pour modéliser le système d'exploitation multi-coeur Trampoline, conforme aux standards OSEK/VDX et AUTOSAR. Nous définissons dans un premier temps ce formalisme et montrons son adéquation avec la modélisation de systèmes concurrents temps reel. Nous utilisons en-suite ce formalisme pour modéliser le système d'exploitation multi-coeur Trampoline et vérifions par model-checking sa conformité avec le standard AUTOSAR. À partir de ce modèle, nous pouvons vérifier des propriétés aussi bien sur l'OS que sur l'application telles que l'ordonnançabilité d'un système tempsréel ainsi que les mécanismes de synchronisation : accès concurrents aux structures de données du système d'exploitation, ordonnancement multi-coeur et traitement des interruptions inter-coeur. À titre d'illustration, cette méthode a permis l'identification automatique de deux erreurs possibles de l'OS Trampoline dans l'exécution concurrente, montrant une protection insuffisante des données et une synchronisation défectueuse. Title: AUTOSAR compliant multi-core RTOS formal modeling and verification Keywords: Formal verification, Model-checking, High-level Colored Time Petri Nets, Real-Time Operating Systems (RTOS), Multi-core execution, AUTOSAR OS verification.

  Trampoline is a Real-Time Operating System (RTOS) developed by the STR (Real Time Systems) group of the LS2N laboratory in Nantes, France. This operating system is OSEK/VDX 2.2.3 and AUTOSAR 4.0 compliant[START_REF] Béchennec | Trampoline an open source implementation of the OSEK/VDX RTOS specification in Emerging Technologies and Factory Automation[END_REF]. Trampoline is mostly written in C

	Application Layer
	Runtime Environment (RTE)
	Basic Software Layer
	ECU Abstraction Layer
	Service Layer	Complex Drivers
	Microcontroller Abstraction
	Layer
	Microcontroller

  𝑇 𝑎𝑛𝑦 , and ∃𝑐 𝑎 ∈ 𝐶 such that ∀𝑝 ∈ 𝑃, 𝑚( 𝑝) [𝑐 𝑎 ] ≥ pre( 𝑝, 𝑡) [𝑎𝑛𝑦] and ∀𝑐 ∈ 𝐶 \ {𝑐 𝑎 }, 𝑚( 𝑝) [𝑐] ≥ pre( 𝑝, 𝑡) [𝑐]. The corresponding set of color 𝑐 𝑎 is noted colorSet any (𝑚, 𝑡) ⊆ 𝐶 Finally, a transition 𝑡 ∈ 𝑇 is said to be enabled by a given marking 𝑚 ∈ N 𝑃×𝐶 and a valuation 𝑥 ∈ X 𝑋 if en(𝑚, 𝑡) = 𝑡𝑟𝑢𝑒 and either colorSet any

and ∀𝑝 ∈ 𝑃 and ∀𝑐 ∈ 𝐶, 𝑚( 𝑝) [𝑐] ≥ pre( 𝑝, 𝑡) [𝑐]. We denote en(𝑚, 𝑡) ∈ {𝑡𝑟𝑢𝑒, 𝑓 𝑎𝑙𝑠𝑒}, the true value of this condition. • if 𝑡 ∈

  1] == 1)). Here P 12[0]

	T 1	GetSpinLock	RelSpinLock
	[1, 1]
	isLocked(gate)	T 2	T 8
		[1, 1]	[1, 1]
		! isLocked(gate)	unlock(gate);
	P 2	P 7
		T 3	T 3
		[1, 1]	[1, 1]
	T 4	lock($any, gate)	endOfRSL[$any] = 1;
	[1, 1]	P 3
	isLockedBy($any, gate) == 0	T 5
		[1, 1]
		isLockedBy($any, gate) == 1
		endOfGSL[$any] = 1;

  .9. The second part is a set of Petri subnets, one per task or ISR of the application. The

	Templates		OS infrastructure
	(.goilTemplate)		(.c/ .asm)
	XML application		Kernel sources
	description		(.c/.h)
	OIL application description	GOIL Compiler	Static data structures (c/.h)	C compiler
				+ linker
	Application
	sources (.c / .h)	Roméo	C-like	Executable
		Template Module	Roméo file	code
		(.goilTemplate)	(.c)	(binary)

Table 6 .

 6 1: Computing time and memory used for verification -mc_alarm_s1.

		( 𝑝) → (𝑞)
		Memory used (MB) Computing time (s)
	SWS_Os_00632	662.0	12.4
	SWS_Os_00633	647.7	12.1
	SWS_Os_00636	666.5	12.1
	SWS_Os_00637	663.7	12.0
	SWS_Os_00638	656.0	12.1
	SWS_Os_00639	662.5	12.1
	SWS_Os_00640	672.7	12.1

Table 6 .

 6 2: Computing time and memory used for verification -mc_spinlock_s1.

		( 𝑝) → (𝑞)
	Observer	Memory used (MB) Computing time (s)
	SWS_Os_00649	108.2	2.7
	SWS_Os_00650	107.7	2.7
	SWS_Os_00651	111.6	2.8
	SWS_Os_00652	121.7	2.7
	SWS_Os_00653	120.9	2.7
	SWS_Os_00654	130.2	2.8
	SWS_Os_00655	114.4	2.7
	SWS_Os_00656	113.5	2.7
	SWS_Os_00657	126.6	2.7
	SWS_Os_00658	108.5	2.7
	SWS_Os_00659	121.6	2.7
	SWS_Os_00661	109.7	2.7

Table 6 .

 6 3: Computing time and amount of memory used. 𝐴𝐹 (𝑇 𝑒𝑟𝑚𝑖𝑛𝑎𝑡𝑒𝑇 𝑎𝑠𝑘 𝑖 [𝑡𝑎𝑠𝑘 𝑖 .𝑐𝑜𝑟𝑒_𝑖𝑑] > 0)

	Number of cores	2	3
	Model-checker result	false	false
	Memory used	96.0MB	174.9MB
	Computing time	7.1s	10.7s

Table 6 .

 6 4: Computing time and memory used after correction.

		𝐴𝐹 (𝑇 𝑒𝑟𝑚𝑖𝑛𝑎𝑡𝑒𝑇 𝑎𝑠𝑘 𝑖 [𝑡𝑎𝑠𝑘 𝑖 .𝑐𝑜𝑟𝑒_𝑖𝑑] > 0)
	Number of cores	2	3
	Model-checker result	true	true
	Memory used	117.6MB	127.8MB
	Computing time	51.1s	2629.2s

Table 6 .

 6 5: Computing time and memory used. 𝐴𝐹 (𝐺𝑒𝑡𝑇 𝑎𝑠𝑘 𝐼 𝐷 2 [𝑡𝑎𝑠𝑘 2 .𝑐𝑜𝑟𝑒_𝑖𝑑] > 0)

	Number of cores	2	3
	Model-checker result	false	false
	Memory used	56.6MB	114.0MB
	Computing time	2.6s	3.7s

Table 6 .

 6 6: Computing time and memory used after correction.

		𝐴𝐹 (𝐺𝑒𝑡𝑇 𝑎𝑠𝑘 𝐼 𝐷 2 [𝑡𝑎𝑠𝑘 2 .𝑐𝑜𝑟𝑒_𝑖𝑑] > 0)
	Number of cores	2	3
	Model-checker result	true	true
	Memory used	96.7MB	150.1MB
	Computing time	13.3s	914.8s

Table 7 .

 7

	1: Three-tasks application set characteristics.
	𝐴 𝑖 𝐷 𝑖 𝑇 𝑖 𝐶 𝑖 : [bcet,wcet] Transitions
	𝑡𝑎𝑠𝑘 1 0 32 32	[8,11]	Run 11
		+ [2,2]	Run 12
	𝑡𝑎𝑠𝑘 2 0 32 32	[8,8]	Run 21
	𝑡𝑎𝑠𝑘 3 0 16 16	[10,10]	Run 31

Table 7 .

 7 The result of Roméo synthesis is (10 < 𝑎 ≤ 11) ∧ (10 < 𝑏 ≤ 11) ∧ (𝑎 ≤ 𝑏), thus the execution time of 𝑡𝑎𝑠𝑘 1 must be in the interval ]10, 11]. The computing time and used memory for this analysis are shown in the table 7.2, page 125, and parametric model-Schedule of tasks set with the WCET 1 . The symbols ↑ and ↓ indicate activation and completion of tasks, respectively. 2: Three-tasks application: Computing time and memory used.𝐴𝐺 (𝑂𝑏𝑠 1 < 1 𝑎𝑛𝑑 𝑂𝑏𝑠 2 < 1 𝑎𝑛𝑑 𝑂𝑏𝑠 3 < 1)

			2	4	6	8 10 12 14 16 18 20 22 24 26 28 30 32
	Core 1	𝑡𝑎𝑠𝑘 3	2 31 (job 1 ) 4 6 8 10 12 14 16 18 20 22 24 26 28 30 32 31 (job 2 )
		𝑡𝑎𝑠𝑘 2			21 (job 1 )
	Core 0	𝑡𝑎𝑠𝑘 1	2	4 11 (job 1 ) 12 6 8 10 12 14 16 18 20 22 24 26 28 30 32
			Partitioned FP scheduling	𝑡𝑖𝑚𝑒
	Figure 7.4:

  Boukir et al. have already modified the scheduling policy of Trampoline in Global EDF and EDF-US[𝜉] based on the RTOS model built by Tigori in Uppaal [111]. Significant modifications have been done, making the subject of a Ph.D. thesis [112]. However, the task execution time representation is considered discrete. The principal idea was in fact to verify the implementations of the schedulers.

Table 7 .

 7 3: Tasks set characteristics. 𝐴 𝑖 𝐷 𝑖 𝑇 𝑖 𝐶 𝑖 : [bcet,wcet] HSwPN Transition Figure 7.7: Schedule of tasks set with the BCET 3 . The symbols ↑ and ↓ indicate activation and completion of tasks, respectively. Schedule of tasks set with Roméo. The symbols ↑ and ↓ indicate activation and completion of tasks, respectively.

	𝑡𝑎𝑠𝑘 1 0 10 10	[4,4]	Run 11
	𝑡𝑎𝑠𝑘 2 1 20 20	[5,5]	Run 21
	𝑡𝑎𝑠𝑘 3 0 10 10 [3,6] [3,𝑏]	Run 31
	𝑡𝑎𝑠𝑘 4 2 20 20 [3,3] [𝑎,𝑎]	Run 41

Table 7 .

 7 4: Response time computation using the parametric observer.

	Response time	𝐴𝐺 (𝑂𝑏𝑠 𝑖 < 1)	Memory Computing time
	𝑡𝑎𝑠𝑘 1	𝑅 1 = 7, (𝑑 1 > 7)	273.4MB	81.7s
	𝑡𝑎𝑠𝑘 2	𝑅 2 = 8, (𝑑 2 > 8)	254.8MB	72.2s
	𝑡𝑎𝑠𝑘 3	𝑅 3 = 11, (𝑑 3 > 11) 332.1MB	88.0s
	𝑡𝑎𝑠𝑘 4	𝑅 4 = 3, (𝑑 4 > 3)	260.6MB	70.6s

  Figure 7.9: Schedule of tasks set with the WCET 3 . The symbols ↑ and ↓ indicate activation and completion of tasks, respectively. Here job 1 of 𝑡𝑎𝑠𝑘 3 misses its deadline as indicated by the dashed red circle.

			1	2	3	4	5	6	7	8	9 10 11 12 13 14 15 16 17 18 19 20
	Core 1	𝑡𝑎𝑠𝑘 3	1	2	3 (job 1 ) 4	5	6	7	8	9 10 11 12 13 14 15 16 17 18 19 20 (job 2 )
		𝑡𝑎𝑠𝑘 2						(job 1 )
			1	2	3	4	5	6	7	8	9 10 11 12 13 14 15 16 17 18 19 20
	Core 0	𝑡𝑎𝑠𝑘 4	1	2	3 (job 1 ) 4	5	6	7	8	9 10 11 12 13 14 15 16 17 18 19 20
		𝑡𝑎𝑠𝑘 1					(job 1 )		(job 2 )
			Ad-hoc scheduling		𝑡𝑖𝑚𝑒

The database on http://www.informatik.uni-hamburg.de/TGI/PetriNets/tools/db.html provides an overview of existing tools for Petri Nets.

3. http://www.laas.fr/tina

Calling the scheduler another time.

An OS-Application is an object allowing to gather tasks, ISR, ... to assign them to a computing core but also to restrict interactions between objects belonging to different OS-Applications in order to improve security and safety.

𝑡 𝑝𝑙_𝑠𝑐ℎ𝑒𝑑𝑢𝑙𝑒_𝑠𝑒𝑟𝑣𝑖𝑐𝑒 calls 𝑡 𝑝𝑙_𝑠𝑡𝑎𝑟𝑡 () and 𝑡 𝑝𝑙_𝑝𝑟𝑒𝑒𝑚 𝑝𝑡 ()

at least for the microcontrollers that have it

In the example in this section and in the examples that follow we present models designed with the tool Roméo. In this tool, $𝑎𝑛𝑦 is used instead of 𝑎𝑛𝑦 in guards and updates for syntactic reasons but both have the same meaning.

int[START_REF] Group | OSEK/VDX Operating System Specification tech[END_REF] endOfGSL = {0 , 0};

int[START_REF] Group | OSEK/VDX Operating System Specification tech[END_REF] endOfRSL = {0 , 0};

The two double dots (::) are equivalent to an arc in the model. This syntax proposed by Roméo allows a clear and better organization of the Petri subnet in different XML files, which form only one Petri net. Thus a function call is ensured by the following syntax: the XML file name of the Petri subnet:: the place name to which we want to send a token.

The state READY_AND_NEW is identical to the state READY but the execution context of the task is not yet initialized.

𝑊𝐶𝐸𝑇 corresponds to the worst execution time of the code between two service calls, and 𝐵𝐶𝐸𝑇 to the best case execution time of the code between two service calls.

They are available in the Trampoline repository: https://github.com/TrampolineRTOS/

𝑚𝑐_𝑎𝑙𝑎𝑟𝑚𝑠_𝑠1 to 𝑚𝑐_𝑡𝑎𝑠𝑘𝑇 𝑒𝑟𝑚𝑖𝑛𝑎𝑡𝑖𝑜𝑛_𝑠2 except 𝑚𝑐_𝑡𝑎𝑠𝑘𝑇 𝑒𝑟𝑚𝑖𝑛𝑎𝑡𝑖𝑜𝑛_𝑠1, 𝑚𝑐_𝑠𝑐ℎ𝑒𝑑𝑡𝑎𝑏𝑙𝑒𝑠_𝑠1, and 𝑚𝑐_𝑎𝑢𝑡𝑜𝑠𝑡𝑎𝑟𝑡_𝑠3: https://github.com/TrampolineRTOS/trampoline/tree/master/tests/ functional

read and/or write variables. When it is a variable of the modeled system, one must be careful to reproduce the competition situations of the real system. Therefore the modification of a shared variable accessible in concurrency situations must be cut in two: the reading on a transition and the writing on the following transition.

Multi-core RTOS modeling

The source code of Trampoline includes both the single-core and the multi-core versions. To unify the code of the two versions, a set of macros allows us to generate adequate code according to whether we compile for multi-core or single-core. The RTOS model is composed of the API services and the kernel. Each modeled Trampoline source code function is described by a Petri subnet and, if needed, by a Roméo function defined in a C-like syntax. Roméo tool allows using a variable 𝑎𝑛𝑦, which gives the value of the color used for the transition firing.

A global lock prevents concurrent execution of the kernel by the cores in the multicore implementation of Trampoline. This lock is acquired when calling an OS service by an application task. We represented it by a boolean variable serving as a guard on the transitions modeling the service call. The transition is fireable if the variable is false, and once the transition is fired, the variable is set to true when the transition is fired.

API services modeling

The API contains the various services available to the application. The API function calls allow the application's tasks to access the requested service in user mode. As we presented in 3.5.2, a service is called on a core by entering kernel mode. The kernel

Properties of the model

In the absence of an application, the model of the OS kernel remains in its initial state. We study the properties of OS kernel state space when it is called upon by any application.

The variables and the code of the kernel are included in the model. Let N = (𝑃, 𝑇, 𝑋, 𝐶, pre, post, (𝑚 0 , 𝑥 0 ), 𝑔𝑢𝑎𝑟𝑑, 𝑢 𝑝𝑑𝑎𝑡𝑒, 𝐼) the HCTPN model of the OS. The set 𝑋 is the set of variables of the OS. The state of program pointers is given by the marking. An observable state 𝑠 = (𝑀, 𝑥) of the model is a marking 𝑀 and a valuation 𝑥 of 𝑋.

All the states would be observable by modeling the OS kernel with an assembler instruction per Petri net transition. We would get a perfectly equivalent net to the kernel but at the cost of a state space explosion.

Atomicity avoids this explosion and allows conciseness of the model, but this means that all the states of the kernel are not observable and are not in the state space of the model.

Recall that all the instructions associated with a transition 𝑡 ∈ 𝑇 are executed sequentially (as the real code of the kernel on a given core) and considered as atomic in the state space. For observing a particular state enclosed in a sequence of instructions associated with a transition 𝑡, you only need to add a place in the Petri Net at the point you want to observe.

The use of colors allows the simultaneous enabling of transitions for different cores, but the kernel access is sequenced thanks to a global lock, and atomicity is applied on

FORMAL VERIFICATION OF THE

MULTI-CORE AUTOSAR OS COMPLIANCE

Introduction

This chapter presents a formal process to verify multi-core OS compliance with the AUTOSAR standard and the synchronization mechanisms involved in the concurrent execution of OS services. AUTOSAR conformance testing is based on requirements verification by executing a test suite. The first part focuses on multi-core OS requirements, of which there are 80. Each requirement is formalized by an observer that evaluates compliance. The approach results conclude that the operating system model respects the AUTOSAR specifications. The second part of the verification is based on rare situations with simultaneous service calls in parallel on several cores that are almost impossible to test on real implementation. However, errors can be automatically identified with the model-checking method.

Formal verification of AUTOSAR compliance

We propose an approach based on model-checking to verify the conformity of the operating system to the AUTOSAR standard. Figure 6.1 shows the two main stages of the process. The first phase involves developing a complete model that includes all the OS and application functions and services as represented in chapter 5. The verification phase is based on two possible formalizations of properties with model-checking: (i) expressing them formally with temporal logic to be verified by the model-checker, and (ii) adding Petri nets as external observers able to evaluate the respect of the requirements. In the first case, the TCTL logic allows expressing requirements as properties in Roméo. However, these requirements can easily become difficult to express by involving several above, 𝑎𝑙𝑟𝑒𝑎𝑑𝑦_𝑡𝑎𝑘𝑒𝑛, 𝑛𝑜𝑡_𝑠𝑢𝑐𝑐𝑒𝑠𝑠𝑜𝑟, 𝑙𝑜𝑐𝑘_𝑖𝑠𝑟, and 𝑙𝑜𝑐𝑘_𝑡𝑎𝑠𝑘, and defines the correct nesting of spinlocks to avoid deadlocks. Task 𝑡1 runs on Core 0, task 𝑡2 and the Cat2 Interrupt Service Routine 𝐼𝑆𝑅2 run on Core 1 such that task 𝑡2 has a lower priority than 𝐼𝑆𝑅2. Cat2 ISRs are supported by OSEK and can make OS calls that may cause a rescheduling. Task 𝑡1 is an autostart task that begins automatically at system start-up. It calls a set of spinlock API services as shown in Figure 6.6. First, it gets two times the same spinlock 𝑎𝑙𝑟𝑒𝑎𝑑𝑦_𝑡𝑎𝑘𝑒𝑛 with the 𝐺𝑒𝑡𝑆 𝑝𝑖𝑛𝑙𝑜𝑐𝑘 service and ends with the activation of task 𝑡2 on core 1. Task 𝑡2 tries to get the spinlock 𝑙𝑜𝑐𝑘_𝑡𝑎𝑠𝑘 that Core 0 has. It has an execution budget with protection time enabled. Once its execution budget is consumed, the operating system module calls the 𝑃𝑟𝑜𝑡𝑒𝑐𝑡𝑖𝑜𝑛𝐻𝑜𝑜𝑘 () function that sends a software interrupt to the interrupt handler to enable the core1's 𝐼𝑆𝑅2. This application verifies the requirements from 𝑆𝑊 𝑆_𝑂𝑠_00649 to 𝑆𝑊 𝑆_𝑂𝑠_00661 listed in Table A.1.

Application model

The application model gathers the models of the two tasks and 𝐼𝑆𝑅2, which constitute it. 𝐼𝑆𝑅2 is considered a process activated by the software interrupt sent at the end of task t2 execution. Its detailed model is represented in Figure 6.7. It starts with calling the 𝐺𝑒𝑡𝑆 𝑝𝑖𝑛𝑙𝑜𝑐𝑘 service twice to acquire the same spinlock 𝑎𝑙𝑟𝑒𝑎𝑑𝑦_𝑡𝑎𝑘𝑒𝑛 and then follows up with a set of service calls. Each service call represents a requirement check scenario. For example, the error 𝐸_𝑂𝑆_𝐼 𝑁𝑇 𝐸 𝑅𝐹𝐸 𝑅𝐸 𝑁𝐶𝐸_𝐷𝐸 𝐴𝐷 𝐿𝑂𝐶𝐾 is expected on the second attempt to get the spinlock because it already belongs to the calling core.

Verification results

We conduct the verification on the elaborated application model by adding the observers. All the requirements tested by this application are formalized. Figure 6.8 shows the observer models verifying the requirements SWS_Os_00650 and SWS_Os_00651. Both requirements concern the ability to call 𝐺𝑒𝑡𝑆 𝑝𝑖𝑛𝑙𝑜𝑐𝑘 from tasks and ISR2s and are checked through the same function 𝑆𝑊 𝑆_650_651_𝑂𝑏𝑠𝑒𝑟𝑣𝑒𝑟. The first field of the 𝑏𝑜𝑜𝑙𝑒𝑎𝑛_650_651 data structure, 𝑐𝑜𝑛𝑑𝑖𝑡𝑖𝑜𝑛1, triggers the observer of requirement SWS_Os_00650 when the task is running. Similarly, the second field, 𝑐𝑜𝑛𝑑𝑖𝑡𝑖𝑜𝑛2, triggers the observer of requirement SWS_Os_00651 when the 𝐼𝑆𝑅2 is executed. The observers end their verification with the kernel-mode exit condition via the third field 𝑐𝑜𝑛𝑑𝑖𝑡𝑖𝑜𝑛3, reset with the check of each trigger condition. The description of the requirements from 𝑆𝑊 𝑆_𝑂𝑠_00649 to 𝑆𝑊 𝑆_𝑂𝑠_00661, verified by this test sequence, are found in Table A.1. The property (p)->(q) is satisfied by the Roméo model-checker for each requirement observer, such that 𝑝 represents the first place and 𝑞 the last place of the observer. The verification time in seconds and the memory consumed in MB for each observer verification are included in Table 6.2. For all verifications, the result is true.

Discussion

In our verification process, the computer on which the verification is conducted has a quad-core Intel Core i5 processor running at 2.4 GHz and a RAM of 16 GB. We were not confronted with the combinatorial explosion problem of the state spaces. The combinatorial explosion can be induced by the multi-core interleaving scenarios such that all

FORMAL SCHEDULABILITY ANALYSIS BASED ON MULTI-CORE RTOS MODEL

Introduction

Verification of real-time application schedulability is usually performed using a very abstract system representation, which poorly supports inter-task dependencies. This chapter presents the schedulability analysis of the application running on the multicore operating system model using model-checking techniques. Verification is performed using observers and allows determining the multi-core application's schedulability. Using parameters on the firing intervals allows determining under which temporal conditions the application is schedulable. The multi-core has considerably complicated the scheduling problem, and a greater confidence in new scheduling policies implementation would be achieved by verifying them formally within the RTOS model. Simulation approaches quickly reach their limit as there is parallelism, so model-checking is adapted to multi-core context considering the parallelism, concurrency, and preemption provided state space explosion can be avoided. We show the possibility of verifying new partitionned scheduling policies within the multi-core RTOS using the HCTPN model. To illustrate this possibility with an example, we modify the Trampoline scheduling policy with an ad-hoc scheduler and verify its specifications and the application schedulability. This approach can be used not only to test new scheduling policies, but also to verify a scheduler for its implementation.

Parameters synthesis

The parametric analysis of HCTPNs with stopwatches using Roméo allows synthesizing the parameter values used in the time bounds of the transitions, such that the model verifies the TCTL properties [START_REF] Lime | Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches in 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems[END_REF]. It also allows adding linear constraints on the parameters to restrict their domain. The reachability problem is undecidable for HCTPNs with stopwatches and parametric HCTPNs with stopwatches, and semi-algorithms are implemented in Roméo for these models with polyhedra using the Parma Polyhedra Library [109]. For parametric models, the semi-algorithms are based on the parametric state-class graph [110]. For a given formula, by computing the parametric state space, Roméo synthesize a set of linear constraints over parameters which represents the values of the parameters for which the formula is verified. Parameters can replace any interval bound, such as an offset, the BCET, or the WCET of a task model. Given a property 𝜑, checking 𝜑 with Roméo will synthesize the set of values of the parameters such that 𝜑 is true. For example, by parametrizing the BCET and WCET of a task 𝑡𝑎𝑠𝑘 𝑖 and by using the previous observer, checking 𝐴𝐺 (𝑂𝑏𝑠 𝑖 < 1) will synthesize all the linear constraints over the parameters BCET and WCET such that 𝑡𝑎𝑠𝑘 𝑖 respects its deadline.

• 𝑡𝑎𝑠𝑘 1 and 𝑡𝑎𝑠𝑘 4 are assigned to run on core 0;

• 𝑡𝑎𝑠𝑘 2 and 𝑡𝑎𝑠𝑘 3 are assigned to run on core 1;

• 𝑃𝑟𝑖𝑜(𝑡𝑎𝑠𝑘 1 ) < 𝑃𝑟𝑖𝑜(𝑡𝑎𝑠𝑘 4 );

• When 𝑡𝑎𝑠𝑘 4 runs on core 0, 𝑃𝑟𝑖𝑜(𝑡𝑎𝑠𝑘 2 ) < 𝑃𝑟𝑖𝑜(𝑡𝑎𝑠𝑘 3 ) otherwise 𝑃𝑟𝑖𝑜(𝑡𝑎𝑠𝑘 3 ) < 𝑃𝑟𝑖𝑜(𝑡𝑎𝑠𝑘 2 ).

The requirements of this ad-hoc policy lead to the rescheduling of 𝑡𝑎𝑠𝑘 2 and 𝑡𝑎𝑠𝑘 3 on core 1 once the activation or termination of 𝑡𝑎𝑠𝑘 1 and 𝑡𝑎𝑠𝑘 4 occur on core 0. When the scheduler is called for core 0, it is based on the job currently running on that core (i.e., 𝑡𝑎𝑠𝑘 1 or 𝑡𝑎𝑠𝑘 4 ) and calculates the priority of 𝑡𝑎𝑠𝑘 2 or 𝑡𝑎𝑠𝑘 3 jobs for core 1. It then decides whether a context switch is required on a core and have to be achieved. Thus, two events cause the rescheduling: (i) activation of new 𝑡𝑎𝑠𝑘 1 and 𝑡𝑎𝑠𝑘 4 jobs on core 0; (ii) termination of these tasks jobs running on core 0. That means, for example, 𝑡𝑎𝑠𝑘 2 continues to run on core 1 until 𝑡𝑎𝑠𝑘 3 preempts because 𝑡𝑎𝑠𝑘 4 is activated on core 0. The priority of 𝑡𝑎𝑠𝑘 2 and 𝑡𝑎𝑠𝑘 3 are recalculated such that: 𝑃𝑟𝑖𝑜(𝑡𝑎𝑠𝑘 2 ) < 𝑃𝑟𝑖𝑜(𝑡𝑎𝑠𝑘 3 ). 𝑡𝑎𝑠𝑘 3 starts thus running on core 1 until it is preempted when 𝑡𝑎𝑠𝑘 4 terminates on core 0. We only allow one possible activation of the job and use the Roméo model model-checker to analyze the system.

Ad-hoc scheduler implementation

The scheduler implementation within Trampoline relies on functions and data structures that are manipulated and involved in making decisions as presented in Section 3.5.1, page 46. Among these functions, we find the internal scheduler function 𝑡 𝑝𝑙_𝑠𝑡𝑎𝑟𝑡, called by the main scheduling function 𝑡 𝑝𝑙_𝑠𝑐ℎ𝑒𝑑𝑢𝑙𝑒_ 𝑓 𝑟𝑜𝑚_𝑟𝑢𝑛𝑛𝑖𝑛𝑔, that invokes the scheduler, whether in mono-core or multi-core. 𝑡 𝑝𝑙_𝑠𝑡𝑎𝑟𝑡 allows updating the 𝑒𝑙𝑒𝑐𝑡𝑒𝑑_𝑖𝑑 attribute of the 𝑡 𝑝𝑙_𝑘𝑒𝑟𝑛 structure with the identifier value of the job elected to run on the core. Since the two events that cause rescheduling are job activation and termination, our modification work focuses on the scheduler's internal function 𝑡 𝑝𝑙_𝑠𝑡𝑎𝑟𝑡 called in both cases, at activation by the function 𝑡 𝑝𝑙_𝑠𝑐ℎ𝑒𝑑𝑢𝑙𝑒_ 𝑓 𝑟𝑜𝑚_𝑟𝑢𝑛𝑛𝑖𝑛𝑔 and termination by 𝑡 𝑝𝑙_𝑡𝑒𝑟𝑚𝑖𝑛𝑎𝑡𝑒_𝑠𝑒𝑟𝑣𝑖𝑐𝑒, as shown in Figure 7.6, page 128. This figure also illustrates the other parts concerned with a change, presented in the following, to implement the ad-hoc scheduler in the model. Once the scheduler modified, the four-tasks applica-

PUBLICATIONS

International conferences