In the design of robotic systems, often, state machines are drawn to convey
overall ideas; they are used as a basis to program tool-specific
simulations. The simulation code, written in general or proprietary
programming languages, is, however, the only early account of the robotic
system. We present a modern approach to design that supports automatic
generation of simulation code that is guaranteed to be correct, and
complements the use of simulation with model checking, theorem proving, and
systematic testing. This approach, under development by the RoboStar group
(https://www.cs.york.ac.uk/robostar/), uses two domain-specific languages
supported by a tool. RoboChart is an event-based notation for
design; RoboSim  is a matching cycle-based diagrammatic notation for
simulation. Using RoboTool, we can create RoboChart and RoboSim models, and
generate mathematical models and tests automatically.
About Ana Cavalcanti
Ana Cavalcanti is a Professor at the University of York, UK, and a Royal
Academy of Engineering Chair in Emerging Technologies. Her current work is
on Software Engineering for Robotics, with a leading role in the RoboStar
group (https://www.cs.york.ac.uk/robostar/). From 2012 to 2017, she held a
Royal Society - Wolfson Research Merit Award. In 2003, she was awarded a
Royal Society Industry Fellowship to work with QinetiQ on formal methods.
She has published more than 150 papers, and chaired the Programme Committee
of various well-established international conferences. She has a long-term
interest in refinement, safety-critical systems, object-orientation,
concurrency, and real-time applications. Her work has concentrated on the
development of mathematical techniques to support rigorous Software
Engineering using approaches of industrial relevance.
She has played a major role in the design and formalisation of a
state-rich process algebra, namely, Circus, and its development techniques
using the Hoare and He’s Unifying Theories of Programming. She is currently
Chair of the Formal Methods Europe association.