2018
Journal article
Open Access
Spatio-temporal model checking of vehicular movement in public transport systems
Ciancia V., Gilmore S., Grilletti G., Latella D., Loreti M., Massink M.
Spation-temporal model checking Collective adaptive systems Formal methods for system design & analysis Information Systems Software Smart transportation Spatio-temporal model-checking
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.
Source: International journal on software tools for technology transfer (Internet) 20 (2018): 289–311. doi:10.1007/s10009-018-0483-8
Publisher: Springer, Berlin , Germania
1. Marco Aiello. Spatial Reasoning: Theory and Practice. PhD thesis, ILLC, University of Amsterdam, 2002.
2. Francesco Luca De Angelis and Giovanna Di Marzo Serugendo. Towards a spatial language for run-time assessments in self-organizing systems. In 2015 IEEE 9th International Conference on Self-Adaptive and Self-Organizing Systems, Cambridge, MA, USA, September 21-25, 2015, pages 174{175. IEEE Computer Society, 2015.
3. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.
4. Ezio Bartocci, Ebru Aydin Gol, Iman Haghighi, and Calin Belta. A formal methods approach to pattern recognition and synthesis in reaction di usion networks. IEEE Transactions on Control of Network Systems, pages 1{1, 2016.
5. Gina Belmonte, Vincenzo Ciancia, Diego Latella, and Mieke Massink. From collective adaptive systems to human centric computation and back: Spatial model checking for medical imaging. In Proceedings of the Workshop on FORmal methods for the quantitative Evaluation of Collective Adaptive SysTems, FORECAST@STAF 2016, Vienna, Austria, 8 July 2016., volume 217 of EPTCS, pages 81{92, 2016.
6. Mordechai Ben-Ari, Amir Pnueli, and Zohar Manna. The temporal logic of branching time. Acta Informatica, 20(3):207{226, 1983.
7. Alberto Del Bimbo, Enrico Vicario, and Daniele Zingoni. Symbolic description and visual querying of image sequences using spatio-temporal logic. IEEE Trans. Knowl. Data Eng., 7(4):609{622, 1995.
8. Luca Bortolussi and Laura Nenzi. Specifying and monitoring properties of stochastic spatio-temporal systems in signal temporal logic. In VALUETOOLS, 2014.
9. Francesco Buccafurri, Thomas Eiter, Georg Gottlob, and Nicola Leone. On ACTL formulas having linear counterexamples. J. Comput. Syst. Sci., 62(3):463{515, 2001.
10. Luis Caires. Behavioral and spatial observations in a logic for the -calculus. In Proceedings of the 7th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'04), volume 2987 of LNCS, pages 72{87. Springer, 2004.
11. Luca Cardelli and Philippa Gardner. Processes in space. Theoretical Computer Science, 431(0):40 { 55, 2012. Modelling and Analysis of Biological Systems Based on papers presented at the Workshop on Membrane Computing and Bio-logically Inspired Process Calculi (MeCBIC) held in 2008 (Iasi), 2009 (Bologna) and 2010 (Jena).
12. Luca Cardelli and Andrew D. Gordon. Anytime, anywhere: Modal logics for mobile ambients. In Proceedings of the 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'00), pages 365{377, 2000.
13. Vincenzo Ciancia, Gianluca Grilletti, Diego Latella, Michele Loreti, and Mieke Massink. An experimental spatio-temporal model checker. In Software Engineering and Formal Methods - SEFM 2015 Collocated Workshops, volume 9509 of Lecture Notes in Computer Science, pages 297{311. Springer, 2015.
14. Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. Specifying and Verifying Properties of Space. In Springer, editor, The 8th IFIP International Conference on Theoretical Computer Science, TCS 2014, Track B, volume 8705 of Lecture Notes in Computer Science, pages 222{235, 2014.
15. Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. Model Checking Spatial Logics for Closure Spaces. Logical Methods in Computer Science, Volume 12, Issue 4, October 2016.
16. Vincenzo Ciancia, Diego Latella, Mieke Massink, Rytis Paskauskas, and Andrea Vandin. A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In Tiziana Margaria and Bernhard Ste en, editors, Leveraging Applications of Formal Methods, Veri cation and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part I, volume 9952 of Lecture Notes in Computer Science, pages 657{673, 2016.
17. Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Logic of Programs, volume 131 of Lecture Notes in Computer Science, pages 53{71. Springer, 1986.
18. Edmund M. Clarke and Helmut Veith. Counterexamples revisited: Principles, algorithms, applications. In Nachum Dershowitz, editor, Veri cation: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, volume 2772 of Lecture Notes in Computer Science, pages 208{224. Springer, 2003.
19. Carlos F. Daganzo. A headway-based approach to eliminate bus bunching: Systematic analysis and comparisons. Transportation Research Part B: Methodological, 43(10):913 { 921, 2009.
20. Carlos F. Daganzo and Josh Pilachowski. Reducing bunching with bus-to-bus cooperation. Transportation Research Part B: Methodological, 45(1):267 { 277, 2011.
21. Rocco De Nicola, Joost-Pieter Katoen, Diego Latella, Michele Loreti, and Mieke Massink. Model checking mobile stochastic logic. Theor. Comput. Sci., 382(1):42{70, 2007.
22. Simon A. Dobson, Mirko Viroli, Jose Luis Fernandez-Marquez, Franco Zambonelli, Graeme Stevenson, Giovanna Di Marzo Serugendo, Sara Montagna, Danilo Pianini, Juan Ye, Gabriella Castelli, and Alberto Rosi. Spatial awareness in pervasive ecosystems. Knowledge Eng. Review, 31(4):343{366, 2016.
23. E. Allen Emerson. Temporal and modal logic. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science (Vol. B), pages 995{1072. MIT Press, Cambridge, MA, USA, 1990.
24. Alireza Fathi and John Krumm. Detecting road intersections from GPS traces. In SaraIrina Fabrikant, Tumasch Reichenbacher, Marc van Kreveld, and Christoph Schlieder, editors, Geographic Information Science, volume 6292 of Lecture Notes in Computer Science, pages 56{69. Springer Berlin Heidelberg, 2010.
25. Ebru A. Gol, Ezio Bartocci, and Calin Belta. A formal methods approach to pattern synthesis in reaction di usion systems. In 53rd IEEE Conference on Decision and Control, pages 108{113, 2014.
26. Gianluca Grilletti. Spatio-temporal model checking: Explicit and abstraction-based methods. Master's thesis, Dipartimento di Matematica, Universita di Pisa, 2016.
27. Radu Grosu, Scott A. Smolka, Flavio Corradini, Anita Wasilewska, Emilia Entcheva, and Ezio Bartocci. Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM, 52(3):97{105, 2009.
28. John J. Bartholdi III, Russell J. Clark, David W. Williamson, Donald D. Eisenstein, and Loren K. Platzman. Building a self-organizing urban bus route. In Sixth IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASOW 2012, Lyon, France, September 10-14, 2012, pages 66{70. IEEE Computer Society, 2012.
29. John J. Bartholdi III and Donald D. Eisenstein. A self-coordinating bus route to resist bus bunching. Transportation Research Part B: Methodological, 46(4):481 { 491, 2012.
30. Mathias John, Roland Ewald, and Adelinde M. Uhrmacher. A spatial extension to the pi calculus. Electronic Notes in Theoretical Computer Science, 194(3):133 { 148, 2008. Proceedings of the First Workshop From Biology To Concurrency and back (FBTC 2007).
31. Roman Kontchakov, Agi Kurucz, Frank Wolter, and Michael Zakharyaschev. Spatial logic + temporal logic = ? In Marco Aiello, Ian Pratt-Hartmann, and Johan van Benthem, editors, Handbook of Spatial Logics, pages 497{564. Springer, 2007.
32. Julia Letchner, John Krumm, and Eric Horvitz. Trip Router with Individualized Preferences (TRIP): Incorporating personalization into route planning. In Proceedings of the 18th Conference on Innovative Applications of Arti cial Intelligence - Volume 2, IAAI'06, pages 1795{1800. AAAI Press, 2006.
33. Laura Nenzi, Luca Bortolussi, Vincenzo Ciancia, Michele Loreti, and Mieke Massink. Qualitative and quantitative monitoring of spatio-temporal properties. In Runtime Veri cation - 6th International Conference, RV 2015 Vienna, Austria, September 22-25, 2015. Proceedings, volume 9333 of Lecture Notes in Computer Science, pages 21{37. Springer, 2015.
34. Gordon F. Newell and Renfrey B. Potts. Maintaining a bus schedule. In Proceedings of 2nd Australian Road Research Board, volume 2, pages 388{393, 1964.
35. Celestino Ordon~ez, Javier Mart nez, Jose Rodr guez-Perez, and Andria Reyes. Detection of outliers in GPS measurements by using functional-data analysis. Journal of Surveying Engineering, 137(4):150{155, 2011.
36. Daniel Reijsbergen and Stephen Gilmore. Formal punctuality analysis of frequent bus services using headway data. In Andras Horvath and Katinka Wolter, editors, Computer Performance Engineering - 11th European Workshop, EPEW 2014, Florence, Italy, September 11-12, 2014. Proceedings, volume 8721 of Lecture Notes in Computer Science, pages 164{178. Springer, 2014.
37. Minyan Ruan and Jie Lin. An investigation of bus headway regularity and service performance in Chicago bus transit system. In Transport Chicago, Annual Conference, 14., 2009.
38. James G. Strathman, Thomas J. Kimpel, and Steve Callas. Headway deviation e ects on bus passenger loads: Analysis of Tri-Met's archived AVL-APC data. Technical Report PR126, Portland State University, Centre for Urban Studies, Oregon, 2003.
39. Christos Tsigkanos, Timo Kehrer, and Carlo Ghezzi. Modeling and veri cation of evolving cyber-physical spaces. In Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2017, Paderborn, Germany, September 4-8, 2017, pages 38{48. ACM, 2017.
40. Christos Tsigkanos, Liliana Pasquale, Carlo Ghezzi, and Bashar Nuseibeh. Ariadne: Topology aware adaptive security for cyber-physical systems. In 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering, volume 2, pages 729{732, May 2015.
41. Johan van Benthem and Guram Bezhanishvili. Modal logics of space. In Marco Aiello, Ian Pratt-Hartmann, and Johan van Benthem, editors, Handbook of Spatial Logics, pages 217{298. Springer, 2007.
42. Yiguang Xuan, Juan Argote, and Carlos F. Daganzo. Dynamic bus holding strategies for schedule reliability: Optimal linear control and performance analysis. Transportation Research Part B: Methodological, 45(1):1831 { 1845, 2011.
43. Zhixian Yan. Traj-ARIMA: A spatial-time series model for network-constrained trajectory. In Proceedings of the Second International Workshop on Computational Transportation Science, IWCTS '10, pages 11{16, New York, NY, USA, 2010. ACM.
44. Jiamin Zhao, Maged Dessouky, and Satish Bukkapatnam. Optimal slack time for schedulebased transit operations. Transportation Science, 40(4):529{539, 2006.
2. Francesco Luca De Angelis and Giovanna Di Marzo Serugendo. Towards a spatial language for run-time assessments in self-organizing systems. In 2015 IEEE 9th International Conference on Self-Adaptive and Self-Organizing Systems, Cambridge, MA, USA, September 21-25, 2015, pages 174{175. IEEE Computer Society, 2015.
3. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.
4. Ezio Bartocci, Ebru Aydin Gol, Iman Haghighi, and Calin Belta. A formal methods approach to pattern recognition and synthesis in reaction di usion networks. IEEE Transactions on Control of Network Systems, pages 1{1, 2016.
5. Gina Belmonte, Vincenzo Ciancia, Diego Latella, and Mieke Massink. From collective adaptive systems to human centric computation and back: Spatial model checking for medical imaging. In Proceedings of the Workshop on FORmal methods for the quantitative Evaluation of Collective Adaptive SysTems, FORECAST@STAF 2016, Vienna, Austria, 8 July 2016., volume 217 of EPTCS, pages 81{92, 2016.
6. Mordechai Ben-Ari, Amir Pnueli, and Zohar Manna. The temporal logic of branching time. Acta Informatica, 20(3):207{226, 1983.
7. Alberto Del Bimbo, Enrico Vicario, and Daniele Zingoni. Symbolic description and visual querying of image sequences using spatio-temporal logic. IEEE Trans. Knowl. Data Eng., 7(4):609{622, 1995.
8. Luca Bortolussi and Laura Nenzi. Specifying and monitoring properties of stochastic spatio-temporal systems in signal temporal logic. In VALUETOOLS, 2014.
9. Francesco Buccafurri, Thomas Eiter, Georg Gottlob, and Nicola Leone. On ACTL formulas having linear counterexamples. J. Comput. Syst. Sci., 62(3):463{515, 2001.
10. Luis Caires. Behavioral and spatial observations in a logic for the -calculus. In Proceedings of the 7th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'04), volume 2987 of LNCS, pages 72{87. Springer, 2004.
11. Luca Cardelli and Philippa Gardner. Processes in space. Theoretical Computer Science, 431(0):40 { 55, 2012. Modelling and Analysis of Biological Systems Based on papers presented at the Workshop on Membrane Computing and Bio-logically Inspired Process Calculi (MeCBIC) held in 2008 (Iasi), 2009 (Bologna) and 2010 (Jena).
12. Luca Cardelli and Andrew D. Gordon. Anytime, anywhere: Modal logics for mobile ambients. In Proceedings of the 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'00), pages 365{377, 2000.
13. Vincenzo Ciancia, Gianluca Grilletti, Diego Latella, Michele Loreti, and Mieke Massink. An experimental spatio-temporal model checker. In Software Engineering and Formal Methods - SEFM 2015 Collocated Workshops, volume 9509 of Lecture Notes in Computer Science, pages 297{311. Springer, 2015.
14. Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. Specifying and Verifying Properties of Space. In Springer, editor, The 8th IFIP International Conference on Theoretical Computer Science, TCS 2014, Track B, volume 8705 of Lecture Notes in Computer Science, pages 222{235, 2014.
15. Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. Model Checking Spatial Logics for Closure Spaces. Logical Methods in Computer Science, Volume 12, Issue 4, October 2016.
16. Vincenzo Ciancia, Diego Latella, Mieke Massink, Rytis Paskauskas, and Andrea Vandin. A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In Tiziana Margaria and Bernhard Ste en, editors, Leveraging Applications of Formal Methods, Veri cation and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part I, volume 9952 of Lecture Notes in Computer Science, pages 657{673, 2016.
17. Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Logic of Programs, volume 131 of Lecture Notes in Computer Science, pages 53{71. Springer, 1986.
18. Edmund M. Clarke and Helmut Veith. Counterexamples revisited: Principles, algorithms, applications. In Nachum Dershowitz, editor, Veri cation: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, volume 2772 of Lecture Notes in Computer Science, pages 208{224. Springer, 2003.
19. Carlos F. Daganzo. A headway-based approach to eliminate bus bunching: Systematic analysis and comparisons. Transportation Research Part B: Methodological, 43(10):913 { 921, 2009.
20. Carlos F. Daganzo and Josh Pilachowski. Reducing bunching with bus-to-bus cooperation. Transportation Research Part B: Methodological, 45(1):267 { 277, 2011.
21. Rocco De Nicola, Joost-Pieter Katoen, Diego Latella, Michele Loreti, and Mieke Massink. Model checking mobile stochastic logic. Theor. Comput. Sci., 382(1):42{70, 2007.
22. Simon A. Dobson, Mirko Viroli, Jose Luis Fernandez-Marquez, Franco Zambonelli, Graeme Stevenson, Giovanna Di Marzo Serugendo, Sara Montagna, Danilo Pianini, Juan Ye, Gabriella Castelli, and Alberto Rosi. Spatial awareness in pervasive ecosystems. Knowledge Eng. Review, 31(4):343{366, 2016.
23. E. Allen Emerson. Temporal and modal logic. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science (Vol. B), pages 995{1072. MIT Press, Cambridge, MA, USA, 1990.
24. Alireza Fathi and John Krumm. Detecting road intersections from GPS traces. In SaraIrina Fabrikant, Tumasch Reichenbacher, Marc van Kreveld, and Christoph Schlieder, editors, Geographic Information Science, volume 6292 of Lecture Notes in Computer Science, pages 56{69. Springer Berlin Heidelberg, 2010.
25. Ebru A. Gol, Ezio Bartocci, and Calin Belta. A formal methods approach to pattern synthesis in reaction di usion systems. In 53rd IEEE Conference on Decision and Control, pages 108{113, 2014.
26. Gianluca Grilletti. Spatio-temporal model checking: Explicit and abstraction-based methods. Master's thesis, Dipartimento di Matematica, Universita di Pisa, 2016.
27. Radu Grosu, Scott A. Smolka, Flavio Corradini, Anita Wasilewska, Emilia Entcheva, and Ezio Bartocci. Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM, 52(3):97{105, 2009.
28. John J. Bartholdi III, Russell J. Clark, David W. Williamson, Donald D. Eisenstein, and Loren K. Platzman. Building a self-organizing urban bus route. In Sixth IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASOW 2012, Lyon, France, September 10-14, 2012, pages 66{70. IEEE Computer Society, 2012.
29. John J. Bartholdi III and Donald D. Eisenstein. A self-coordinating bus route to resist bus bunching. Transportation Research Part B: Methodological, 46(4):481 { 491, 2012.
30. Mathias John, Roland Ewald, and Adelinde M. Uhrmacher. A spatial extension to the pi calculus. Electronic Notes in Theoretical Computer Science, 194(3):133 { 148, 2008. Proceedings of the First Workshop From Biology To Concurrency and back (FBTC 2007).
31. Roman Kontchakov, Agi Kurucz, Frank Wolter, and Michael Zakharyaschev. Spatial logic + temporal logic = ? In Marco Aiello, Ian Pratt-Hartmann, and Johan van Benthem, editors, Handbook of Spatial Logics, pages 497{564. Springer, 2007.
32. Julia Letchner, John Krumm, and Eric Horvitz. Trip Router with Individualized Preferences (TRIP): Incorporating personalization into route planning. In Proceedings of the 18th Conference on Innovative Applications of Arti cial Intelligence - Volume 2, IAAI'06, pages 1795{1800. AAAI Press, 2006.
33. Laura Nenzi, Luca Bortolussi, Vincenzo Ciancia, Michele Loreti, and Mieke Massink. Qualitative and quantitative monitoring of spatio-temporal properties. In Runtime Veri cation - 6th International Conference, RV 2015 Vienna, Austria, September 22-25, 2015. Proceedings, volume 9333 of Lecture Notes in Computer Science, pages 21{37. Springer, 2015.
34. Gordon F. Newell and Renfrey B. Potts. Maintaining a bus schedule. In Proceedings of 2nd Australian Road Research Board, volume 2, pages 388{393, 1964.
35. Celestino Ordon~ez, Javier Mart nez, Jose Rodr guez-Perez, and Andria Reyes. Detection of outliers in GPS measurements by using functional-data analysis. Journal of Surveying Engineering, 137(4):150{155, 2011.
36. Daniel Reijsbergen and Stephen Gilmore. Formal punctuality analysis of frequent bus services using headway data. In Andras Horvath and Katinka Wolter, editors, Computer Performance Engineering - 11th European Workshop, EPEW 2014, Florence, Italy, September 11-12, 2014. Proceedings, volume 8721 of Lecture Notes in Computer Science, pages 164{178. Springer, 2014.
37. Minyan Ruan and Jie Lin. An investigation of bus headway regularity and service performance in Chicago bus transit system. In Transport Chicago, Annual Conference, 14., 2009.
38. James G. Strathman, Thomas J. Kimpel, and Steve Callas. Headway deviation e ects on bus passenger loads: Analysis of Tri-Met's archived AVL-APC data. Technical Report PR126, Portland State University, Centre for Urban Studies, Oregon, 2003.
39. Christos Tsigkanos, Timo Kehrer, and Carlo Ghezzi. Modeling and veri cation of evolving cyber-physical spaces. In Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2017, Paderborn, Germany, September 4-8, 2017, pages 38{48. ACM, 2017.
40. Christos Tsigkanos, Liliana Pasquale, Carlo Ghezzi, and Bashar Nuseibeh. Ariadne: Topology aware adaptive security for cyber-physical systems. In 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering, volume 2, pages 729{732, May 2015.
41. Johan van Benthem and Guram Bezhanishvili. Modal logics of space. In Marco Aiello, Ian Pratt-Hartmann, and Johan van Benthem, editors, Handbook of Spatial Logics, pages 217{298. Springer, 2007.
42. Yiguang Xuan, Juan Argote, and Carlos F. Daganzo. Dynamic bus holding strategies for schedule reliability: Optimal linear control and performance analysis. Transportation Research Part B: Methodological, 45(1):1831 { 1845, 2011.
43. Zhixian Yan. Traj-ARIMA: A spatial-time series model for network-constrained trajectory. In Proceedings of the Second International Workshop on Computational Transportation Science, IWCTS '10, pages 11{16, New York, NY, USA, 2010. ACM.
44. Jiamin Zhao, Maged Dessouky, and Satish Bukkapatnam. Optimal slack time for schedulebased transit operations. Transportation Science, 40(4):529{539, 2006.
Metrics
Back to previous page
BibTeX entry
@article{oai:it.cnr:prodotti:387128,
title = {Spatio-temporal model checking of vehicular movement in public transport systems},
author = {Ciancia V. and Gilmore S. and Grilletti G. and Latella D. and Loreti M. and Massink M.},
publisher = {Springer, Berlin , Germania},
doi = {10.1007/s10009-018-0483-8},
journal = {International journal on software tools for technology transfer (Internet)},
volume = {20},
pages = {289–311},
year = {2018}
}
0000-0003-1314-0574
