
R. Berghammer, H. Hitoshi, W. Guttmann, P. Höfner:
Relational Characterisations of Paths. In Journal of Logic and Algebraic Methods in Programming 117, Elsevier, 2020.
arXiv: CoRR abs/1801.04026  doi: 10.1016/j.jlamp.2020.100590
abstract  pdf  bibtex
Abstract:
Binary relations are one of the standard ways to encode, characterise and reason about graphs. Relation algebras provide equational axioms for a large fragment of the calculus of binary relations. Although relations are standard tools in many areas of mathematics and computing, researchers usually fall back to pointwise reasoning when it comes to arguments about paths in a graph. We present a purely algebraic way to specify different kinds of paths in relation algebras. We study the relationship between paths with a designated root vertex and paths without such a vertex. Since we stay in firstorder logic this development helps with mechanising proofs. To demonstrate the applicability of the algebraic framework we verify the correctness of three basic graph algorithms. All results of this paper are formally verified using Isabelle/HOL.
@article{Hoefner20203,
Author = {Berghammer, R. and Hitoshi, H. and Guttmann, W. and H{\"o}fner, P.},
Title = {Relational Characterisations of Paths},
Journal = {Journal of Logic and Algebraic Methods in Programming},
Volume = {117},
Year = {2020},
Publisher = {Elsevier},
Doi = {10.1016/j.jlamp.2020.100590}
}

J. Drury, P. Höfner, W. Wang:
Formal Models of the OSPF Routing Protocol. In A. Fehnker, H. Garaval (eds.), Models for Formal Analysis of Real Systems (MARS 2020). Electronic Proceedings in Theoretical Computer Science 316, pp. 72120, Open Publishing Association, 2020.
doi: 10.4204/EPTCS.316.4
abstract  pdf  bibtex
Abstract:
We present three formal models of the OSPF routing protocol. The first two are formalised in the timed process algebra TAWN, which is not only tailored for routing protocols, but also specifies protocols in pseudocode that is easily readable. The difference between the two models lies in the level of detail (level of abstraction). From the more abstract model we then generate the third model. It is based on networks of timed automata and can be executed in the model checker Uppaal.
@InProceedings{Hoefner20202,
Author = {Drury, J. and H{\"o}fner, P. and Wang, W.},
Title = {Formal Models of the {OSPF} Routing Protocol},
BookTitle = {Models for Formal Analysis of Real Systems (MARS 2020)},
Editor = {Fehnker, A. and Garaval, H.},
Series = {Electronic Proceedings in Theoretical Computer Science},
Volume = {316},
Pages = {72120},
Year = {2020},
Publisher = {Open Publishing Association},
Doi = {10.4204/EPTCS.316.4}
}

R. Barry, R.J. van Glabbeek, P. Höfner:
Formalising the Optimised Link State Routing Protocol. In A. Fehnker, H. Garaval (eds.), Models for Formal Analysis of Real Systems (MARS 2020). Electronic Proceedings in Theoretical Computer Science 316, pp. 4071, Open Publishing Association, 2020.
doi: 10.4204/EPTCS.316.3
abstract  pdf  bibtex
Abstract:
Routing protocol specifications are traditionally written in plain English. Often this yields ambiguities, inaccuracies or even contradictions. Formal methods techniques, such as process algebras, avoid these problems, thus leading to more precise and verifiable descriptions of protocols. In this paper we use the timed process algebra TAWN for modelling the Optimised Link State Routing protocol (OLSR) version 2.
@InProceedings{Hoefner20201,
Author = {Barry, R. and van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {Formalising the Optimised Link State Routing Protocol},
BookTitle = {Models for Formal Analysis of Real Systems (MARS 2020)},
Editor = {Fehnker, A. and Garaval, H.},
Series = {Electronic Proceedings in Theoretical Computer Science},
Volume = {316},
Pages = {4071},
Year = {2020},
Publisher = {Open Publishing Association},
Doi = {10.4204/EPTCS.316.3}
}

R.J. van Glabbeek, P. Höfner:
Progress, Justness and Fairness. In ACM Computing Surveys 52(4):69:169:38, ACM, 2019.
arXiv: CoRR abs/1810.07414  doi: 10.1145/3329125
abstract  pdf  bibtex
Abstract:
Fairness assumptions are a valuable tool when reasoning about systems. In this paper, we classify several fairness properties found in the literature and argue that most of them are too restrictive for many applications. As an alternative we introduce the concept of justness.
@article{Hoefner20192,
Author = {van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {Progress, Justness and Fairness},
Journal = {ACM Computing Surveys},
Number = {4},
Volume = {52},
Pages = {69:169:38},
Year = {2019},
Publisher = {ACM},
Doi = {10.1145/3329125}
}

R.J. van Glabbeek, P. Höfner, M. Markl:
A Process Algebra for Link Layer Protocols. In L. Caires (ed.), Programming Languages and Systems (ESOP 2019). Lecture Notes in Computer Science 11423, pp. 668693, Springer, 2019.
arXiv: CoRR abs/1907.13329  doi: 10.1007/9783030171841_24
abstract  pdf  bibtex
Abstract:
We propose a process algebra for link layer protocols, featuring a unique mechanism for modelling frame collisions. We also formalise suitable liveness properties for link layer protocols specified in this framework. To show applicability we model and analyse two versions of the CarrierSense Multiple Access with Collision Avoidance (CSMA/CA) protocol. Our analysis confirms the hidden station problem for the version without virtual carrier sensing. However, we show that the version with virtual carrier sensing not only overcomes this problem, but also the exposed station problem with probability 1. Yet the protocol cannot guarantee packet delivery, not even with probability 1.
@InProceedings{Hoefner20193,
Author = {van Glabbeek, R.J. and H{\"o}fner, P. and Markl, M.},
Title = {A Process Algebra for Link Layer Protocols},
BookTitle = {Programming Languages and Systems (ESOP 2019)},
Editor = {Caires, L.},
Series = {Lecture Notes in Computer Science},
Volume = {11423},
Pages = {668693},
Year = {2019},
Publisher = {Springer},
Doi = {10.1007/9783030171841_24}
}