English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Safety-critical systems should demonstrate functional safety and correctness through formal methods, as recommended by regulation authorities and international standards such as IEC-61508 [1] and DO-178B/C [2]. ‘Qplus-AIR’ [3]–[6] is a recently-developed real-time operating system (RTOS) for avionics, complying with ARINC-653 specification [7], and it is a DO-178B certifiable RTOS. Scheduling and synchronization services are critical components of RTOS that are being used in safety-critical applications [8]. The applications typically structured in sets of process (i.e., tasks) that share resources via the RTOS. In such contexts, Qplus-AIR should guarantee and demonstrate its correctness for scheduling all tasks on various operating environments and conditions. This paper reports a formal verification result about ‘Qplus-653,’ which is a kernel core of Qplus-AIR. The formal verification used the model checker, Times [9], to verify the correctness of Qplus-653. By looking into the source code of Qplus-653, we first modeled various tasks of Qplus653 using timed automata [10] and then performed model checking with Times to check whether the scheduler of Qplus-653 schedules all tasks successfully in accordance with the prioritized preemptive strategy. Timed automata has been used to verify correctness of real time systems. In order to check whether timing requiremts of tasks are met, [11], [12] set deadline miss states of the tasks in the real time system models and conducted reachability analysis for the states using model checkers such as UPPAAL and Times.

Timed Model-Based Formal Analysis of a Scheduler of Qplus-AIR, an ARINC-653 Compliance RTOS