PsALM: specification of dependable robotic missions

Engineering dependable software for mobile robots is becoming increasingly important. A core asset to engineering mobile robots is the mission specification – a description of the mission that mobile robots shall achieve. Mission specifications are used, among others, to synthesize, verify, simulate or guide the engineering of robot software. However, development of precise mission specifications is challenging, as engineers need to translate requirements into specification structures often ex- pressed in a logical language – a laborious and error-prone task. Specification patterns, as solutions for recurrent specification problems have been recognized as a solution for this problem. Each pattern details the usage intent, known uses, relationships to other patterns, and—most importantly—a template mission specification in temporal logic. Patterns constitute reusable build- ing blocks that can be used by engineers to create complex mission specifications while reducing mistakes. To this end, we describe PsALM, a toolchain supporting the development of dependable robotic missions. PsALM supports the description of mission requirements through specification patterns and allows automatic generation of mission specifications. PsALM produces specifications expressed in LTL and CTL temporal logics to be used by planners, simulators and model checkers, supporting systematic mission design.