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

Timed model checking has been extensively researched in recent years. Manynew formalisms with time extensions and tools based on them have beenpresented. On the other hand, Explicit-Time Description Methods aim to verifyreal-time systems with general untimed model checkers. Lamport presented anexplicit-time description method using a clock-ticking process (Tick) tosimulate the passage of time together with a group of global variables for timerequirements. This paper proposes a new explicit-time description method withno reliance on global variables. Instead, it uses rendezvous synchronizationsteps between the Tick process and each system process to simulate time. Thisnew method achieves better modularity and facilitates usage of more complextiming constraints. The two explicit-time description methods are implementedin DIVINE, a well-known distributed-memory model checker. Preliminaryexperiment results show that our new method, with better modularity, iscomparable to Lamport's method with respect to time and memory efficiency.

Verifying Real-Time Systems using Explicit-time Description Methods