HIBOU (for Holistic Interaction Behavioral Oracle Utility) provides utilities for designing, drawing & manipulating interaction models, explore their semantics and analyse outputs of distributed systems (sets of distributed logs) with regard to formal specifications written as interaction models.
This present version "hibou_label" treats labelled interaction models. A fork "hibou_efm" that treats interaction models enriched with data and time is also available.
This piece of software has been developed as part of my PhD thesis in 2018-2021 at the CentraleSupelec engineering school (part of Université Paris-Saclay) in collaboration with the CEA (Commissariat à l'énergie atomique et aux énergies alternatives).
Associated publications (in chronological order):
- "Revisiting Semantics of Interactions for Trace Validity Analysis"
- "A small-step approach to multi-trace checking against interactions"
- "Equivalence of Denotational and Operational Semantics for Interaction Languages"
- "Interaction-based Offline Runtime Verification of Distributed Systems" (best paper award)
- "Denotational and operational semantics for interaction languages: Application to trace analysis"
The theoretical background of this present tool has been checked with some automated proofs written in Coq:
- equivalence of three semantics for the base language
- syntactic equivalence relation between semantically equivalent interactions terms
- proof of correctness for the multi-trace analysis algorithm
- equivalence of two semantics for a language extended with concurrent regions
The convergence of rewrite systems used for computing simplified / canonical forms of interactions have been proven using dedicated tools:
(Multi-)Trace analysis:
- solving 3SAT problems wth HIBOU
- using a lifeline-removal operation to analyze partially observed multi-traces
- using simulation steps to analyze partially observed multi-traces
Translations and model synthesis:
- benchmarking the automated synthesis of Non-deterministic Finite Automata (NFA) from interactions
- NFA synthesis on some concrete use cases
- exploiting NFA synthesized from interactions for trace analysis
A README (not up-to-date) can be accessed here.