This page complements the manuscript "Robotic Mission Specification Patterns: Providing Support for Quantitative Properties"
and is an online repository of a quantitative specification pattern catalog for missions of mobile robots, along with an accompanying DSL and tool support: QUARTET
. The pattern system is not intended to be exhaustive or complete, and the repository is not intended to be static. The set of patterns will grow over time as designers specify missions that do not belong to the provided patterns.
You can further find the patterns, information on requirements collection as well as DSL and tool support through QUARTET. Reproduction kits, specifications and accompanying code can be found in evaluation. See also an introductory video to QUARTET.
Pattern Catalog
Elementary Patterns
Elementary mission specification problems capture fundamental quantitative measures
.
Pattern | Description |
---|---|
Maximise | Maximize m while performing the mission miss. |
Minimise | Minimize m while performing the mission miss. |
At most | Keep m lower than or equal to v while performing miss. |
Less than | Keep m strictly lower than v while performing miss. |
At least | Keep m greater than or equal to v while performing miss. |
Greater than | Keep m strictly greater than v while performing miss. |
Exactly | Keep m exactly v while performing miss. |
Bounding the value | Keep m within the (closed) interval [v1, v2] while performing miss. |
Strict bounding the value | Keep m within the (open) interval (v1, v2) while performing miss. |
Composite Patterns
Composite mission specification problems express higher- order robotics concerns
.
Pattern | Description |
---|---|
Conservation | Minimize the value of m performing miss. |
Preservation | Keep the value of m within interval [bl ,bu ] while performing miss. |
Pause | Pause the mission miss for m time instants. Then, restart it. |
Timeout-deadline | Execute miss. Stop the the execution when the timeout m is reached. |
Repeat | Repeat the mission miss every m time units. |
End | Terminate mission miss exactly at time m. |
Proportionality | Keep the time to perform miss1 and miss2 proportional by a factor p. |
Simultaneously | Execute the actions act1 ,act2 ,…, actn simultaneously. |
Accrue | Maximize the performance m while performing miss. |
Reliably | Ensure that the measure m is higher/lower than the value v. |
Confidently | Achieve miss and ensure that confidence m is higher/lower than v. |
Equidistance | rob performs miss by keeping rob1 and rob2 at the same distance. |
Trail | rob follows object o keeping a distance v. |