Towards a UTP semantics for Modelica

DOI10.1007/978-3-319-52228-9_3MaRDI QIDQ2971175zbMATH OpenOpenAlexFDO

Authors Simon Foster, Bernhard Thiele, Ana Cavalcanti, Jim 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) Formalization of mathematics in connection with theorem provers (68V20) Mathematical modeling or simulation for problems pertaining to systems and control theory (93-10) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Recommendations

• Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
• Towards verification of cyber-physical systems with UTP and Isabelle/HOL
• A Hybrid Denotational Semantics for Hybrid Systems
• A hybrid relational modelling language
• UTP semantics for Handel-C

Cites work

• A calculus of durations
• A Theory of Pointers for the UTP
• Automatic proof and disproof in Isabelle/HOL
• Circus Time with Reactive Designs
• Formal verification of Simulink/Stateflow diagrams
• Generating denotational semantics from algebraic semantics for event-driven system-level language
• scientific article; zbMATH DE number 1670741 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 1487733 (Why is no real title available?)
• scientific article; zbMATH DE number 1507210 (Why is no real title available?)
• Implementation of a modelica compiler using JastAdd attribute grammars
• Isabelle/HOL. A proof assistant for higher-order logic
• Isabelle/UTP: a mechanised theory engineering framework
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Logical analysis of hybrid systems. Proving theorems for complex dynamics.
• The Consistent Initialization of Differential-Algebraic Systems
• Theorem Proving in Higher Order Logics
• Unifying theories for logic programming
• Unifying theories of programming that distinguish nontermination and abort
• UTP semantics for Handel-C

Cited in

(13)

• 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
• A denotational semantics of simulink with higher-order UTP
• Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
• Hybrid relations in Isabelle/UTP
• An Axiomatic Value Model for Isabelle/UTP
• Behavioural models for FMI co-simulations
• Unifying heterogeneous state-spaces with lenses
• Optics
• Shallow Expressions
• Z Mathematical Toolkit in Isabelle/HOL

Describes a project that uses

Uses Software

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

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

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