Reference : PsALM: specification of dependable robotic missions
Scientific congresses, symposiums and conference proceedings : Paper published in a book
Engineering, computing & technology : Computer science
Security, Reliability and Trust
PsALM: specification of dependable robotic missions
Menghi, Claudio mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Tsigkanos, Christos [TU Wien, Vienna, Austria]
Berger, Thorsten [Chalmers & University of Gothenburg, Gothenburg, Sweden]
Pelliccione, Patrizio [Chalmers & University of Gothenburg, Gothenburg, Sweden and University of L'Aquila, L'Aquila, Italy]
Proceedings of the 41st International Conference on Software Engineering: Companion Proceedings
International Conference on Software Engineering
from 25-05-2019 to 31-05-2019
[en] Robotic ; Patterns ; Mission
[en] 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.
H2020 ; 694277 - TUNE - Testing the Untestable: Model Testing of Complex Software-Intensive Systems

File(s) associated to this reference

Fulltext file(s):

Open access
psalm.pdfAuthor postprint732.64 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.