{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,17]],"date-time":"2026-10-17T19:17:01Z","timestamp":1792264621856,"version":"4.4.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319101804","type":"print"},{"value":"9783319101811","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10181-1_5","type":"book-chapter","created":{"date-parts":[[2014,8,29]],"date-time":"2014-08-29T14:28:38Z","timestamp":1409322518000},"page":"71-86","source":"Crossref","is-referenced-by-count":17,"title":["An Analysis Pathway for the Quantitative Evaluation of Public Transport Systems"],"prefix":"10.1007","author":[{"given":"Stephen","family":"Gilmore","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mirco","family":"Tribastone","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrea","family":"Vandin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Tang, L., (Vonu) Thakuriah, P.: Ridership effects of real-time bus information system: A case study in the city of Chicago. Transportation Research Part C: Emerging Technologies\u00a022, 146\u2013161 (2012)","DOI":"10.1016\/j.trc.2012.01.001"},{"key":"5_CR2","unstructured":"The\u00a0City of\u00a0Edinburgh\u00a0Council. Bus Tracker Edinburgh real-time bus information website (2014), \n                        http:\/\/www.mybustracker.co.uk"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-642-40725-3_13","volume-title":"Computer Performance Engineering","author":"P. Reinecke","year":"2013","unstructured":"Reinecke, P., Krau\u00df, T., Wolter, K.: Phase-type fitting using HyperStar. In: Balsamo, M.S., Knottenbelt, W.J., Marin, A. (eds.) EPEW 2013. LNCS, vol.\u00a08168, pp. 164\u2013175. Springer, Heidelberg (2013)"},{"issue":"33-34","key":"5_CR4","doi-asserted-by":"publisher","first-page":"3065","DOI":"10.1016\/j.tcs.2009.02.037","volume":"410","author":"F. Ciocchetta","year":"2009","unstructured":"Ciocchetta, F., Hillston, J.: Bio-PEPA: A framework for the modelling and analysis of biological systems. Theoretical Computer Science\u00a0410(33-34), 3065\u20133084 (2009)","journal-title":"Theoretical Computer Science"},{"key":"5_CR5","unstructured":"Sebastio, S., Vandin, A.: MultiVeStA: Statistical model checking for discrete event simulators. In: 7th International Conference on Performance Evaluation Methodologies and Tools, VALUETOOLS, Torino, Italy (December 2013)"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Duguid, A., Gilmore, S., Guerriero, M.L., Hillston, J., Loewe, L.: Design and development of software tools for Bio-PEPA. In: Dunkin, A., Ingalls, R.G., Y\u00fccesan, E., Rossetti, M.D., Hill, R., Johansson, B. (eds.) Winter Simulation Conference, WSC, pp. 956\u2013967 (2009)","DOI":"10.1109\/WSC.2009.5429725"},{"key":"5_CR7","unstructured":"Vissat, L.L., Clark, A., Gilmore, S.: Finding optimal timetables for Edinburgh bus routes. In: Proceedings of the Seventh International Workshop on Practical Applications of Stochastic Modelling (PASM 2014), Newcastle, England (May 2014)"},{"issue":"2","key":"5_CR8","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1109\/TSE.2008.75","volume":"35","author":"P. Kemper","year":"2009","unstructured":"Kemper, P., Tepperp, C.: Automated trace analysis of discrete-event system models. IEEE Trans. Software Eng.\u00a035(2), 195\u2013208 (2009)","journal-title":"IEEE Trans. Software Eng."},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"5_CR10","unstructured":"Czarnecki, K., Eiseneckerp, U.W.: Generative Programming: Methods, Tools, and Applications. Addison-Wesley (2000)"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Boehm, B.W., Garlan, D., Kramer, J. (eds.) ICSE, pp. 411\u2013420. ACM (1999)","DOI":"10.1145\/302405.302672"},{"key":"5_CR12","unstructured":"Reed, S.: Transport for London\u2014Using tools, analytics and data to inform passengers. Journeys, 96\u2013104 (September 2013)"},{"key":"5_CR13","unstructured":"Tranter, M.: Department for Transport\u2014annual bus statistics: England 2012\/2013 (September 2013)"},{"key":"5_CR14","unstructured":"Smarter Scotland: Scottish Government. Bus Punctuality Improvement Partnerships (BPIP) (March 2009)"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Stewart, W.J.: Probability, Markov Chains, Queues, and Simulation. Princeton University Press (2009)","DOI":"10.1515\/9781400832811"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-642-19811-3_8","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Massink","year":"2011","unstructured":"Massink, M., Latella, D., Bracciali, A., Hillston, J.: Modelling non-linear crowd dynamics in Bio-PEPA. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol.\u00a06603, pp. 96\u2013110. Springer, Heidelberg (2011)"},{"issue":"2","key":"5_CR17","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s00165-011-0188-1","volume":"24","author":"M. Massink","year":"2012","unstructured":"Massink, M., Latella, D., Bracciali, A., Harrison, M.D., Hillston, J.: Scalable context-dependent analysis of emergency egress models. Formal Aspects of Computing\u00a024(2), 267\u2013302 (2012)","journal-title":"Formal Aspects of Computing"},{"issue":"2-3","key":"5_CR18","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/s11721-013-0079-6","volume":"7","author":"M. Massink","year":"2013","unstructured":"Massink, M., Brambilla, M., Latella, D., Dorigo, M., Birattari, M.: On the use of Bio-PEPA for modelling and analysing collective behaviours in swarm robotics. Swarm Intelligence\u00a07(2-3), 201\u2013228 (2013)","journal-title":"Swarm Intelligence"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-54624-2_10","volume-title":"Specification, Algebra, and Software","author":"L. Belzner","year":"2014","unstructured":"Belzner, L., De Nicola, R., Vandin, A., Wirsing, M.: Reasoning (on) service component ensembles in rewriting logic. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol.\u00a08373, pp. 188\u2013211. Springer, Heidelberg (2014)"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Sebastio, S., Amoretti, M., Lluch-Lafuente, A.: A computational field framework for collaborative task execution in volunteer clouds. In: Proceedings of the 9th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2014) (2014)","DOI":"10.1145\/2593929.2593943"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Pianini, D., Sebastio, S., Vandin, A.: Distributed statistical analysis of complex systems modeled through a chemical metaphor. In: 5th International Workshop on Modeling and Simulation of Peer-to-Peer and Autonomic Systems (MOSPAS 2014) (2014)","DOI":"10.1109\/HPCSim.2014.6903715"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-60045-0_48","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1995","unstructured":"Aziz, A., Singhal, V., Balarin, F., Brayton, R., Sangiovanni-Vincentelli, A.L.: It usually works: The temporal logic of stochastic systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 155\u2013165. Springer, Heidelberg (1995)"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"CONCUR\u201999. Concurrency Theory","author":"C. Baier","year":"1999","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H.: Approximate Symbolic Model Checking of Continuous-Time Markov Chains (Extended Abstract). In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 146\u2013161. Springer, Heidelberg (1999)"},{"issue":"5","key":"5_CR24","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput.\u00a06(5), 512\u2013535 (1994)","journal-title":"Formal Asp. Comput."}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10181-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,28]],"date-time":"2023-01-28T08:26:59Z","timestamp":1674894419000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-10181-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319101804","9783319101811"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10181-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}