A formal model for the analysis and verification of a pre-emptive round-robin arbiter Online publication date: Fri, 09-Nov-2018
by Imene Ben Hafaiedh; Maroua Ben Slimane; Riadh Robbana
International Journal of Critical Computer-Based Systems (IJCCBS), Vol. 8, No. 2, 2018
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.
Online publication date: Fri, 09-Nov-2018
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Critical Computer-Based Systems (IJCCBS):
Login with your Inderscience username and password:
Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.If you still need assistance, please email firstname.lastname@example.org