Abstract
We report on a case study in which we have formally specified a ride-sharing system in Maude, a rewriting logic-based specification/programming language and model checked that the system enjoys desired liveness as well as safety properties with the Maude LTL model checker. In our approach to formal specification of the system, a map, a collection of cars and a collection of persons are treated as parameters. Thus, it suffices to write one formal systems specification from which the specification instance is generated for each fixed map, each fixed collection of cars and each fixed collection of persons. We often need fairness assumptions to model check liveness properties, which makes model checking performance slower or even infeasible. The case study also demonstrates that such a situation can be alleviated by a divide & conquer approach to liveness model checking under fairness.
This work was supported in part by JSPS KAKENHI Grant Number JP19H04082.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Newcomb, D.: You won’t need a driver’s license by 2040. https://www.wired.com/2012/09/ieee-autonomous-2040/ (2012)
Clavel, M., et al.: All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1
Ogata, K.: A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions. Front. Comput. Sci. 13, 51–72 (2019)
Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State/event-based software model checking. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 128–147. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24756-2_8
d’Orey, P.M., Fernandes, R., Ferreira, M.: Empirical evaluation of a dynamic and distributed taxi-sharing system. In: 15th IEEE ITSC, pp. 140–146 (2012)
Kristensen, T., Ezeora, N.J.: Simulation of intelligent traffic control for autonomous vehicles. In: IEEE ICIA 2017, pp. 459–465 (2017)
Choi, S., Yeo, H.: Framework for simulation-based lane change control for autonomous vehicles. In: IEEE IV 2017, pp. 699–704 (2017)
Zhang, C., Liu, Y., Zhao, D., Su, Y.: RoadView: a traffic scene simulator for autonomous vehicle simulation testing. In: 17th IEEE ITSC, pp. 1160–1165 (2014)
Fernandes, L.E.R., Custodio, V., Alves, G.V., Fisher, M.: A rational agent controlling an autonomous vehicle: implementation and formal verification. In: 1st FVAV. EPTCS, vol. 257, pp. 35–42 (2017)
Mitsch, S., Ghorbal, K., Vogelbacher, D., Platzer, A.: Formal verification of obstacle avoidance and navigation of ground robots. Int. J. Robot. Res. 36, 1312–1340 (2017)
Meseguer, J.: Localized fairness: a rewriting semantics. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 250–263. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-32033-3_19
Bae, K., Meseguer, J.: Model checking linear temporal logic of rewriting formulas under localized fairness. Sci. Comput. Program. 99, 193–234 (2015)
Ogata, K., Futatsugi, K.: Comparison of Maude and SAL by conducting case studies model checking a distributed algorithm. IEICE Trans. Fundam. 90-A, 1690–1703 (2007)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Muramoto, E., Ogata, K., Shinoda, Y. (2020). Formal Specification and Model Checking of a Ride-sharing System in Maude. In: Miao, H., Tian, C., Liu, S., Duan, Z. (eds) Structured Object-Oriented Formal Language and Method. SOFL+MSVL 2019. Lecture Notes in Computer Science(), vol 12028. Springer, Cham. https://doi.org/10.1007/978-3-030-41418-4_14
Download citation
DOI: https://doi.org/10.1007/978-3-030-41418-4_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-41417-7
Online ISBN: 978-3-030-41418-4
eBook Packages: Computer ScienceComputer Science (R0)