Design, formalization and realization of harmonic box coordination language : an externally timed specification substrate for arbitrarily reliable distributed systems

• Main Author: George, Samuel R. J.
• Published: University of Bristol 2014
• Subjects: 005.3
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.681554

The functional specifications of high integrity systems include details needed to harden them against hardware and implementation failures, leading to a lack of design transparency, duplicative certification exercises and implementation inflexibility. This thesis develops a new ontology-driven meta-model for specifying such systems, in which the language itself is instantiated over a canonical coordinate system in spacetime. We define a system of localized timed types, denoted by a canonical tree of identifiers, and a dense model of time, which we call Pre-HBcL (Pre-Harmonic Box Coordination Language), for which we give a deep embedding in the Coq proof assistant. We go on to develop a full coordination programming language of harmonic boxes (full HBCL), defined over these types; the language is parametrized on arbitrary inner box languages, and we provide a simple example that gives rise to a hardware description language. We give a full semantics at progressive levels of formality. We argue that the decoupling of a light-weight ontology from formalizing logic language produces a more flexible approach than can be achieved with monolithic specification languages, allowing bisimulation properties to be established between HBCL programs and more directly physical axiomatizations of hardware. We demonstrate how the use of a reflexive morphism in HBCL simplifies the establishment of timing properties and composition of specifications. We develop an interpreter exported from a proof assistant. In doing so, we demonstrate an unusually easy route to establishing soundness of our language up to the soundness of the formalizing logic, and discuss the completeness limitations. To this end, we review issues in computability, and construct a comparison in which formal logics are included in the same schema as coordination and specification languages. We conclude with an empirical demonstration of properties derived from the interpreter, and evaluate the extent to which the work substantiates our conjectures.