Towards a UTP Semantics for Modelica

DOI10.1007/978-3-319-52228-9_3zbMath1483.68053OpenAlexW2569046096MaRDI QIDQ2971175

Bernhard Thiele, Simon Foster, Ana Cavalcanti, J. C. P. Woodcock

Publication date: 4 April 2017

Published in: Unifying Theories of Programming (Search for Journal in Brave)

Full work available at URL: https://eprints.whiterose.ac.uk/105107/1/utp2016.pdf

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30) 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 (6)

Behavioural Models for FMI Co-simulations ⋮ Unifying Heterogeneous State-Spaces with Lenses ⋮ Unifying theories of time with generalised reactive processes ⋮ Unifying theories of reactive design contracts ⋮ On checking equivalence of simulation scripts ⋮ Integration of formal proof into unified assurance cases with Isabelle/SACM

Uses Software

• Isabelle
• Isabelle/HOL
• Sledgehammer
• Handel-C
• Isabelle/Circus
• Transfer
• Lifting
• Isabelle/UTP
• Circus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A calculus of durations
• Isabelle/HOL. A proof assistant for higher-order logic
• Implementation of a modelica compiler using JastAdd attribute grammars
• Isabelle/UTP: A Mechanised Theory Engineering Framework
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Generating Denotational Semantics from Algebraic Semantics for Event-Driven System-Level Language
• Automatic Proof and Disproof in Isabelle/HOL
• Circus Time with Reactive Designs
• Formal Verification of Simulink/Stateflow Diagrams
• Unifying Theories of Programming That Distinguish Nontermination and Abort
• UTP Semantics for Handel-C
• The Consistent Initialization of Differential-Algebraic Systems
• Logical Analysis of Hybrid Systems
• Theorem Proving in Higher Order Logics
• A Theory of Pointers for the UTP

This page was built for publication: Towards a UTP Semantics for Modelica