Logical Support for Bike-Sharing System Design

Ionuţ Ţuţu (Lead / Corresponding author), Claudia Elena Chiriţă, Antónia Lopes, José Luiz Fiadeiro

Research output: Chapter in Book/Report/Conference proceedingChapter

3 Citations (Scopus)
204 Downloads (Pure)


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.

Original languageEnglish
Title of host publicationFrom Software Engineering to Formal Methods and Tools, and Back
Subtitle of host publicationEssays Dedicated to Stefania Gnesi on the Occasion of Her 65th Birthday
EditorsMaurice H. ter Beek, Alessandro Fantechi, Laura Semini
Place of PublicationSwitzerland
PublisherSpringer Verlag
Number of pages20
ISBN (Electronic)9783030309855
ISBN (Print)9783030309848
Publication statusPublished - 2019

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


  • artificial intelligence
  • computer architecture
  • formal logic
  • formal methods
  • formal model
  • formal verification
  • model checking
  • natural language processing
  • programming languages
  • requirements engineering
  • semantics
  • software engineering
  • software evaluation
  • software product lines
  • specifications
  • temporal logic
  • testing
  • theorem proving
  • theoretical computer science
  • verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Logical Support for Bike-Sharing System Design'. Together they form a unique fingerprint.

Cite this