Rapporto tecnico, 2016, ENG

On spatio-temporal model-checking of vehicular movement in public transport systems

Ciancia V.; Gilmore S.; Grilletti G.; Latella D.; Loreti M.; Massink M.

CNR-ISTI, Pisa, Italy; University of Edinburgh, Edinburgh, Scotland; Scuola Normale Superiore, Pisa, Italy; CNR-ISTI, Pisa, Italy; Università di Firenze, Firenze e IMT-Lucca, Italy; CNR-ISTI, Pisa, Italy

In this paper we present the use of a novel spatio-temporal model-checker to detect problems in the data and operation of an adaptive system. We categorise received data as being plausible, implausible, possible or problematic. Data correctness is essential to ensure behavioural correctness in systems which adapt in response to data and our categorisation suggests the degree of caution which should be used in acting in response to this received 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 behavioural phenomenon of clumping", the undesired reduction of separation between subsequent buses serving the same route. Vehicle location data is visualised symbolically on a street map, and categories of problems identied by the spatial part of the model-checker are rendered by repainting the symbols for vehicles in dierent colours. 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.

Keywords

Spatio-temporal logics, Specifying and verifying and reasoning about programs

CNR authors

Massink Mieke, Latella Diego, Ciancia Vincenzo

CNR institutes

ISTI – Istituto di scienza e tecnologie dell'informazione "Alessandro Faedo"

ID: 362866

Year: 2016

Type: Rapporto tecnico

Creation: 2016-12-19 11:10:25.000

Last update: 2021-01-28 15:39:53.000

External links

OAI-PMH: Dublin Core

OAI-PMH: Mods

OAI-PMH: RDF

External IDs

CNR OAI-PMH: oai:it.cnr:prodotti:362866