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.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:635128 |
| Date | January 2014 |
| Creators | Capper, John |
| Publisher | University of Nottingham |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://eprints.nottingham.ac.uk/27759/ |
Page generated in 0.1691 seconds