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

Usage control models provide an integration of access control, digitalrights, and trust management. To achieve this integration, usage control modelssupport additional concepts such as attribute mutability and continuity ofdecision. However, these concepts may introduce an additional level ofcomplexity to the underlying model, rendering its definition a cumbersome andprone to errors process. Applying a formal verification technique allows for arigorous analysis of the interactions amongst the components, and thus forformal guarantees in respect of the correctness of a model. In this paper, weelaborate on a case study, where we express the high-level functional model ofthe UseCON usage control model in the TLA+ formal specification language, andverify its correctness for <=12 uses in both of its supporting authorisationmodels.

Formal Verification of Usage Control Models: A Case Study of UseCON Using TLA+