How can we provide guarantees of behaviours for autonomous systems such
as driverless cars? This tutorial text, for professionals, researchers
and graduate students, explains how autonomous systems, from intelligent
robots to driverless cars, can be programmed in ways that make them
amenable to formal verification. The authors review specific
definitions, applications and the unique future potential of autonomous
systems, along with their impact on safer decisions and ethical
behaviour. Topics discussed include the use of rational cognitive agent
programming from the Beliefs-Desires-Intentions paradigm to control
autonomous systems and the role model-checking in verifying the
properties of this decision-making component. Several case studies
concerning both the verification of autonomous systems and extensions to
the framework beyond the model-checking of agent decision-makers are
included, along with complete tutorials for the use of the
freely-available verifiable cognitive agent toolkit Gwendolen, written
in Java.