PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Ciancia V., Latella D., Massink M., Paskauskas R., Vandin A. A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In: ISOLA 2016 - Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 7th International Symposium (Corfu, Greece, 10-14 October 2016). Proceedings, vol. Part I pp. 657 - 673. Tiziana Margaria, Bernhard Steffen (eds.). (Lecture Notes in Computer Science, vol. 9952). Springer, 2016.
 
 
Abstract
(English)
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.
URL: http://link.springer.com/chapter/10.1007/978-3-319-47166-2_46
DOI: 10.1007/978-3-319-47166-2_46
Subject Statistical Model-checking
Spatial Logics
Spatial Logics Model-checking
Smart cities
Bike-sharing
F.4.1 MATHEMATICAL LOGIC AND FORMAL LANGUAGES. Mathematical Logic
D.2.4 SOFTWARE ENGINEERING. Software/Program Verification


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional