ABSTRACT. The calculus formalises human intuition and common sense about space, time and causality in the natural world. Its intention is to assist in the design and implementation of programs, of programming languages, and of interworking by tool chains that support rational pro- gram development. The theses of this paper are that Concurrent Kleene Algebra is the algebra of programming, that the diagrams of the Unified Modelling Language provide its geometry, and that Unifying Theories of Programming provides its logic. These theses are illustrated by a formalisation of features of the first concurrent object-oriented language, Simula 67. Each level of the calculus is a conservative extension of its predecessor.

ABSTRACT. In this paper, we discuss the role of formal semantics from a testing perspective. Our focus is on conformance testing, where we test if a given system-under-test conforms to an abstract description of its intended behaviour. We show how the main semantic paradigms, namely algebraic, denotational, and operational semantics, support a systematic testing process and give examples from our own work on automated test-case generation.

ABSTRACT. Unifying theories distil common features of programming languages and design methods by means of algebraic operators and their laws. Several practical concerns---e.g., improvement of a program, conformance of code with design, correctness with respect to specified requirements---are subsumed by the powerful notion that programs and designs are special forms of specification and their relationships are instances of logical implication between specifications. Mathematical development of this idea has been very successful but limited to an impoverished notion of specification: trace properties. However, some mathematically precise properties of programs---dubbed hyperproperties---refer to collections of traces, e.g., confidentiality involves knowledge of possible traces. This note reports on both obvious and surprising results about lifting algebras of programming to hyperproperties, suggesting directions for further research.

ABSTRACT. We study the semantics of recursion for computations that make strict progress. The underlying unified computation model has an abstract notion of progress, which instantiates in ways such as longer traces, passing of real time, or counting the number of steps. Recursion is given by least fixpoints in a unified approximation order. Other time-based models define the semantics of recursion by greatest fixpoints in the implication order. We give sufficient criteria for when least fixpoints in the approximation order coincide with greatest fixpoints in the implication order.

ABSTRACT. We outline a probabilistic denotational semantics for the RoboChart language, a diagrammatic, domain-specific notation for de- scribing robotic controllers with their hardware platforms and operating environments. We do this using a powerful (but perhaps not so well known) semantic technique: He, Morgan, and McIver’s weakest completion semantics, which is based on Hoare and He’s Unifying Theories of Programming. In this approach, we do the following: (1) start with the standard semantics for a nondeterministic programming language; (2) propose a new probabilistic semantic domain; (3) propose a forgetful function from the probabilistic semantic domain to the standard semantic domain; (4) use the converse of the forgetful function to embed the standard semantic domain in the probabilistic semantic domain; (5) demonstrate that this embedding preserves program structure; (6) define the probabilistic choice operator. As pointed out by its inventors, weakest completion semantics guides the semantic definition of new languages by building on existing semantics. In this case, this semantic method guides the development of the semantics of probabilistic choice and directly tackles a notoriously thorny issue: the relationship between demonic and probabilistic choice. As He et al. note: choosing the right semantic extension can be a lucky guess: here is a principle that reduces guesswork. Consistency ensures that programming intuitions, development techniques, and proof methods can be carried over from the standard language to the probabilistic one. We largely follow He et al., our contribution being an explication of the technique with meticulous proofs suitable for mechanisation in Isabelle/UTP.

ABSTRACT. We describe our UTP theory of hybrid relations, which extends the relational calculus with continuous variables and differential equations. This enables the use of UTP in modelling and verification of hybrid systems, supported by our mechanisation in Isabelle/UTP. The hybrid relational calculus is built upon the same foundation as the UTP's theory of reactive processes, which is accomplished through a generalised trace algebra and a model of piecewise-continuous functions. From this foundation, we give semantics to hybrid programs, including ordinary differential equations and preemption, and show how the theory can be used to reason about sequential hybrid systems.

ABSTRACT. The efficient design of safety-critical embedded systems involves at least the three modeling aspects common to cyber-physical systems (CPSs): functionality, physics and architecture. Existing modelling formalisms cannot provide strong support to take all of these three dimensions into account uniformly, e.g., AADL is a precise formalism for modelling architecture and prototyping hardware platforms, but it is weak on modelling physical and software behaviors and their interaction. By contrast, Simulink/Stateflow is strong on modelling physical and software behavior and their interaction, but weak on modelling architecture and hardware platforms. To address this issue, we consider the combination of AADL and Simulink/Stateflow, two widely used graphical modelling formalisms for CPS design in industry. This combination provides a unified graphical co-modelling formalism supporting the design of CPSs from all three perspectives uniformly. This paper focuses on the required concepts to combine them together, and outlines how to verify and simulate a system model defined by the combined graphical views of its constituents, by considering the case study of an Isollete System.

ABSTRACT. Algebras have always played a critical role in Unifying Theories of Programming, especially in their role in providing the ``laws'' of programming. The algebraic laws form a triad with two other forms, namely operational and denotational semantics. In this paper we demonstrate that algebras are not just for providing external laws for reasoning about programs. In addition, they can be very beneficial for assisting in the development of theoretical models, most notably denotational semantics. We refer to the algebras used to develop a denotational model as ``inner algebras'', while the resulting algebraic semantics we consider to be an ``outer algebra''. In this paper we present a number of inner algebras that arose in the development of a fully compositional denotational semantics, called UTCP, for shared-state concurrency. We explore how these algebras helped to develop (and debug!) the theory, and discuss how they may assist in the ultimate aim of exposing the outer algebra of UTCP, which we expect to be very similar to Concurrent Kleene Algebra.

ABSTRACT. An algebra for rely/guarantee concurrency has been constructed via a hierarchy of theories starting from basic theories like lattices through to theories of synchronous behaviour of atomic steps and a theory to support localisation. The algebra is supported by a model based on Aczel traces. We examine the role of these theories in developing a theory for deriving concurrent programs and outline some of the challenges remaining.

ABSTRACT. The mCWQ calculus was recently proposed for describing the features of broadcast and mobility in Mobile Ad Hoc Networks (MANETs), especially forcusing on the quality of wireless communications. In this paper, we investigate the denotational semantics for mCWQ calculus, whose behaviour is composed of the behaviours of subnetworks. A trace variable tr is introduced to record the communications among wireless nodes as well as the time point when the communication happens. A set of algebraic laws, especially the laws about the communications with quality binders, are also explored based on the formalized model.