| Conference: | Verification Futures 2019 (click here to see full programme) |
| Speaker: | Jim Woodcock, University of York |
| Presentation Title: | RoboChart and RoboSim: Verified Simulation for Robotics |
| Abstract: | Simulation is a favoured technique for analysis of robotic systems. The state of the art is for simulations to be programmed in an ad hoc way for specific simulators, using either proprietary languages or general languages like C or C++. Even when a higher-level language is used, a clear relation between the simulation and a design model is rarely established.
We present a tool-independent notation called RoboSim, designed specifically for modelling of (verified) simulations. We also show how we can use RoboSim models to check if a simulation is consistent with a functional design written in RoboChart, a UML-like notation akin to those often used by practitioners on an informal basis. We show how to check whether the design enables a feasible scheduling of behaviours in cycles as needed for a simulation, and formalise implicit assumptions routinely made when programming simulations. Our results enable the description of simulations using tool-independent diagrammatic models amenable to verification and automatic generation of code. |
| Speaker Bio: | Jim Woodcock is Professor of Software Engineering in the Department of Computer Science at the University of York, with research interests in the verification and correctness of computer-based systems. He was previously Professor of Software Engineering at the University of Oxford, where he worked on a project funded by IBM on formalising the CICS transaction processing system, under the supervision of Ib Holm Sorensen and Sir Tony Hoare FRS.
The project won the 1992 Queen’s Award for Technological Achievement for its work on formal methods. He worked on proving security properties about the Mondex smart-card electronic cash system, allowing it to be the first product to achieve ITSEC level E6, the highest granted security-level classification. He was head of the Department of Computer Science at York between 2012 and 2016. He is a member of York’s RoboStar* Research Group, one of the largest research groups in the world in software engineering of robotics. He is a Chartered Engineer, a Fellow of the Royal Academy of Engineering, a Fellow of the British Computer Society, and a member of the London Mathematical Society. He is a Grundfos Foundation Professor at Aarhus University and a Distinguished Research Professor at Southwest University in China. |
| Slides |
