Name
Abstract | ||
|---|---|---|
We propose an automated method for computing inductive invariants used to proving deadlock freedom of parametric component-based systems. The method generalizes the approach for computing structural trap invariants from bounded to parametric systems with general architectures. It symbolically extracts trap invariants from interaction formulae defining the system architecture. The paper presents the theoretical foundations of the method and proves its soundness. It also reports on a preliminary experimental evaluation on several textbook examples. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1016/j.jlamp.2020.100621 | Journal of Logical and Algebraic Methods in Programming |
Keywords | Field | DocType |
Parametric systems,Deadlock-freedom,Trap invariants,Interaction logic,Cardinality constraints,Quantifier elimination | Computer science,First order,Deadlock,Theoretical computer science,Parametric statistics,Invariant (mathematics),Systems architecture,Soundness,Monadic predicate calculus,Bounded function | Journal |
Volume | ISSN | Citations |
119 | 2352-2208 | 1 |
PageRank | References | Authors |
0.35 | 10 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marius Bozga | 1 | 2100 | 127.83 |
| Radu Iosif | 2 | 483 | 42.44 |
| Joseph Sifakis | 3 | 6064 | 814.75 |