Model-based Software Engineering for Robotics
Abstract
Robots are anticipated to play important roles in supporting human activities across several sectors of societal importance. Current software development practices, however, are not adequate to ensure they operate safely. Model-based software engineering techniques underpinned by mathematics and supported by state-of-the-art reasoning tools, on the other hand, can be exploited for the design of trustworthy robotics software. In this series of lectures, we will learn about modelling and verification of robotic software controllers using a model-based approach anchored in sound mathematical theories.
Preparation Material for the Course
Introductory material about RoboStar, the suite used in the course, is available here. Attendees are invited to read it before the course, so to have it ready for its use during the lectures.
Practical Material
References for practical material used in the course can be found on this RoboStar page.
Course Content
Session 1 - RoboStar technology
Software Engineering for Robotics
This lecture will introduce the RoboStar suite of modelling notations, namely, RoboChart and RoboSim, for designing the software of mobile and autonomous robots. Topics covered include:
- Motivation and state of practice
- Robotic software controllers
- RoboChart and RoboSim: core language concepts
Case study: firefighting drone
In this session, we will introduce a running example of a firefighting drone and consider the development of a safety function informed from hazard analysis. Topics covered include:
- Case study motivation
- Safety issues
- Hazard analysis
- Safety function
Session 2 - RoboSim: core concepts
RoboSim: a modelling language for simulation
The RoboSim notation will be introduced in more detail in this session. Topics covered include:
- Cyclic paradigm: key concepts and assumptions
- RoboSim: core language, states, transitions and operations
Practical: Modelling the safety state machine
In this interactive session, students will be expected to design a state machine for a software component of the Firefighting UAV using RoboTool, an Eclipse-based environment for constructing RoboSim models with support for validation and formal verification. Topics covered include:
- Case-study revisited: modelling of the safety function
Session 3 - Foundations
Practical: modelling of firefighting drone software component (continued)
We will continue with modelling the firefighting drone software component.
Formal foundations of simulation software
In this lecture, we will study the formal semantics underpinning the RoboSim notation, given in tock-CSP, a discrete-timed version of the process algebra of Communicating Sequential Processes (CSP). Topics covered include:
- tock-CSP model and core operators: budgets and deadlines, and refinement
- Semantics of RoboSim
Session 4 - Verification
From foundations to verification and automated test-generation
In this session, we will discuss how the formal semantics of RoboStar notations can be used to verify properties and derive test specifications. Topics covered:
- Verification of basic properties
- Formal testing specifications
- Model-based testing: mutation testing and exhaustive approaches
Practical: Automatic verification and test-generation
In this session, students will be expected to use their model from Session 2, or a sample solution, to perform formal verification, using RoboTool and FDR, and derive test specifications that could be leveraged in testing, for example, of a ROS implementation.