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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We adapt an existing preemptive scheduling model of RTOS kernel by eChronosfrom machine-assisted proof to Spin-based model checker. The model weconstructed can be automatically verified rather than formulating proofs byhand. Moreover, we look into the designs of a Linux-like real-timekernel--Piko/RT and the specification of ARMv7-M architecture to reconstructthe model, and use LTL to specify a simple concurrentprograms--consumer/producer problem during the development stage of the kernel.We show that under the preemptive scheduling and the mechanism of ARMv7-M, theprogram will not suffer from race condition, starvation, and deadlock.

A Spin-based model checking for the simple concurrent program on a preemptive RTOS