Document - A tool-chain for statistical spatio-temporal model checking of bike sharing systems

2016

Conference article Open Access

A tool-chain for statistical spatio-temporal model checking of bike sharing systems

Ciancia V., Latella D., Massink M., Paskauskas R., Vandin A.

Bike-sharing Statistical Model-checking Smart cities F.4.1 MATHEMATICAL LOGIC AND FORMAL LANGUAGES. Mathematical Logic Spatial Logics Model-checking D.2.4 SOFTWARE ENGINEERING. Software/Program Verification Spatial Logics

Prominent examples of collective systems are often encountered when analysing smart cities and smart transportation systems. We propose a novel modelling and analysis approach combining statistical model checking, spatio-temporal logics, and simulation. The proposed methodology is applied to modelling and statistical analysis of user behaviour in bike sharing systems. We present a tool-chain that integrates the statistical analysis toolkit MultiVeStA, the spatio-temporal model checker topochecker, and a bike sharing systems simulator based on Markov renewal processes. The obtained tool allows one to estimate, up to a user-specified precision, the likelihood of specific spatio-temporal formulas, such as the formation of clusters of full stations and their temporal evolution.

Source: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 7th International Symposium, pp. 657–673, Corfu, Greece, 10-14 October 2016

Metrics

Back to previous page

Cite as

BibTeX entry

@inproceedings{oai:it.cnr:prodotti:359672,
	title = {A tool-chain for statistical spatio-temporal model checking of bike sharing systems},
	author = {Ciancia V. and Latella D. and Massink M. and Paskauskas R. and Vandin A.},
	doi = {10.1007/978-3-319-47166-2_46},
	booktitle = {Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 7th International Symposium, pp. 657–673, Corfu, Greece, 10-14 October 2016},
	year = {2016}
}