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 Tools annual

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 monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Programmable Logic Controllers (PLCs) provide a prominent choice ofimplementation platform for safety-critical industrial control systems. Formalverification provides ways of establishing correctness guarantees, which can bequite important for such safety-critical applications. But since PLC code doesnot include an analytic model of the system plant, their verification islimited to discrete properties. In this paper, we, thus, start the other wayaround with hybrid programs that include continuous plant models in addition todiscrete control algorithms. Even deep correctness properties of hybridprograms can be formally verified in the theorem prover KeYmaera X thatimplements differential dynamic logic, dL, for hybrid programs. After verifyingthe hybrid program, we now present an approach for translating hybrid programsinto PLC code. The new tool, HyPLC, implements this translation of discretecontrol code of verified hybrid program models to PLC controller code and, viceversa, the translation of existing PLC code into the discrete control actionsfor a hybrid program given an additional input of the continuous dynamics ofthe system to be verified. This approach allows for the generation of realcontroller code while preserving, by compilation, the correctness of a validand verified hybrid program. PLCs are common cyber-physical interfaces forsafety-critical industrial control applications, and HyPLC serves as apragmatic tool for bridging formal verification of complex cyber-physicalsystems at the algorithmic level of hybrid programs with the execution layer ofconcrete PLC implementations.

HyPLC: Hybrid Programmable Logic Controller Program Translation for Verification