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

A railway interlocking system is one example of a critical system, and, therefore, it must have a high level of reliability in order to avoid problems that may result on the loss of people's lives. However, many railway systems are still specified using historical relay-based diagrams, whose analysis are made by human inspection, which is error prone. Relay-based diagrams are specified by nodes and cables in a graphical manner, which resemble undirected graphs. This paper presents a framework for the specification of relay diagrams in a formal language, B-method, based on the specification of a graph and its properties. The use of a formal language allows one to prove the correctness of these railway interlocking systems regarding structural properties. This framework has been evaluated by the specification of a case study.

A Framework for the Formal Specification of Relay-Based Systems Based on a b-Method Graph Specification