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 "Lang, Frédéric"

Filter results by typing the first few letters
Now showing 1 - 2 of 2
  • No Thumbnail Available
    Item
    Compositional Verification of Priority Systems Using Sharp Bisimulation
    (2023) Di Stefano, Luca; Lang, Frédéric
    Sharp bisimulation is a refinement of branching bisimulation, parame terized by a subset of the system’s actions, called strong actions. This parameterization allows the sharp bisimulation to be tailored by the property under verification, whichever property of the modal µ-calculus is considered, while potentially reducing more than strong bisimulation. Sharp bisimulation equivalence is a congruence for process algebraic oper ators such as parallel composition, hide, cut, and rename, and hence can be used in a compositional verification setting. In this paper, we prove that sharp bisimulation equivalence is also a congruence for action priority operators under some conditions on strong actions. We com pare sharp bisimulation with orthogonal bisimulation, whose equivalence is also a congruence for action priority. We show that, if the internal action τ neither gives priority to nor takes priority over other actions, then the quotient of a system with respect to sharp bisimulation equiv alence (called sharp minimization) cannot be larger than the quotient of the same system with respect to orthogonal bisimulation equivalence. We then describe a signature-based partition refinement algorithm for sharp minimization, implemented in the BCG_MIN and BCG_CMP tools of the CADP software toolbox. This algorithm can be adapted to implement orthogonal minimization. We show on a crafted exam ple that using compositional sharp minimization may yield state space reductions that outperform compositional orthogonal minimization by Verification of Priority Systems Using Sharp Bisimulation several orders of magnitude. Finally, we illustrate the use of sharp minimization and priority to verify a bully leader election algorithm.
  • No Thumbnail Available
    Item
    Compositional Verification of Stigmergic Collective System
    (2023) Di Stefano, Luca; Lang, Frédéric
    Collective adaptive systems may be broadly defined as en sembles of autonomous agents, whose interaction may lead to the emer gence of global features and patterns. Formal verification may provide strong guarantees about the emergence of these features, but may suffer from scalability issues caused by state space explosion. Compositional verification techniques, whereby the state space of a system is generated by combining (an abstraction of) those of its components, have shown to be a promising countermeasure to the state space explosion problem. Therefore, in this work we apply these techniques to the problem of verifying collective adaptive systems with stigmergic interaction. Specif ically, we automatically encode these systems into networks of LNT pro cesses, apply a static value analysis to prune the state space of individual agents, and then reuse compositional verification procedures provided by the CADP toolbox. We demonstrate the effectiveness of our approach by verifying a collection of representative systems.