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

The paper relates an industrial experiment performed jointly by LAAS-CNRS and Electricite de France (EdF in short) for assessing the application of a formal method to the reverse engineering of (a part of) a fault-tolerant monitoring system designed for the control room of French N4 nuclear power plants. More specifically, the experiment is devoted to the formal specification and verification of the distributed scheduling algorithm managing the hot redundancy between the two computers composing the system, a single fault hypothesis being assumed for this function. The formal method used for the experiment is RT-LOTOS, a temporal extension of the LOTOS standard Formal Description Technique (FDT in short). The main motivation behind the experiment was to get a better understanding of the fault-tolerant features of the scheduling algorithm by means of both simulation and formal verification.

springer ebooks

An experiment in using RT-LOTOS for the formal specification and verification of a distributed scheduling algorithm in a nuclear power plant monitoring system