Simulation is a favoured technique in robotics. It is, however, costly, in terms of development time, and its usability is limited by the lack of standardisation and portability of simulators. We present RoboSim, a diagrammatic tool-independent domain-specific language to model robotic platforms and their controllers. It can be regarded as a profile of UML/SysML enriched with time primitives, differential equations, and a mathematical semantics. Our previous work on RoboSim described a notation to specify control software. In this paper, we present a novel notation to describe physical models: block diagrams that can be linked to the platform-independent software model to characterise how services required by the software are realised by actuators and sensors. Behaviours are specified by differential equations, and simulations and mathematical models of the whole system can be generated automatically. Our main contributions are a modular and extensible diagrammatic notation that supports the explicit specification of physical behaviours; a set of validation rules that identify well-formed models; a model-to-model transformation from RoboSim to an input format accepted by several simulators; and a formal semantics for mathematical reasoning.

Security-critical applications often rely on memory isolation mechanisms to ensure integrity of critical data (e.g., keys) and program instructions (e.g., implementing an attestation protocol). These include software-based security microvisor S μV or hardware-based (e.g., TrustLite or SMART) techniques. Here, we must guarantee that during an execution of a program, none of the assembly-level instructions corresponding to the program violate the imposed memory access restrictions. We focus on two security architectures (S μV and TrustLite). We use Binary Analysis Platform (BAP) to generate assembly-level code in an intermediate language (BIL) for a compiled C program. This is then translated to Isabelle/HOL theories. We develop an operational semantics by defining a collection of transition rules for a subset of BIL (called AIRv2) that is sufficient for our work. We develop an adversary model and define conformance predicates for each assembly-level instruction. A conformance predicate holds iff the associated memory access restriction imposed by the underlying security architecture is satisfied. We generate a set of programs covering all possible cases in which an assembly-level instruction attempts to violate at least one of the conformance predicates. For S μV, we capture all such violations not only by checking specific lines of the program but also by applying the operational semantics for every machine-state transition. This shows that the memory access restrictions of S μV is operationally maintained. For TrustLite, we capture all such violations by checking specific lines of the program. Also, we provide an example to show how we can use the operational semantics to capture such violations.