vTSL - A Formally Verifiable DSL for Specifying Robot Tasks
Christian Heinzemann, Ralph Lange · 2018
Preprogramming of tasks still plays an important role in complex robotic systems despite the advances in automated planning and symbolic learning. Often, it is desired that end-users implement further tasks to adapt the robotic application to their needs. These user-defined tasks have to meet safety and integrity constraints for protecting the robotic platform and its users. We introduce a verifiable task specification language (vTSL) that enables to automatically prove that a task specification satisfies a set of predefined or task-specific constraints. We illustrate our approach using an example of a self-driving vehicle for intra-logistics and report experiences with two commercial applications.