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

Reactive Promela/RSPIN is an extension to the protocol validator Promela/SPIN. It enhances the simulation and veri cation capabilities of SPIN by allowing modular speci cations to be analysed while alleviating the state-space explosion problem. Reactive Promela is a simple reactive language. The tool RSPIN is a preprocessor for SPIN which translates a Reactive Promela speci cation into a corresponding Promela speci cation. The main function performed by RSPIN is to combine con gurations of Reactive Promela automata into Promela proctypes. The translated speci cation can then be simulated and veri ed using SPIN. We demonstrate the language and tool by the speci cation, translation, simulation and verication of the LAP{B data link protocol. This protocol is quite complex, and bene ts from decomposition.

Protocol verification with reactive PROMELA/RSPIN