Semantic methods for functional hybrid modelling
Equation-based modelling languages have become a vital tool in many areas of science and engineering. Functional Hybrid Modelling (FHM) is an approach to equation-based modelling that allows the behaviour of a physical system to be expressed as a modular hierarchy of undirected equations. FHM suppor...
| Main Author: | |
|---|---|
| Format: | Thesis (University of Nottingham only) |
| Language: | English |
| Published: |
2014
|
| Online Access: | https://eprints.nottingham.ac.uk/27759/ |
| _version_ | 1848793431348871168 |
|---|---|
| author | Capper, John |
| author_facet | Capper, John |
| author_sort | Capper, John |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | Equation-based modelling languages have become a vital tool in many areas of science and engineering. Functional Hybrid Modelling (FHM) is an approach to equation-based modelling that allows the behaviour of a physical system to be expressed as a modular hierarchy of undirected equations. FHM supports a variety of advanced language features — such as higher-order models and variable system structure — that sets it apart from the majority of other modelling languages. However, the inception of these new features has not been accompanied by the semantic tools required to effectively use and understand them. Specifically, there is a lack of static safety assurances for dynamic models and the semantics of the aforementioned language features are poorly understood.
Static safety guarantees are highly desirable as they allow problems that may cause an equation system to become unsolvable to be detected early, during compilation. As a result, the use of static analysis techniques to enforce structural invariants (e.g. that there are the same number of equations as unknowns) is now in use in main-stream equation-based languages like Modelica. Unfortunately, the techniques employed by these languages are somewhat limited, both in their capacity to deal with advanced language features and also by the spectrum of invariants they are able to enforce.
Formalising the semantics of equation-based languages is also important. Semantics allow us to better understand what a program is doing during execution, and to prove that this behaviour meets with our expectation. They also allow different implementations of a language to agree with one another, and can be used to demonstrate the correctness of a compiler or interpreter. However, current attempts to formalise such semantics typically fall short of describing advanced features, are not compositional, and/or fail to show correctness. This thesis provides two major contributions to equation-based languages.
Firstly, we develop a refined type system for FHM capable of capturing a larger number of structural anomalies than is currently possible with existing methods. Secondly, we construct a compositional semantics for the discrete aspects of FHM, and prove a number of key correctness properties. |
| first_indexed | 2025-11-14T19:00:11Z |
| format | Thesis (University of Nottingham only) |
| id | nottingham-27759 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T19:00:11Z |
| publishDate | 2014 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-277592025-02-28T11:32:19Z https://eprints.nottingham.ac.uk/27759/ Semantic methods for functional hybrid modelling Capper, John Equation-based modelling languages have become a vital tool in many areas of science and engineering. Functional Hybrid Modelling (FHM) is an approach to equation-based modelling that allows the behaviour of a physical system to be expressed as a modular hierarchy of undirected equations. FHM supports a variety of advanced language features — such as higher-order models and variable system structure — that sets it apart from the majority of other modelling languages. However, the inception of these new features has not been accompanied by the semantic tools required to effectively use and understand them. Specifically, there is a lack of static safety assurances for dynamic models and the semantics of the aforementioned language features are poorly understood. Static safety guarantees are highly desirable as they allow problems that may cause an equation system to become unsolvable to be detected early, during compilation. As a result, the use of static analysis techniques to enforce structural invariants (e.g. that there are the same number of equations as unknowns) is now in use in main-stream equation-based languages like Modelica. Unfortunately, the techniques employed by these languages are somewhat limited, both in their capacity to deal with advanced language features and also by the spectrum of invariants they are able to enforce. Formalising the semantics of equation-based languages is also important. Semantics allow us to better understand what a program is doing during execution, and to prove that this behaviour meets with our expectation. They also allow different implementations of a language to agree with one another, and can be used to demonstrate the correctness of a compiler or interpreter. However, current attempts to formalise such semantics typically fall short of describing advanced features, are not compositional, and/or fail to show correctness. This thesis provides two major contributions to equation-based languages. Firstly, we develop a refined type system for FHM capable of capturing a larger number of structural anomalies than is currently possible with existing methods. Secondly, we construct a compositional semantics for the discrete aspects of FHM, and prove a number of key correctness properties. 2014-12-09 Thesis (University of Nottingham only) NonPeerReviewed application/pdf en arr https://eprints.nottingham.ac.uk/27759/1/thesis.pdf Capper, John (2014) Semantic methods for functional hybrid modelling. PhD thesis, University of Nottingham. |
| spellingShingle | Capper, John Semantic methods for functional hybrid modelling |
| title | Semantic methods for functional hybrid modelling |
| title_full | Semantic methods for functional hybrid modelling |
| title_fullStr | Semantic methods for functional hybrid modelling |
| title_full_unstemmed | Semantic methods for functional hybrid modelling |
| title_short | Semantic methods for functional hybrid modelling |
| title_sort | semantic methods for functional hybrid modelling |
| url | https://eprints.nottingham.ac.uk/27759/ |