Articles, chapters, papers, reports Department of Computer Science and Engineering

Permanent URI for this collectionhttps://gupea-staging.ub.gu.se/handle/2077/74181

Browse

Browsing Articles, chapters, papers, reports Department of Computer Science and Engineering by Author "De Nicola, Rocco"

Filter results by typing the first few letters
Now showing 1 - 4 of 4
  • No Thumbnail Available
    Item
    Automated replication of tuple spaces via static analysis
    (2022) De Nicola, Rocco; Di Stefano, Luca; Inverso, Omar; Uwimbabazi, Aline
    Coordination languages for tuple spaces can offer significant advantages in the specification and implementation of distributed systems, but often do require manual programming effort to ensure consistency. We propose an experimental technique for automated replication of tuple spaces in distributed systems. The system of interest is modelled as a concurrent Go program where different threads represent the behaviour of the separate components, each owning its own local tuple repository. We automatically transform the initial program by combining program transformation and static analysis, so that tuples are replicated depending on the components' read-write access patterns. In this way, we turn the initial system into a replicated one where the replication of tuples is automatically achieved, while avoiding unnecessary replication overhead. Custom static analyses may be plugged in easily in our prototype implementation. We see this as a first step towards developing a fully-fledged framework to support designers to quickly evaluate many classes of replication-based systems under different consistency levels.
  • No Thumbnail Available
    Item
    Intuitive Modelling and Formal Analysis of Collective Behaviour in Foraging Ants
    (2024) De Nicola, Rocco; Di Stefano, Luca; Inverso, Omar; Valiani, Serinella
    We demonstrate a novel methodology that integrates intuitive modelling, simulation, and formal verification of collective behaviour in biological systems. To that end, we consider the case of a colony of foraging ants, where, for the combined effect of known biological mechanisms such as stigmergic interaction, pheromone release, and path integration, the ants will progressively work out the shortest path to move back and forth between their nest and a hypothetical food repository. Starting from an informal description in natural language, we show how to devise intuitive specifications for such scenario in a formal language. We then make use of a prototype software tool to formally assess whether such specifications would indeed replicate the expected collective behaviour of the colony as a whole
  • No Thumbnail Available
    Item
    Modelling Flocks of Birds and Colonies of Ants from the Bottom Up
    (2023) De Nicola, Rocco; Di Stefano, Luca; Inverso, Omar; Valiani, Serenella
  • No Thumbnail Available
    Item
    Modelling Flocks of Birds from the Bottom Up
    (2022) De Nicola, Rocco; Di Stefano, Luca; Inverso, Omar; Valiani, Serenella
    We argue that compositional specification based on formal languages can facilitate the modelling of, and reasoning about, sophisticated collective behaviour in many natural systems. One defines a system in terms of individual components and local rules, so that collective behaviours emerge naturally from the combined effect of the different actions of the individual components. With appropriate linguistic constructs, this can yield compact and intuitive models that are easy to refine and extend in small incremental steps. In addition, automated workflows implemented on top of this methodology can provide quick feedback, thereby allowing rapid design iterations. To support our argument, we consider flocking, a well-known example of emergent behaviour in collective adaptive systems. We build a minimalistic bottom-up model of a flock of birds incrementally, discussing specific language constructs as we go along. We then describe a prototype simulator, and use it to validate our model in a controlled experiment, where a flock is attacked by a bird of prey. The flock effectively reacts to the attack by splitting into smaller groups and regathering once the threat subsides, consistently with both natural observations and previous models from the literature.