| dc.description.abstract | Safety critical systems place additional requirements to the programming
language used to implement them with respect to traditional environments.
Examples of features that in
uence the suitability of a programming language
in such environments include complexity of de nitions, expressive
power, bounded space and time and veri ability. Hume is a novel programming
language with a design which targets the rst three of these, in some
ways, contradictory features: fully expressive languages cannot guarantee
bounds on time and space, and low-level languages which can guarantee
space and time bounds are often complex and thus error-phrone. In Hume,
this contradiction is solved by a two layered architecture: a high-level fully
expressive language, is built on top of a low-level coordination language
which can guarantee space and time bounds.
This thesis explores the veri cation of Hume programs. It targets safety
properties, which are the most important type of correctness properties,
of the low-level coordination language, which is believed to be the most
error-prone. Deductive veri cation in Lamport's temporal logic of actions
(TLA) is utilised, in turn validated through algorithmic experiments. This
deductive veri cation is mechanised by rst embedding TLA in the Isabelle
theorem prover, and then embedding Hume on top of this. Veri cation of
temporal invariants is explored in this setting.
In Hume, program transformation is a key feature, often required to guarantee
space and time bounds of high-level constructs. Veri cation of transformations
is thus an integral part of this thesis. The work with both invariant
veri cation, and in particular, transformation veri cation, has pinpointed
several weaknesses of the Hume language. Motivated and in
uenced by
this, an extension to Hume, called Hierarchical Hume, is developed and
embedded in TLA. Several case studies of transformation and invariant veri
cation of Hierarchical Hume in Isabelle are conducted, and an approach
towards a calculus for transformations is examined. | en_US |
