Keywords

1 Introduction

Modern robotics simulators enable fast prototyping of robots, using a virtual simulation environment as a software creation and design tool. They provide realistic, computer gaming-style, 3-D rendering of robots and environments with physics engines to animate their movements authentically in automatically generated movies. Examples of such simulators include the Virtual Robot Experimentation Platform (V-REP) [54] and Webots [56].

One drawback of using these simulators as part of a principled development process is a lack of tool interoperability, with each simulator depending on a customised programming language or API. As a result of this, there are few possibilities for reuse of specifications and algorithms, and software development starts at a low-level with few abstractions. A notable exception to this is the Robot Modeling Language, RobotML [7], which targets the design of robotic applications, their simulation, and their deployment to multiple target execution platforms. The motivation for RobotML is to encourage a more abstract design process with explicit architectures, but there is no support for formal methods for verifying properties of these designs and architectures.

The RoboStar programme is developing a framework for modelling and simulating mobile and autonomous robots [49].Footnote 1 An early product of the research is the RoboChart language, a graphical domain-specific notation with a code generator that automatically produces mathematical models [40, 41, 48] in the notations of Communicating Sequential Processes (CSP) [52]. This enables the analysis of structural properties of RoboCharts: freedom from deadlock, livelock, and nondeterminism; it also supports the verification of more general untimed and timed properties by refinement checking [51]. RoboChart has an associated Eclipse-based development support environment, RoboTool [39], that enables graphical modelling and automatic generation of CSP scripts, and is integrates CSP’s refinement model checker FDR4 [9].

RoboCalc’s RoboSim language [4] provides a second graphical notation for developing simulations. A novel feature of RoboSim is the ability to verify simulations against their abstract RoboChart models. This ensures that the combination of models, simulations, deployed controllers, and hardware platforms refine the properties verified and validated by analysis and simulation. RoboChart and RoboSim support real time, discrete, continuous, and probabilistic properties; we consider only discrete probabilistic semantics in this paper. Our probabilistic models are essentially Markov Decision Processes (MDPs).

RoboChart and RoboSim have strong mathematical foundations, but they are also practical for industrial-strength robotic software engineering. This requires that they be attractive to practising engineers, but with additional powers to enable formal verification. The state of the art in industry is to use modelling techniques to specify the behaviours of robot controllers, but not the robotic hardware platform or the operating environment. Even at their most advanced, current industrial techniques use only simple state machines without formal semantics [3, 7, 47, 55]. Any abstract descriptions that are used guide simulation development, but without any relationship between abstract descriptions and implemented code. There is often a so-called “reality gap” between the state machine and simulation on the one hand, and the hardware platform on the other, and ad hoc adjustments must be made to get the robot working. It is for this reason that we have developed RoboChart with high-fidelity modelling capabilities, including continuous time and probabilism [41].Footnote 2 There is little motivation to keep the abstract state machine in line with these changes.

RoboChart has a probabilistic choice operator, but this cannot be supported by the translation into CSP, because the standard semantics and tools are not probabilistic. This paper presents an approach to developing a suitable imperative, reactive, probabilistic semantics for RoboChart. The method chosen to develop this semantics is the weakest completion semantics [24] approach based on Unifying Theories of Programming [31]. In this paper, we consider a semantics for the imperative action language for RoboChart. Elsewhere, we consider the use of this semantics to produce a sound translation from diagrams to mathematics, suitable for analysis by verification tools [10].

Our contribution is an explication of the weakest completion approach: a detailed analysis of this principle for developing semantics, enabling future application to RoboChart [41], a complex language with events, timed primitives, rich data types, a concurrency model based on synchronous and asynchronous communications, and shared variables. The inspiration for our work is precisely that of He, Morgan, and McIver [24]; but it is not straightforward to take their informal proof outlines and use them directly in a mechanical theorem prover: they are inspirational, but essentially informal. We present an abbreviation of our proof due to space limitations, but our proof steps are based on explicit axioms, lemmas, theorems, and inferences.

This paper has the following structure. In Sect. 2, we describe a few elements of the RoboChart language. In Sect. 3, we give an overview of Unifying Theories of Programming. In Sect. 4, we provide an interlude, where we discuss two predicate transformers: weakest preconditions and weakest prespecifications. In Sect. 5, we describe the technique of weakest completion semantics. In Sect. 6, we present a nondeterministic probabilistic programming language and its semantic domain. In Sect. 7, we describe the semantics of probabilistic choice and discuss how to combine distributions. In Sect. 8, we provide a detailed example: embedding nondeterministic choice in the probabilistic domain. In Sect. 9, we discuss related work on formalising probabilistic RoboCharts. Finally, in Sect. 10, we draw some conclusions from this research in progress and discuss future work.

2 RoboChart

We model robot controllers using RoboChart [41], a UML profile [44]. RoboChart models are Statecharts, a diagrammatic notation for defining behaviour [22]. State machines are part of the fabric of computing, recognisable in many forms (including, for example, Mealy and Moore automata [37]) and they are widely accepted in the embedded-software industry as a design notation. Statecharts [22] extend these familiar diagrams with two features: hierarchy and orthogonal regions. Hierarchy is provided by allowing states themselves to contain state machines, where control flow resides in exactly one state: the so-called OR-decomposition of behaviour; orthogonal regions provide a complementary AND-decomposition, where control-flow can simultaneously reside in one position in each orthogonal region, fully independently. This parallel decomposition can lead to a reduction in complexity (the “conjunction as composition” paradigm [63]). RoboChart inherits both features: it has hierarchical state machines (which encourage modularity and reuse) and parallelism, arising for components defined by several state machines and for composite states, including durative actions.

In RoboChart, the behaviour of a robot is characterised by a state, in which it may execute a particular operation and react to events from its environment. RoboChart includes structures for describing robotic platforms and their controllers, with CSP-style synchronous communication between controllers and asynchronous communication between controllers and their hardware. It has constructs to specify time properties: budgets and deadlines for operations and events. Here, we consider only the probabilistic aspects of RoboChart. We isolate a language subset of flat nondeterministic state machines with a probabilistic choice node.

RoboTool [39] provides a graphical editor for RoboChart models and automatically generates mathematical definitions in CSP that precisely define their behaviour. RoboTool is closely coupled with the FDR model checker [9] to analyse these definitions.

We present two RoboChart models to illustrate the language. The first model is part of the controller for a tele-operated robot used to search an arena for evidence of a harmful chemical, using the receptor density algorithm [28]. The RoboChart is depicted in Fig. 1, which is from a RoboTool session. The robot controller uses a sensor to detect changes in the chemical composition of air over time. It reacts to gas anomalies depending on their nature and composition: with a yellow or a red light, a siren, and a flag to mark the location. The hardware includes a robot body, wheels, and motor, a main processor to detect gas and accept movement commands from an operator, and a microcontroller to manage the light, siren, and flag.

Fig. 1.
figure 1

(taken from [40]).

Signalling state machine for Chemical Detector Robot

Full size image

Our second example is part of the controller for a foraging robot [57] (the corresponding RoboChart model and the results of its analysis are available online [50]).Footnote 3 The robot has an idealised randomising device with two states that are equally likely to occur; the device generates an outcome from a flip event in every time step.Footnote 4 The robot uses the device to decide whether to terminate or to continue a particular activity (here, foraging for energy). The robot may choose to ignore the outcome of the device. Finally, the robot considers only a limited number of times whether to continue foraging. We call this number N and leave it loosely defined. Our simple modelling objective is to explore different values for N that give us a high probability of terminating.

We specify the behaviour of the device as a RoboChart model in Fig. 2. One possibility in the FORAGE state is for the flip event to occur and the robot to remain in the FORAGE state; this models the robot ignoring the randomising device. The other possibility is available only if the number of choices has not been exhausted (\(flips < N\)). In this case, the robot controller proceeds to a probabilistic choice between two equally likely alternatives. One alternative is to move into the STOP state, which it signals with the stop event; the other alternative is to return to the FORAGE state, signalling this with the forage event. In both cases, the controller keeps track of the number of choices made. Note that, if in the FORAGE state \(flips < N\), then the behaviour is nondeterministic: the robot controller might take either alternative. In the STOP state, only the flip event is possible, with a self-loop acting as a sink. A well-formed MDP must be free from deadlock (every state must have at least one outgoing transition), and anyway, this transition is needed because of the requirement that flip must occur in every time step, even when the controller has terminated.

Fig. 2.
figure 2

RoboChart model of a foraging robot.

Full size image

Analysis of the generated model using Prism [35] shows that the model is deadlock free, but that the STOP state is not always possible (the minimum probability of finally reaching STOP is zero) because the model could stay in the FORAGE state forever. Additionally, using experiment for N ranging from 1 to 20, we can obtain the probability of finally reaching STOP, as shown in Fig. 3. For N \(\ge \) 6 the device will terminate with probability greater than 0.98.

Fig. 3.
figure 3

Model checking experiment for foraging robot.

Full size image

3 Unifying Theories of Programming

There are tutorial introductions to UTP’s theory of designs [59, 60], CSP [6], and the use of Galois connections to link these theories [61]. UTP embodies Hehner’s predicative semantic paradigm [25,26,27], where programs are predicates [29]: a program is identified with its meaning as a predicate, expressed pointwise. Theories describe the meaning of a computation as a relation between a before-state and an after-state, and these relations form complete lattices ordered by refinement. Several basic UTP theories are relevant to this paper.

  1. 1.

    A relational theory of a nondeterministic programming language (basically, Dijkstra’s guarded command language (GCL)) supports reasoning about partial correctness [31, Chap. 2].

  2. 2.

    A theory of designs, pre- and postcondition pairs, and an associated version of GCL supports reasoning about total correctness [31, Chap. 3].

  3. 3.

    A theory of reactive processes with communication and concurrency [31, Chap. 8].

  4. 4.

    A theory of CSP, essentially a predicative version of CSP’s failures-divergences semantics [31, Chap. 8].

  5. 5.

    Circus, a combination of CSP and Z [45, 46].

UTP has been used in a wide variety of applications, from specifying and reasoning about difficult program features [23], to specifying the semantic interfaces in a cyber-physical systems tool chain [12, 36].

A core concept is the embedding of the pre- and postconditions of designs in other semantic domains. For example, the theory of reactive designs [6] is an embedding of designs in the theory of reactive processes, which brings the familiar techniques of assertional reasoning and design calculi to reactive programming, allowing the creation of a reactive Hoare logic and a reactive weakest precondition calculus.

Unification in UTP is in three dimensions:

  1. 1.

    Programming paradigms: comparing and combining different language features in a coherent way.

  2. 2.

    Levels of abstraction: refining different design concepts.

  3. 3.

    Methods of presentation: moving between denotational, algebraic, and operational semantics.

There are four principal mechanisms for unification:

  1. 1.

    Subset embeddings, e.g., total and partial correctness (designs and relations) [58].

  2. 2.

    Weakest completion semantics, e.g., probabilistic and standard programs, as explained in Sect. 5.

  3. 3.

    Galois connections, e.g., imperative programs and reactive processes [5, 58].

  4. 4.

    Parametrised theories, e.g., reactive processes and hybrid processes [15].

We have implemented UTP in the Isabelle/HOL theorem prover [42]. The resulting proof tool is Isabelle/UTP [13, 16,17,18,19]. Our research aim is a sound automated theorem prover, built in Isabelle/UTP, for diagrammatic descriptions of reactive, timed, probabilistic controllers for robotics and autonomous systems. We note that it is not straightforward to take the informal proof outlines in [24] and use them directly in a mechanical theorem prover. In this paper, our objective is to explicate the weakest completion semantic technique and in doing so, to explore how to mechanise it.

4 Weakest Preconditions and Prespecifications

In this section, we review Dijkstra’s weakest precondition predicate transformer [8] and its generalisation, the weakest prespecification [30].

A typical stage in program development is to prove that a program meets its specification. Schematically, this is a problem in three variables: the program and its specification, which is a precondition and a postcondition. The weakest precondition calculus fixes two of these variables, the program and the postcondition, and calculates the third, the precondition, as an extreme value.

figure a

(This derivation is a small variation on that in [31, Chap. 2].) UTP’s relational calculus is alphabetised: names are an important part of the meaning. Where we think that it might help, we have emphasised which names occur in each predicate by using parameters. This also streamlines substitution.

Formally, given program and postcondition , the problem is to find the weakest precondition (in terms of and ) such that refines . refines , written , just in case , where and denote the before and after states. In UTP, universal closure over an alphabet is abbreviated by brackets, so refinement is defined as .

So the predicate is the weakest precondition for execution of to guarantee postcondition (written as ). Here, is the relational composition of and , [31, Chap. 2] defined by . Our minor generalisation accounts for its use with non-homogeneous relations later in the paper. Note that there is a modality here, between necessity and possibility. Compare the definition of weakest precondition with its dual, the conjugate weakest precondition [62]: .

figure y

During the derivation of weakest precondition, we see that . This has universal force: every final state of the program must satisfy . Its conjugate has existential force: some execution of satisfies .

Now we move on to a generalisation of weakest precondition: the weakest prespecification. First, we define relational converse . For example, the converse of an assignment is calculated as follows:

figure ag

Weakest prespecifications generalise weakest preconditions from conditions to relations: given specifications and , find the weakest specification (in terms of and ), such that is refined by . We proceed in a similar way to our previous calculation for the weakest precondition: first, isolate on the stronger side of the refinement relation, so that we can conclude we have a weakest solution; then rewrite the other side of the relation so that we can use the definition of sequential composition. Our derivation is (as far as we know) novel in the literature. There is a strong analogy between the weakest precondition and weakest prespecification predicate transformers; see Appendix A for further motivation.

figure ap

So, must be at least as strong as . We read this as “The weakest prespecification of through ”, and denote it by (the weak inverse of the function ). The weakest prespecification forms one adjoint of a Galois connection, with sequential composition as the other adjoint; that is: . We give an example of calculating a leading assignment: we want to implement the assignment as the sequential composition . That is, is the weakest prespecification of through .

figure bc

5 Weakest Completion Semantics

We now turn to weakest completion semantics [24], where we lift standard designs to probabilistic designs. Our objective is to give semantics to a nondeterministic probabilistic programming language that is consistent with a similar standard programming language: the only difference being the presence or absence of a probabilistic choice operator. Consistency is important to make sure that programming intuitions, development techniques, and proof methods can be carried over, as far as possible, from the standard language to the probabilistic one.

One way to achieve consistency is to extend the standard semantics to the probabilistic one in a controlled way. He et al.’s work [24] develops a semantic method to extend theories of programming automatically, as far as possible. Their method is to make only a few explicit assumptions and then generate a semantics by following a set of principles. They have applied their technique to two semantics for the nondeterministic programming language: a relational semantics and a predicate-transformer one.

He et al. propose the following procedure:

  1. 1.

    Start from the semantics for the nondeterministic programming language.

  2. 2.

    Propose a probabilistic semantic domain.

  3. 3.

    Propose a mapping from the probabilistic semantics to the standard semantics to relate computations of probabilistic programs to computations of standard programs.

  4. 4.

    Use this mapping to induce automatically an embedding of programs over the standard semantics: the technique is to consider the weakest completion of a sub-commuting diagram expressing refinement, rather than equality.

  5. 5.

    Determine its defining algebraic characteristics of the new language.

6 Probabilistic Programs

Our standard and our probabilistic programming languages have identical syntax, except that the latter has the addition of a probabilistic choice operator: . This is a choice between with probability , and with probability . The syntax of this language is given in

figure bi

This nondeterministic probabilistic language is a suitable target for probabilistic RoboChart [10]. The semantic domain for the language without probabilistic choice is the UTP theory of designs. This theory allows the boolean observation of a program starting ( ) and of it terminating ( ). A design with precondition and postcondition is a pair of predicates , which is defined as the single relation . This is a statement of total correctness: if the program is started in a state satisfying its precondition, then it will terminate and when it does, its postcondition will be satisfied. The vectors of variables represent the initial and final states of ordinary program variables, which are modelled as mappings from the names of program variables to their values. The UTP semantics for this nondeterministic programming language is well known [31, Chap. 3].

figure bq

Next, we consider the probabilistic semantic domain. Let the state space be . Let the set of probabilistic distributions over be the set of total functions to probabilities: . The probabilities in a discrete distribution sum to : , for .

A probabilistic design is defined as , where the alphabet of is and the alphabet of is , for \(s \in S\) and .

The relationship between standard and probabilistic programs is most easily understood as an abstraction from the probabilistic semantic domain: a mapping that forgets the probabilities and replaces them by possibilities. We define as a design with a non-homogeneous alphabet: , where and design observations about initiation and termination, is a discrete probability distribution, and .

figure cl

This non-homogeneous design is a forgetful function: the probability of arriving in state is ; this is replaced by the possibility of arriving in that state: .

Note now that is a standard design if is a probabilistic design.

Using this idea, for probabilistic design and standard design , we construct the following sub-commuting diagram

figure ct

where . This is an inequality in three variables, two of which we already know: and . So, we calculate using the weakest prespecification of wrt . The result is the weakest probabilistic design related to the standard design . We introduce the following definition: for any standard design , define as its embedding in the probabilistic world.

We need to prove that this embedding really does produce probabilistic designs, which we do in the following theorem. For any subset of , define , for any probability distribution function . Furthermore, for any relation with alphabet (both in ), define .Footnote 5 If and are disjoint sets then

figure dy

A corollary is that

figure dz

Theorem 1

(Embedded standard designs are probabilistic designs).

figure ea

Proof

Start by simplifying the definition of by pushing the weakest prespecification operator into the postcondition. Note that the law we use requires that the design is \(\mathbf {H3}\) healthy [31, Chap. 3]: its precondition must not mention any variables from the after-state.Footnote 6 This assumption is discharged here. Our account of this law is novel, but we do not present it in this paper.

figure eg

Now show that

figure ei

Our next task is to prove that the embedding is a homomorphism on the structure of standard programs. As a result, most of the algebraic laws that hold in the standard semantic framework remain valid in the probabilistic model. We give two example cases in the proof of the homomorphism: the embedding of assignment (here) and nondeterminism (in Sect. 8).

Lemma 1

(Embedded assignment).

figure ej

Proof

figure ek

In the next section, we consider how to combine probability distributions in order to support probabilistic and nondeterministic choice operators.

7 Probabilistic Choice and Combining Distributions

We start with a motivating example of combining probability distributions: expressing multiway probabilistic choice as a combination of binary probabilistic choices. This leads us to propose a semantics for probabilistic choice in the spirit of UTP’s parallel-by-merge operator. We consider how to decompose a probability distribution into two distributions combined by probabilistic choice. This leads to two projection functions, one for each operand. We conclude the section with three lemmas that will be used in the case for nondeterministic choice in the proof of being a homomorphism. These lemmas provide witnesses for the decomposition required.

Consider a multiway probabilistic choice, as found in the Reactive Modules formalism, [1] used by the probabilistic model checker Prism [35]:

figure em

Here, each assignment is labelled by a probability and these probabilities sum to . How can we express this using binary probabilistic choice? One simple solution uses two operators:

figure eo

To show that this is a solution, note that the assignment is chosen with probability ; is chosen with probability ; and must be chosen with the remaining probability, which is . A slightly more complicated solution uses three operators:

figure ev

Analysing probabilities once more gives us for ; for ; and for . Simple arithmetic proves that we got this right.

These examples show how distributions are combined as we move the binary operator to its multi-way cousin. In the first example, we are combining the following two distributions:Footnote 7

figure fe

and we are combining them in the ratio given by the outermost choice operator: :

figure fg

To formalise this, define the merge of two distributions, and , to form distribution as: , for some probability ratio r. We use this in the definition of an operator inspired by UTP’s parallel-by-merge [31, Chap. 7] to combine the probability distributions described by two postconditions:

figure fl

This operator may be applied equally well to a design, rather than an individual postcondition, without any confusion.

With this operator, we now have a semantics for probabilistic choice:

figure fm

The meaning of probabilistic choice is clearly compositional: if we have the meaning of and , then we can find the meaning of . But we can also think about the decomposition of a probabilistic program into the probabilistic choice between two subprograms. Suppose that we have two sets of states and , such that and a probabilistic ratio (to ensure and are well defined).Footnote 8 In this case we can unravel the merge of two distributions if and . To do this, we define the projections.Footnote 9

figure gj

For to be a distribution, we need its domain to sum to unity; that is, . These projections satisfy our merge predicate, and in that sense provide a joint witness.

Lemma 2

(Merge witnesses). For , , and ,

figure gp

Proof

figure gq

Now we state two lemmas that ensure that our two projections are probability distributions that sum to unity.

Lemma 3

(Total witness 1). Let and ; then

figure gt

Proof

figure gu

Lemma 4

(Total witness 2). Let and ; then

figure gx

Proof

Similar to Lemma 3.

The main result that we want to present in this paper is stated and proved in the next section.

8 Nondeterministic Choice

In this section, we prove the case for nondeterministic choice in the homomorphism theorem. Nondeterministic choice can be used in the top-down development of a program to abstract from detail, including specific details of a probabilistic choice. So should distribute through nondeterministic choice in the following way:

figure gz

Refinement to a particular probabilistic choice would then follow by strengthening the result, choosing for . In this section, we prove one half of this result, omitting the other half only because we lack space.

The next lemma simplifies the embedding of nondeterministic choice.

Lemma 5

(Embedded nondeterministic choice).

figure hd

Proof

figure he

Now we show half of our result: that the embedding is a weakening homomorphism for nondeterministic choice. This means that as distributes through nondeterminism, it produces a weaker predicate.

Theorem 2

(Nondeterminism embedding weakening).

figure hg

Proof

figure hh

We omit the (easier) proof that the embedding is a strengthening homomorphism for nondeterministic choice: as distributes through nondeterminism we obtain a stronger predicate.

This concludes our presentation of the semantics for the nondeterministic probabilistic programming language that serves as the textual version of RoboChart diagrams with discrete probabilistic behaviour. We have described the semantic domain and an embedding function from standard programs to probabilistic ones. We have shown just two cases for the proof that the embedding is a homomorphism. This has guided the definition of individual program operators. For example, we have

figure hj

This definition is supported by Theorem 2 and a matching proof for the strengthening homomorphism (omitted in this paper). The proof identified the need for the two special cases in the semantics of nondeterminism: and .

9 Related Work

Jansen et al. propose a probabilistic extension to UML [33, 34]. They add to UML’s basic Statecharts a probabilistic choice node whose out-edges are annotated with probabilities. They identify interferences between Statechart transition priorities and the order of resolving nondeterministic and probabilistic choice. Verification is performed using the Prism probabilistic model checker, with the probabilistic logic PCTL specifying properties over Statecharts. They describe the operational semantics of step execution. This is then embedded in a finite Markov Decision Process specified as a probabilistic Kripke system.

Nokovic and Sekerinski [43] propose pCharts, another variation on Statecharts, but extended with timed transitions, probabilistic transitions, costs and rewards, and state invariants. They present a translation scheme from untimed pCharts to Markov Decision Processes (MDPs), from timed pCharts to probabilistic timed automata (PTA), and from pCharts to executable C code. Everything is implemented in the pState tool. MDPs are used to verify probabilistic and nondeterministic behaviour. PTAs are used to verify additional real-time constraints, such as the maximum or minimum probability of reaching a state within a given time and the maximum expected time to reach that state (its deadline). pCharts can be augmented with quantitative information for costs and rewards for both transitions and states: priced PTAs. This permits analysis of the maximum or minimum expected time before a transition takes place, or the number of expected steps to reach a particular state. Translation rules deal with hierarchy and orthogonality.

Both Jansen’s and Nokovic’s work is similar to He et al.’s [24], and therefore ours, in constructing a conservative extension of standard Statecharts. Both of them go further in dealing with hierarchy and orthogonality. This differs from our work in several ways. We focus on producing a semantics that can be combined with other UTP theories. Both Jansen and Nokovic focus on model checking, and therefore have a closed-world assumption and restrict variables to bound integers. We are interested in both model checking and theorem proving.

In 2004, Goldsmith reported an experiment [20] to extend the input language for FDR2 to accept a probabilistic choice construct with added functionality, to produce models suitable for analysis by Prism [35]. Goldsmith describes some encouraging results, but also warns about various drawbacks in the work: the loss of regularity in code emitted from FDR2 that would lead to Prism exploiting symmetries in its model checking; and that the transformation scheme does not support CSP’s full failures-divergences model. The probabilistic functionality in FDR2 was lost when development moved to FDR3 in 2012 and remained lost with the move to FDR4 in 2017.

Mota et al. [10] rediscovered the functionality in FDR2 (as well as legacy copies of the tool) in their work on analysing probability in RoboChart. They define the semantics of the RoboChart probabilistic choice operator in terms of CSP’s probabilistic operator. They show how this augmented CSP semantics for RoboChart can be translated into the Prism’s Reactive Modules input language to check stochastic properties of RoboChart.

Zhao et al. [65] describe mapping rules between UML state diagrams and probabilistic Kripke structure semantics. They present an asynchronous parallel language based on discrete time Markov chains. Non-functional properties of systems specified using PCTL, with verification provided by the Prism model checker. Interactive theorem proving is also supported and linked to experimental results. Interestingly, the mapping rules are provided as a bidirectional transformation.

Zhang et al. [64] address the formal verification of dynamic behaviour of UML diagrams. They automatically verify UML state machine models by translating UML models to the input language of the PAT model checker in such a way as to be transparent for users. They can check safety and liveness properties with fairness assumptions using the PAT model checker [38].

10 Conclusions and Future Work

We have presented an overview of our ongoing work in giving a probabilistic semantics to RoboChart. We have concentrated on the imperative, sequential action language for RoboChart, using the weakest completion semantics approach. The result is a programming theory that can now be combined with other programming paradigms, using UTP’s unification techniques explained in Sect. 3. The next step for us is to lift the current semantics into UTP’s reactive theory to produce a theory of reactive probabilistic designs.

We have explicated the weakest completion approach, showing how proof outlines in [24] can be turned into near formal proofs suitable for implementation in a theorem prover. In doing this, we spent a surprising amount of time understanding the structure of He et al.’s proof, especially the nondeterminism case for the proof that the embedding function is a homomorphism. This led us to investigate the weakest prespecification operator for the design theory in some detail, coming up with what we believe to be a novel derivation of the operator that echoes Hoare and He’s derivation of the weakest precondition operator [31]. We observe that a law quoted in the proof of this case in [24] requires a side condition that the design to which it is applied satisfies the healthiness condition [31, Chap. 3]. This is the case in the proof where it is used, but it does raise an interesting question for our lifting the current semantics to the reactive world. We found a small number of inconsistencies in the proof outlines, but these have not affected the validity of the lemmas and theorems in [24].

Our future work consists of the following:

  1. 1.

    Complete the rest of the proof that is a homomorphism (essentially, the Kleisli lifting needed for sequential composition).

  2. 2.

    Implement our proofs in the Isabelle/UTP theorem prover [19].Footnote 10

  3. 3.

    Lift the semantics to the reactive theory.

  4. 4.

    Use our semantics to verify the soundness of a translation from RoboChart to Reactive Modules, so that Prism can be used to analyse probabilistic RoboCharts.

  5. 5.

    Tackle a range of different examples using both model checking and theorem proving to challenge our work. We have in our sights various probabilistic robotic control algorithms.

Examples include verifying robot localisation algorithms, such as the Random Sample Consensus algorithm Ransac that is frequently used in robotic control [11]; providing bounds for the battery life required for coverage using random walks and arena-mapping techniques by autonomous robotic cleaners and searchers; and verifying learning algorithms for robots in uncertain environments.