Verification

> Simulation-based programmable logic controller (PLC) code verification is a part of virtual commissioning, where the control code is verified against a virtual prototype of an application. With today’s general OPC interface, it is easy to connect a PLC to a simulation tool for, e.g., verification purposes. However, there are some problems with this approach that can lead to an unreliable verification result. In this paper, four major problems with the OPC interface are described, and two possible solutions to the problems are presented: a general IEC 61131-3-based software solution, and a new OPC standard solution.

~

Formal Verification of Subsets of the Rust Language | SkillsCast, [no date]. Formal Verification of Subsets of the Rust Language | SkillsCast. Online. [Accessed 25 November 2021]. Available from: https://skillsmatter.com/skillscasts/17053-formal-verification-of-subsets-of-the-rust-languageRust London User Group community cast. Bas Spitters: In this presentation, Bas will give a very brief introduction to interactive formal verification of pro... JEFFREY, Alan, 2012. LTL types FRP: linear-time temporal logic propositions as types, proofs as functional reactive programs. In: Proceedings of the sixth workshop on Programming languages meets program verification - PLPV ’12. Online. Philadelphia, Pennsylvania, USA: ACM Press. 2012. p. 49. [Accessed 21 March 2021]. ISBN 978-1-4503-1125-0. DOI 10.1145/2103776.2103783. JELTSCH, Wolfgang, 2013. Temporal logic with “Until”, functional reactive programming with processes, and concrete process categories. In: Proceedings of the 7th workshop on Programming languages meets program verification - PLPV ’13. Online. Rome, Italy: ACM Press. 2013. p. 69. [Accessed 21 March 2021]. ISBN 978-1-4503-1860-0. DOI 10.1145/2428116.2428128.