The RoboStar frameworkFootnote 1 supports model-based engineering of robotic applications. Modelling is carried out using diagrammatic domain-specific languages: RoboChart [13] and RoboSim [3]. Verification and generation of artefacts is justified by a formal semantics given using a state-rich hybrid version of a process algebra for refinement [7]. It is inspired by CSP [19] and cast in Hoare and He’s Unifying Theories of Programming (UTP) [10] formalised in Isabelle [6].

RoboChart is an event-based language for design, while RoboSim is a cycle-based language for simulation. Tool support is provided by RoboTool, which includes facilities for graphical modelling, validation, and automatic generation of CSP (for analysis with the model checker FDR [9]) and PRISM [11] scripts (for verification of probabilistic controllers), and simulations. RoboChart and RoboSim are based on the use of state machines to specify behaviour, akin to notations already in widespread use [2, 5, 16, 20], but RoboChart and RoboSim are enriched with facilities for verification and traceability of artefacts.

Recent work has focussed on enriching RoboSim for physical modelling. Current practice in robotics often uses simulation to understand the behaviour of a robotic controller for a particular robotic platform and environment. A wide variety of simulators for robotics use different tool-dependent or even proprietary programming languages and API [8, 12, 14, 17, 18]. Physical modelling of the platforms are encoded by programs in customised notations, generated from graphical tools, or in C++, Java, Python, or C#, for example.

RoboSim, on the other hand, is a tool-independent notation. For physical modelling, we have defined a notation based on SysML block diagrams [15]. Our profile is inspired by XML-based notations used by robotics simulatorsFootnote 2. It defines a physical model by a diagram that captures the physical components of a platform as links (rigid bodies), joints, sensors, and actuators. Properties of these blocks capture their attributes that are relevant for simulation and for capturing behaviour: movement and use of sensors and actuators.

In contrast with XML-based notations in current use, RoboSim block diagrams encourage readability and support modularisation via several mechanisms. Models can be parametrised by constants that represent, for example, key measures of physical bodies. The pose of an element is defined always in reference to the element that contains it. A richer notion of connection captures flexible and fixed compositions. A library fosters reuse by the possibility of defining parts and fragments that can be instantiated or simply included to define a complete model. Finally, well-formedness rules ensure validity of models.

The most distinctive feature of RoboSim block diagrams, however, is the possibility of defining systems of differential algebraic equations that capture behaviour of the platform. For sensors, these equations define how inputs (from the environment) are reflected in sensor outputs for use with the software. For actuators, the equations define how inputs from the software affect the outputs of the actuators, and therefore, affect the platform itself (in the case of motors, for example), or the environment. For joints, the equations define how their movement induces movement on the links connected to them.

A system view is provided by connecting a RoboSim block diagram that specifies a physical model for a robotic platform, to a RoboSim module that specifies a control software. This is achieved by a platform mapping, which specifies how software elements that abstract services of the platform are defined. In specifying these services, we can use outputs of sensors and inputs of actuators.

Ongoing work, provides support to translate RoboSim block diagrams to XML for use in simulation (using Coppelia, formerly, v-rep). For mathematical modelling, the UTP semantics constructs a hybrid model, with constructs inspired by those of  [4], combining Z [1, 21] and CSP.