Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP

DOI10.1007/978-3-030-15792-0_10zbMath1486.68045OpenAlexW2935786612MaRDI QIDQ5861786

Kangfeng Ye, Simon Foster, J. C. P. Woodcock

Publication date: 2 March 2022

Published in: From Astrophysics to Unconventional Computation (Search for Journal in Brave)

Full work available at URL: https://eprints.whiterose.ac.uk/129640/15/Compositional_Assume_Guarantee_Reasoning_of_Control_Law_Diagrams_using_UTP_Tech_Report.pdf

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20) Mathematical modeling or simulation for problems pertaining to systems and control theory (93-10)

Related Items (3)

A contract-based semantics and refinement for Simulink ⋮ Automated reasoning for probabilistic sequential programs with theorem proving ⋮ A denotational semantics of simulink with higher-order UTP

Uses Software

• Isabelle
• Isabelle/HOL
• HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Contract-based verification of MATLAB-style matrix programs
• Isabelle/HOL. A proof assistant for higher-order logic
• Unifying theories of reactive design contracts
• Mechanically proving determinacy of hierarchical block diagram translations
• Isabelle/UTP: A Mechanised Theory Engineering Framework
• Simulink Timed Models for Program Verification
• Process algebra for synchronous communication
• Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems
• Unifying Theories in ProofPower-Z
• FDR3 — A Modern Refinement Checker for CSP
• FM 2005: Formal Methods
• Integrated Formal Methods

This page was built for publication: Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP