Dear readers,
My name is Sadashiv Balawad and I am working as Junior Software Engineer at Luxoft India. Luxoft gave me many opportunities to work on various projects, which inspired me to talk about the importance of multicore Real Time Operating Systems(Part-2)

Motivations
Our goals are two;
1) To test and assess the behavior of the real time operating system (RTOS) by subjecting it to application models that comply with the OSEK/VDX [6]. Autosar [3] standards. This will help determine whether the RTOS meets the standards.
2) To examine the issues related to using this operating system, such, as multi core schedulability, in real time scenarios.

When it comes to understanding the behavior of a core RTOS we face three main challenges;
1) The operating system is influenced by various stimuli, especially those related to real time operations.
2) The applications and code blocks of the operating system are run at the time, on cores.
3) Certain portions of the operating systems code can be executed concurrently by cores, such, as the StartOS service and Spinlock services.

Choice of the model
To achieve this goal we utilize methods, the technique of model checking. Model checking is an approach to handle concurrency and interactions, between parallel processes, which often give rise to errors in systems. These concurrency related errors are intricate and challenging to reproduce or identify during testing due to the interleavings, in the execution of parallel processes. However model checking is excellently suited for detecting concurrency bugs and proving their absence in a system. It relies on exploring the state space of the system model to verify the correctness of properties throughout the execution path.We apply our methodology to Trampoline, a real time operating system that supports cores and complies with OSEK/VDX and AUTOSAR standards.

Because it is written in C, a model-checker running on concurrent C programs like [9] may be useful with the RTOS we are dealing with; however, calling services goes through assembly code that would require to be formally analyzed within the complete hardware architecture model and hence not portable. Additionally, it is not enough to only check for properties of C-program but because they are checked against real-time stimuli causing consequent interruptions. Therefore, we need a time-aware modelchecker since we are taking into account execution times of application tasks. The genericity of the approach does not take into account execution times of OS instruction blocks. Information about timing should hold only for a specific hardware.

employs timed automata that can replicate concurrency and its interleaving. The only problem with it is that it cannot imitate the simultaneous execution of a code sequence on many cores unless the code sequence model itself is cloned. As such, time Petri nets will be used for both concurrent and time modeling. We will add to them by defining colors in such a way that multiple tokens with different colors representing cores on which operations are executed can traverse the same sequence of transitions.

** Scientific contribution**
The results of your thesis provide three main contributions to the goals set in the preceding section. First is the contribution touching on design paradigm for modeling. Since Petri Nets do not by default capture simultaneous access to shared resources and
time, as is often required when controlling multi-core real-time systems, we propose an extension of this formalism with colored transitions and a high-level function i.e., a predefined syntax manipulating different types of expressions made up of variables. Along with sequential pseudo code, High-Level Colored Time Petri Nets includes both timed multi-enablement of transitions and reachability problem that is decidable for this model.To represent the real-time application as a sequence of RTOS system calls instead of the multi-core RTOS that reproduces its control flow, we use this extended formalism, which uses similar variables with implementation ones.
The second contribution has two parts. First is the formal verification of the RTOS conformity to the AUTOSAR standard using test-suite modelling that includes several HCTPN applications. Second, we verify the mechanism for inter-core synchronization in
the context of concurrent OS service execution. AUTOSAR conformance testing relies on requirements checking. For this, we have eighty multi core operating system (OS) requirements.
Each specification is enforced by an evaluator that measures compliance. Observer models are benign i.e. they do not interfere with system operation. The cores are associated with Petri net transition colors. We perform model-checking to validate the AUTOSAR specifications. Result from the approach shows that the present operating system model meets AUTOSAR expectations.
This paper concludes with a focus on verifying simultaneous service calls execution on cores for safety analysis as part of the AUTOSAR compliance veri cation of multi-core RTOS and since these cases are synchronous, they do not include concurrent situations; However, when it comes to verifying simultaneous service calls execution on cores for safety analysis as part of the AUTOSAR compliance veri cation of multi-core RTOS and since these cases are synchronous, they do not include concurrent situations;

fig 2- Formal verification approach
Finally, we offer a verification method to decide the schedulability of real time applications with established preemptive duties on the distinct multi-middle RTOS model. It also allows figuring out beneath which temporal conditions the application is schedulable the usage of parameters at the firing periods. Verification of real-time applications schedulability is commonly accomplished the use of a very abstract device illustration, which poorly supports inter-challenge dependencies. We represent every software mission through a Petri net whose transitions deliver Best-Case Execution Time and Worst-Case Execution Time [𝐵𝐶𝐸𝑇, 𝑊𝐶𝐸𝑇] firing durations and make carrier calls to the OS. Preemption is supported by using stopwatches. We correctly examine worst-case reaction time computation for based preemptive duties in multi-middle structures. Thus, our contribution is a whole method to verifying the schedulability of aactual-time system, the AUTOSAR compliance of multi-center RTOS, and the inter-center synchronization mechanism involved in concurrent OS provider execution the usage of High-Level Colored Time Petri Nets (HCTPN). The technique steps are illustrated in Figure 2 We depend upon the Roméo model-checker device for the verification, to be had beneath a free license

I will try to explain more this topic in next part

Thank you