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

This paper describes how, as a very important part in the development of the protocol, verifications for a developed protocol specification are complementary techniques that are used to increase the level of confidence in the system functions by their specifications. Using the informal method for specifying the protocol, a little ambiguity may be contained in the protocol. This indwelling ambiguity in control systems can be the cause of accidents, especially for safety-critical systems. To clear the ambiguity contained in the designed protocol, we use the Labelled Transition System (LTS) model to design the standard protocol for railway signaling systems. Then the paper verifies the safety and liveness properties automatically and formally through the model checking method. The modal µ-calculus, which is an expressive method of temporal logic, has been applied to the model checking method. This paper verifies the safety and liveness properties of the Korean standard protocol for railway signaling systems. To automatically check the safety and liveness properties of the designed protocol, the formal checker is implemented. The developed tools are implemented by the C++ language under Windows XP.

Model checker for railway signalling communication protocol