Title: A formal model for the analysis and verification of a pre-emptive round-robin arbiter

Authors: Imene Ben Hafaiedh; Maroua Ben Slimane; Riadh Robbana

Addresses: Institut Supérieur d'Informatique (ISI), Université de Tunis El Manar (UTM), Tunis, Tunisia ' Ecole Polytechnique de Tunisie (EPT), Université de Carthage (UC), La Marsa, Tunisia ' INSAT, Université de Carthage (UC), Sidi Bou Said, Avenue de la République, Carthage 1054, Tunisia

Abstract: Resource arbitration is a fundamental problem in communication and computing system design. Thus, a fast and efficient arbitration algorithm is one of the most dominant factors for high performance networks-on-chip (NoCs) and ensuring their reliability and performance is highly required. In this context, we propose, a formal model for the analysis and validation of the round-robin protocol, considered as the most widely adopted scheduling algorithm, in particular for real-time applications. The contribution of this paper is first to propose a high-level formal, distributed and scalable model for round-robin arbiter based on the formalism of timed automata. We then employ model checking, to verify a set of relevant properties of the round-robin protocol such as deadlock freedom and invariant. In order to evaluate the efficiency and the scalability of the protocol under study, a set of experimental results are presented based on an automatically generated code of our proposed model.

Keywords: bus arbitration; round-robin; multiprocessor system-on-a-chips; MPSoCs; formal verification; deadlock-freedom; timing constraints.

DOI: 10.1504/IJCCBS.2018.096193

International Journal of Critical Computer-Based Systems, 2018 Vol.8 No.2, pp.169 - 192

Received: 11 Sep 2017
Accepted: 15 Aug 2018
Published online: 15 Nov 2018 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article