|
Motlatsi Seotsanyana
|
Researcher develops a runtime verifier to enhance robotics safety
Autonomous robotic systems are increasingly ubiquitous in everyday life and this has led to a need to develop safe and reliable systems. If a system is to operate autonomously, its safe operation becomes critical and hence developing runtime verification algorithms can be important in ensuring safe and reliable interaction of these systems with human beings. Most software and hardware failures are a consequence of erroneous system behaviour arising from faults in these systems.
CSIR Mobile intelligent autonomous systems (MIAS) researcher, Motlatsi Seotsanyana, is doing work on formal methods in robotics to make sure that, scientists and engineers design and implement safe and reliable autonomous systems. “Formal methods refer to the use of mathematical techniques for the specification, development and verification of software and hardware systems,” he explains.
The traditional verification techniques such as testing, simulation, model checking and theorem proofing often do not scale up well to large systems such as robotic systems, which are inherently characterised by uncertainties due to heavy reliance on sensor data, dynamic environments and changes over time. These conditions make it hard to predict and verify these systems prior to their execution. “Therefore, stochastic runtime verification is an appropriate technique to complement traditional verification techniques,” he remarks.
The stochastic runtime verification refers to the use of probabilistic techniques to check whether an autonomous system under scrutiny satisfies or violates the set of given probabilistic constraints.
The main aim of Seotsanyana’s research is to develop an intelligent stochastic runtime verifier which is able to learn the behaviour of systems under scrutiny and react accordingly if any undesired behaviour is detected. The verifier deals among others with the following sources of faults in the system: incomplete sensing; faulty sensing; wear and tear of hardware; dynamic environment; third party software libraries that may have subtle errors; etc. These sources of errors are detected by: first, specifying the desired behaviour of the system in a stochastic linear temporal logic; second, training the verifier with this correct or desired behaviour through data mining techniques; and lastly, verifying the behaviour of the system against probabilistic requirements at runtime and reacting accordingly during the system execution. That is, put the system in a safe state if any undesired catastrophic behaviour is detected.
This – according to Seotsanyana – is a new concept in robotics. “Researchers worldwide are conducting studies on formal methods mostly on path planning and control not on runtime verification of autonomous systems,” he says, adding, “At least that is what the literature suggests.” His work on formal methods in robotics has produced a journal paper titled Temporal Logic in Motion Planning in Defence Science Journal and a book chapter, titled, Temporal Logic in Robotics in the book, Mobile Intelligent Autonomous Systems published by CRC Press.
The man…
Seotsanyana hails from the Mountain Kingdom of Lesotho. He received his undergraduate degree in computer science and statistics at the National University of Lesotho in 1999. After graduating, he worked at the same university as an assistant lecturer. In 2004, he came to South Africa to pursue his Honours degree in the same discipline at the University of the Witwatersrand and graduated a year later. In 2006, he headed to the University of Stellenbosch where he studied his Master’s in computer science and graduated the following year. In 2008, he rejoined the National University of Lesotho as a lecturer in the Department of Mathematics and Computer Science. He then came to South Africa and joined the CSIR MIAS as a researcher. He is currently pursuing a PhD part-time in field robotics, through the University of Sydney in Australia.
|
