vTSL - A Formally Verifiable DSL for Specifying Robot Tasks

Christian Heinzemann; Ralph Lange

IROS 2018poster19 citations

vTSL - A Formally Verifiable DSL for Specifying Robot Tasks

Abstract

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.

BibTeX

@inproceedings{iros2018_vtslaformallyver,
  title = {vTSL - A Formally Verifiable DSL for Specifying Robot Tasks},
  author = {Christian Heinzemann and Ralph Lange},
  booktitle = {IROS 2018},
  year = {2018}
}