Name
Abstract | ||
|---|---|---|
We present the use of a novel spatio-temporal model checker to detect problems in the data and operation of a collective adaptive system. Data correctness is important to ensure operational correctness in systems which adapt in response to data. We illustrate the theory with several concrete examples, addressing both the detection of errors in vehicle location data for buses in the city of Edinburgh and the undesirable phenomenon of “clumping” which occurs when there is not enough separation between subsequent buses serving the same route. Vehicle location data are visualised symbolically on a street map, and categories of problems identified by the spatial part of the model checker are rendered by highlighting the symbols for vehicles or other objects that satisfy a property of interest. Behavioural correctness makes use of both the spatial and temporal aspects of the model checker to determine from a series of observations of vehicle locations whether the system is failing to meet the expected quality of service demanded by system regulators. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1007/s10009-018-0483-8 | STTT |
Keywords | Field | DocType |
Spatio-temporal model checking, Collective adaptive systems, Smart transportation, 68N30, 68Q60, 03B70 | Model checking,Adaptive system,Computer science,Correctness,Road map,Quality of service,Real-time computing,Public transport,Location data,Collective adaptive systems | Journal |
Volume | Issue | ISSN |
20 | 3 | 1433-2779 |
Citations | PageRank | References |
3 | 0.39 | 27 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Vincenzo Ciancia | 1 | 84 | 7.32 |
| Stephen Gilmore | 2 | 3 | 0.39 |
| Gianluca Grilletti | 3 | 13 | 1.99 |
| Diego Latella | 4 | 1168 | 113.42 |
| Michele Loreti | 5 | 812 | 58.60 |
| Mieke Massink | 6 | 1095 | 87.58 |