Abstract
Automated bicycle-sharing systems (bss) are a prominent example of reconfigurable cyber-physical systems for which the locality and connectivity of their elements are central to the way in which they operate. These features motivate us to study bss from the perspective of Actor-Network Theory – a framework for modelling cyber-physical-system protocols in which systems are networks of actors that are no longer limited to programs but can also include humans and physical artefacts. In order to support logical reasoning about information-flow properties that occur in bss, we use a logical framework that we have recently developed for actor networks, which results from a two-stage hybridization process. The first stage corresponds to a logic that captures the locality and connectivity of actors in a given configuration of the network; the second stage corresponds to a logic of possible interactions between actors, which captures the dynamics of the system in terms of network reconfigurations. To illustrate the properties that can be checked using this framework, we provide an actor-network specification of a particular bss, and use a recently developed tool for hybridized logics to highlight and correct an information-flow vulnerability of the system.
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
Notes
- 1.
- 2.
- 3.
We use this colon notation to separate a propositional symbol from its sort, and also to separate a channel type from the two sorts on which it is defined.
- 4.
We annotate the variables of sort \(s\) with the set of actor names of sort \(s\) in order to ensure that there are no accidental clashes between variables and actors names.
- 5.
Similarly to the logic \(\mathsf {LNC}\), we annotate \(\mathsf {LAN}\)-variables with the set of configuration names in order to avoid accidental name clashes when building the extension.
- 6.
This problem is notorious for axiomatizing the way in which states change when an event occurs; various solutions have been proposed in connection to formalisms such as the situation calculus, event calculus, or default logic, among others; see, e.g. [28].
- 7.
For (11), note that \( \langle \mathsf {ask} {\rangle }\, r\) entails \( \langle \pi {\rangle }\, r\); moreover, under the hypothesis \(@_{u}\, \langle \mathsf {choose} {\rangle }\, b\), and by (3), (4) and the functionality of \(\pi \), \(@_{u}\, \langle \mathsf {ask} {\rangle }\, r\) and \(\exists \{d :\mathsf {Dock} {\}}\cdot @_{b}\, \langle \pi {\rangle }\, (d \wedge \langle \pi {\rangle }\, r{)}\) are semantically equivalent. Still, to give a better picture of the configurations affected by \(\mathsf {Take} \) (or by any of the other interactions), we write the precondition in full.
- 8.
When both \(X\) and \(Y\) are empty, we can further prove that \(\psi \) holds at all reachable configurations of the model of \(\langle \varOmega , \varGamma {\rangle }\) by verifying that \(\varGamma \) entails \(\mathsf {init}: \psi \).
References
Bartocci, E., Bortolussi, L., Loreti, M., Nenzi, L.: Monitoring mobile and spatially distributed cyber-physical systems. In: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2017, Vienna, Austria, 29 September–2 October 2017, pp. 146–155. ACM (2017)
ter Beek, M.H., Fantechi, A., Gnesi, S.: Challenges in modelling and analyzing quantitative aspects of bike-sharing systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part I. LNCS, vol. 8802, pp. 351–367. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-45234-9_25
ter Beek, M.H., Gnesi, S., Latella, D., Massink, M.: Towards automatic decision support for bike-sharing system design. In: Bianculli, D., Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9509, pp. 266–280. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-49224-6_22
Blackburn, P.: Representation, reasoning, and relational structures: a hybrid logic manifesto. Logic J. IGPL 8(3), 339–365 (2000)
Braüner, T.: Hybrid Logic and its Proof-Theory. Applied Logic Series, vol. 37. Springer, Dordrecht (2011). https://doi.org/10.1007/978-94-007-0002-4
Ciancia, V., Latella, D., Loreti, M., Massink, M.: Model checking spatial logics for closure spaces. Log. Methods Comput. Sci. 12(4), 1–51 (2016)
Codescu, M.: Hybridisation of institutions in Hets. In: 8th Conference on Algebra and Coalgebra in Computer Science, CALCO 2019, London, 3–6 June 2019
Codescu, M., Kuksa, E., Kutz, O., Mossakowski, T., Neuhaus, F.: Ontohub: a semantic repository engine for heterogeneous ontologies. Appl. Ontol. 12(3–4), 275–298 (2017)
Diaconescu, R.: Quasi-varieties and initial semantics for hybridized institutions. J. Log. Comput. 26(3), 855–891 (2016)
Diaconescu, R.: Introducing H, an institution-based formal specication and veri-cation language. CoRR abs/1908.09868 (2019)
Diaconescu, R., Codescu, M.: The H system. Developed in the project Formal Verication of Recongurable Systems (PN-III-P2-2.1-PED-2016-0494) at Simion Stoilow Institute of Mathematics of the Romanian Academy, Romania (2017–2018). http://imar.ro/~diacon/forver/forver.html
Diaconescu, R., Madeira, A.: Encoding hybridized institutions into first-order logic. Math. Struct. Comput. Sci. 26(5), 745–788 (2016)
Diaconescu, R., Stefaneas, P.S.: Ultraproducts and possible worlds semantics in institutions. Theor. Comput. Sci. 379(1–2), 210–230 (2007)
Fiadeiro, J.L., Ţuţu, I., Lopes, A., Pavlovic, D.: Logics for actor networks: a two-stage constrained-hybridisation approach. J. Log. Algebraic Methods Program. 106, 141–166 (2019)
Finger, M., Gabbay, D.M.: Adding a temporal dimension to a logic system. J. Logic Lang. Inf. 1(3), 203–233 (1992)
Găină, D., Ţuţu, I.: Birkhoff completeness for hybrid-dynamic first-order logic. In: Cerrito, S., Popescu, A. (eds.) TABLEAUX 2019. LNCS, vol. 11714, pp. 277–293. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29026-9_16
Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. J. ACM 39(1), 95–146 (1992)
Hennicker, R., Madeira, A., Knapp, A.: A hybrid dynamic logic for event/data-based systems. In: Hähnle, R., van der Aalst, W. (eds.) FASE 2019. LNCS, vol. 11424, pp. 79–97. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-16722-6_5
Latour, B.: Reassembling the Social: An Introduction to Actor-Network Theory. Oxford University Press, Oxford (2005)
Madeira, A., Barbosa, L.S., Hennicker, R., Martins, M.A.: A logic for the stepwise development of reactive systems. Theor. Comput. Sci. 744, 78–96 (2018)
Martins, M.A., Madeira, A., Diaconescu, R., Barbosa, L.S.: Hybridization of institutions. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 283–297. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22944-2_20
Mateus, P., Sernadas, A., Sernadas, C.: Exogenous semantics approach to enriching logics. In: Essays on the Foundations of Mathematics and Logic. Advanced Studies in Mathematics and Logic, vol. 1, pp. 165–194. Polimetrica (2005)
Moon-Miklaucic, C., Bray-Sharpin, A., de la Lanza, I., Khan, A., Re, L.L., Maassen, A.: The evolution of bike sharing: 10 questions on the emergence of new technologies, opportunities, and risks. Technical report. World Resources Institute, Washington, DC (2019). http://www.wri.org/publication/evolution-bike-sharing
Mossakowski, T., Maeder, C., Lüttich, K.: The heterogeneous tool set (Hets). In: Proceedings of 4th International Verification Workshop in connection with CADE-21, vol. vol. 259. CEUR-WS.org (2007)
Pavlovic, D., Meadows, C.: Actor-network procedures (extended abstract). In: Ramanujam, R., Ramaswamy, S. (eds.) ICDCIT 2012. LNCS, vol. 7154, pp. 7–26. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28073-3_2
Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2–3), 91–110 (2002)
Sannella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-17336-3
Shanahan, M.: Solving the Frame Problem – A Mathematical Investigation of the Common Sense Law of Inertia. MIT Press, Cambridge (1997)
Ţuţu, I., Chiriţă, C., Lopes, A., Fiadeiro, J.: A hybrid-logic specification of a BSS. Ontohub (2019). https://ontohub.org/forver/BSS.dol
Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 140–145. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_10
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Ţuţu, I., Chiriţă, C.E., Lopes, A., Fiadeiro, J.L. (2019). Logical Support for Bike-Sharing System Design. In: ter Beek, M., Fantechi, A., Semini, L. (eds) From Software Engineering to Formal Methods and Tools, and Back. Lecture Notes in Computer Science(), vol 11865. Springer, Cham. https://doi.org/10.1007/978-3-030-30985-5_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-30985-5_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-30984-8
Online ISBN: 978-3-030-30985-5
eBook Packages: Computer ScienceComputer Science (R0)