
V. Dyseryn, R.J. van Glabbeek, P. Höfner:
Analysing Mutual Exclusion using Process Algebra with Signals. In K. Peters, T. Tini (eds.), Expressiveness in Concurrency and Structural Operational Semantics (EXPRESS/SOS 2017). Electronic Proceedings in Theoretical Computer Science 255, Open Publishing Association, 2017.
doi: 10.4204/EPTCS.255.2
abstract  pdf  bibtex
Abstract:
In contrast to common belief, the Calculus of Communicating Systems (CCS) and similar process algebras lack the expressive power to accurately capture mutual exclusion protocols without enriching the language with fairness assumptions. Adding a fairness assumption to implement a mutual exclusion protocol seems counterintuitive. We employ a signalling operator, which can be combined with CCS, or other process calculi, and show that this minimal extension is expressive enough to model mutual exclusion: we confirm the correctness of Peterson's mutual exclusion algorithm for two processes, as well as Lamport's bakery algorithm, under reasonable assumptions on the underlying memory model. The correctness of Peterson's algorithm for more than two processes requires stronger, less realistic assumptions on the underlying memory model.
@InProceedings{Hoefner20176,
Author = {Dyseryn, V. and van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {Analysing Mutual Exclusion using Process Algebra with Signals},
BookTitle = {Expressiveness in Concurrency and Structural Operational Semantics (EXPRESS/SOS 2017)},
Editor = {Peters, K. and Tini, T.},
Series = {Electronic Proceedings in Theoretical Computer Science},
Volume = {255},
Pages = {00},
Year = {2017},
Publisher = {Open Publishing Association},
Doi = {10.4204/EPTCS.255.2}
}

R.J. van Glabbeek, P. Höfner:
Split, Send, Reassemble: A Formal Specification of a CAN Bus Protocol Stack. In Models for Formal Analysis of Real Systems (MARS 2017). Electronic Proceedings in Theoretical Computer Science 244, pp. 1452, Open Publishing Association, 2017.
doi: 10.4204/EPTCS.244.2
abstract  pdf  bibtex
Abstract:
We present a formal model for a fragmentation and a reassembly protocol running on top of the standardised CAN bus, which is widely used in automotive and aerospace applications. Although the CAN bus comes with an inbuilt mechanism for prioritisation, we argue that this is not sufficient and provide another protocol to overcome this shortcoming.
@InProceedings{Hoefner20173,
Author = {van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {Split, Send, Reassemble: A Formal Specification of a CAN Bus Protocol Stack},
BookTitle = {Models for Formal Analysis of Real Systems (MARS 2017)},
Editor = {},
Series = {Electronic Proceedings in Theoretical Computer Science},
Volume = {244},
Pages = {1452},
Year = {2017},
Publisher = {Open Publishing Association},
Doi = {10.4204/EPTCS.244.2}
}

R. Berghammer, N. Danilenko, P. Höfner, I. Stucke:
Cardinality of Relations with Applications. In Discrete Mathematics 339(12):30893115, Elsevier, 2016.
doi: 10.1016/j.disc.2016.06.019
abstract  pdf  bibtex
Abstract:
Based on Y. Kawaharaâ€™s characterisation of the cardinality of relations we derive some fundamental properties of cardinalities concerning vectors, points and mappingrelated relations. As applications of these results we verify some properties of linear orders and graphs in a calculational manner. These include the cardinalities of rooted trees and some estimates concerning graph parameters. We also calculationally prove the result of D. Kőnig that in bipartite graphs the matching number equals the vertex cover number.
@article{Hoefner20169,
Author = {Berghammer, R. and Danilenko, N. and H{\"o}fner, P. and Stucke, I.},
Title = {Cardinality of Relations with Applications},
Journal = {Discrete Mathematics},
Number = {12},
Volume = {339},
Pages = {30893115},
Year = {2016},
Publisher = {Elsevier},
Doi = {10.1016/j.disc.2016.06.019}
}

E. Bres, R.J. van Glabbeek, P. Höfner:
A Timed Process Algebra for Wireless Networks with an Application in Routing (Extended Abstract). In Programming Languages and Systems (ESOP'16). Lecture Notes in Computer Science 9632, pp. 95122, Springer, 2016.
doi: 10.1007/9783662494981_5
abstract  pdf  bibtex
Abstract:
This paper proposes a timed process algebra for wireless networks, an extension of the Algebra for Wireless Networks. It combines treatments of local broadcast, conditional unicast and data structures, which are essential features for the modelling of network protocols. In this framework we model and analyse the Ad hoc OnDemand Distance Vector routing protocol, and show that, contrary to claims in the literature, it fails to be loop free. We also present boundary conditions for a fix ensuring that the resulting protocol is indeed loop free.
@InProceedings{Hoefner20167,
Author = {Bres, E. and van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {A Timed Process Algebra for Wireless Networks with an Application in Routing (Extended Abstract)},
BookTitle = {Programming Languages and Systems (ESOP'16)},
Editor = {},
Series = {Lecture Notes in Computer Science},
Volume = {9632},
Pages = {95122},
Year = {2016},
Publisher = {Springer},
Doi = {10.1007/9783662494981_5}
}

T. Bourke, R.J. van Glabbeek, P. Höfner:
Mechanizing a Process Algebra for Network Protocols. In Journal of Automated Reasoning 56(3):309341, Springer, 2016.
doi: 10.1007/s1081701593589
abstract  pdf  bibtex
Abstract:
This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invariant properties. Mechanizing the core process algebra in Isabelle/HOL is relatively standard, but its layered structure necessitates special treatment. The control states of reactive processes, such as nodes in a network, are modelled by terms of the process algebra. We propose a technique based on these terms to streamline proofs of inductive invariance. This is not sufficient, however, to state and prove invariants that relate states across multiple processes (entire networks). To this end, we propose a novel compositional technique for lifting global invariants stated at the level of individual nodes to networks of nodes.
@article{Hoefner20166,
Author = {Bourke, T. and van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {Mechanizing a Process Algebra for Network Protocols},
Journal = {Journal of Automated Reasoning},
Number = {3},
Volume = {56},
Pages = {309341},
Year = {2016},
Publisher = {Springer},
Doi = {10.1007/s1081701593589}
}