Blogs (1) >>
ICSE 2019
Sat 25 - Fri 31 May 2019 Montreal, QC, Canada
Fri 31 May 2019 14:00 - 14:20 at Van-Horne - Specifications and Models Chair(s): Sylvain Hallé

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, the development of precise mission specifications is challenging, as engineers need to translate requirements into specification structures often expressed 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 building blocks that can be used by engineers to create complex mission specifications while reducing mistakes. To this end, we describe PsALM, a toolchain supporting development of dependable robotic missions through patterns. 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.

Fri 31 May
Times are displayed in time zone: Eastern Time (US & Canada) change

14:00 - 15:30: Specifications and ModelsPapers / Demonstrations / Technical Track at Van-Horne
Chair(s): Sylvain HalléUniversité du Québec à Chicoutimi, Canada
14:00 - 14:20
PsALM: Specification of Dependable Robotic MissionsDemos
Claudio MenghiUniversity of Luxembourg, SnT, Christos TsigkanosTechnische Universität Wien, Thorsten BergerChalmers University of Technology, Sweden / University of Gothenburg, Sweden, Patrizio PelliccioneChalmers | University of Gothenburg and University of L'Aquila
14:20 - 14:40
Symbolic Repairs for GR(1) SpecificationsArtifacts Evaluated ReusableTechnical Track
Technical Track
Shahar MaozTel Aviv University, Jan Oliver RingertTel Aviv University, Rafi ShalomTel Aviv University
14:40 - 15:00
ARepair: A Repair Framework for AlloyDemos
Kaiyuan WangGoogle, Inc., Allison SullivanNorth Carolina Agriculture and Technical State University, Sarfraz KhurshidUniversity of Texas at Austin
15:00 - 15:20
Visual Debugging of Behavioural ModelsDemos
Gianluca BarbonUniversité Grenoble Alpes, Inria, LIG, Vincent LeroyUniversity of Grenoble - CNRS, Gwen SalaünUniversity of Grenoble Alpes, Emmanuel YahUniversité Grenoble Alpes
15:20 - 15:30
Discussion Period