hiralysis

 

Subproject

S2

Categories

Model reduction

Overview

hiralysis computes abstract graph transformation: Graphs of infinite size (that is, graphs with an infinite number of nodes and possibly edges) are abstracted using a finite over-approximation and user-specified graph transformation rules (that replace subgraphs by other subgraphs), that may additionally be restricted by negative application conditions, are applied on this abstract representation. The tool has been written with topology analysis of DCS protocols in mind. hiralysis uses the partner abstraction method.

Publications

J. Bauer and R. Wilhelm. Static analysis of dynamic communication systems by partner abstraction. In Gilberto Filé and Hanne Riis Nielson, editors, Static Analysis Symposium, Springer LNCS, 2007.

Benchmarks

Car Platooning

Download

---

Manual

---

Status

---