Kourtis, G, Dixon, C 
ORCID: 0000-0002-4610-9533, Fisher, M and Lisitsa, A
(2021)
Parameterized verification of leader/follower systems via first-order temporal logic.
FORMAL METHODS IN SYSTEM DESIGN, 58 (3).
pp. 440-468.
Abstract
<jats:title>Abstract</jats:title><jats:p>We introduce a framework for the verification of protocols involving a distinguished machine (referred to as a leader) orchestrating the operation of an arbitrary number of identical machines (referred to as followers) in a network. At the core of our framework is a high-level formalism capturing the operation of these types of machines together with their network interactions. We show that this formalism automatically translates to a tractable form of first-order temporal logic. Checking whether a protocol specified in our formalism satisfies a desired property (expressible in temporal logic) then amounts to checking whether the protocol’s translation in first-order temporal logic entails that property. Many different types of protocols used in practice, such as cache coherence, atomic commitment, consensus, and synchronization protocols, fit within our framework. First-order temporal logic also facilitates parameterized verification by enabling us to model such protocols abstractly without referring to individual machines.</jats:p>
| Item Type: | Article |
|---|---|
| Uncontrolled Keywords: | Parameterized verification, First-order logic, Temporal logic |
| Divisions: | Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 26 May 2022 15:52 |
| Last Modified: | 18 Jan 2023 21:00 |
| DOI: | 10.1007/s10703-022-00390-y |
| Open Access URL: | https://link.springer.com/article/10.1007/s10703-0... |
| Related URLs: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3155544 |
Dimensions
Dimensions
