PsALM provides a GUI (1) that allows the definition of robotic missions requirements through a structured English grammar which uses patterns as basic building blocks and AND and OR logic operators to compose these patterns.
The SE2PT component extracts from a mission requirement the set of patterns that are composed through the AND and OR operators (2). The PT2LTL (3) and PT2CTL (4) components automatically generate LTL and CTL specifications from these patterns.
The produced LTL specification is an intermediate non-ambiguous artifact that can be used in different ways – three possible usages are presented in the figure above. The LTL formulae are (i) fed into an existing planner and used to generate plans that satisfy the mission specification (5); (ii) converted into Deterministic Buchi automata used as input to the Spectra robotic application modeling tool (6); and (iii) converted into the NuSMV input language to be used as input for model checking (7). The plans produced using the planner are (i) used as inputs by the Simbad simulation package (1), which is an autonomous robot simulation package for education and research; and (ii) performed by actual real robots (9). Produced CTL specifications are also converted into the NuSMV input language to be used as input for model checking (7).
The open source PsALM toolchain has been submitted to the ICSE tool demonstration track.
Pending a seperate release of PsAlM, below you can the supporting tool.
PsAlM Download
| File | File Contents # |
|---|---|
| PsAlM.zip | 5 |
Installation guide
Download NuSMV and install it (if you want to use the simulator and the planning capability)
Execute the tool from command line, by running within the Psalm folder the following command java -jar psalm.jar
Define your mission
Select the mission by clicking on the button select mission when you are ready
Click on run the Simbad simulator
Load the environment environment0.txt