Towards interactive verification of programmable logic controllers using modal Kleene algebra and KIV

DOI10.1007/978-3-319-24704-5_15MaRDI QIDQ3460629zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Roland Glück, Florian Benedikt Krebs

Publication date 8 January 2016

Published in Relational and Algebraic Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://elib.dlr.de/117312/1/Vortrag_Bern.pdf

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems involving computers (process control, etc.) (93C83)

Recommendations

• Verifying hybrid systems with modal Kleene algebra
• Modal Kleene algebra applied to program correctness
• scientific article; zbMATH DE number 1836374
• Algebraic derivation of until rules and application to timer verification
• Building program construction and verification tools from algebraic principles

Cited in

(3)

• Verifying hybrid systems with modal Kleene algebra
• scientific article; zbMATH DE number 139804 (Why is no real title available?)
• scientific article; zbMATH DE number 1755142 (Why is no real title available?)

Describes a project that uses

Uses Software

• KIV

This page was built for publication: Towards interactive verification of programmable logic controllers using modal Kleene algebra and KIV

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3460629)