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

We present a technique for automatically verifying linear- time tempo- ral logic safety properties of programs written in E STEREL, a formally-defined language for programming reactive systems. In our approach, linear-time tempo- ral logic safety properties are first translated into ESTEREL programs that model these properties. Using the E STEREL compiler, the translations are compiled in parallel with the E STEREL program to be verified. A trivial reachability analysis of the output of the compiler then indicates whether or not th e safety property is satisfied by the program. We describe two real-world software problems — E S- TEREL versions of two features of the AT&T 5ESS R switching system — and one well-known benchmark problem — the generalized railroad cr ossing problem — that we have verified using our technique and associated toolset.

Safety property verification of Esterel programs and applications to telecommunications software