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

We are interested in verifying dynamic properties of finite state reactivesystems under fairness assumptions by model checking. The systems we want toverify are specified through a top-down refinement process. In order to dealwith the state explosion problem, we have proposed in previous works topartition the reachability graph, and to perform the verification on each partseparately. Moreover, we have defined a class, called Bmod, of dynamicproperties that are verifiable by parts, whatever the partition. We decide if aproperty P belongs to Bmod by looking at the form of the Buchi automaton thataccepts the negation of P. However, when a property P belongs to Bmod, theproperty f => P, where f is a fairness assumption, does not necessarily belongto Bmod. In this paper, we propose to use the refinement process in order tobuild the parts on which the verification has to be performed. We then showthat with such a partition, if a property P is verifiable by parts and if f isthe expression of the fairness assumptions on a system, then the property f =>P is still verifiable by parts. This approach is illustrated by its applicationto the chip card protocol T=1 using the B engineering design language

PLTL-partitioned model checking for reactive systems under fairness assumptions