Show simple item record

dc.contributor.authorMirzaei, Saberen_US
dc.contributor.authorEsposito, Flavioen_US
dc.date.accessioned2017-03-15T14:45:40Z
dc.date.available2017-03-15T14:45:40Z
dc.date.issued2014-07-15
dc.identifier.citationMirzaei, Saber; Esposito, Flavio. "An alloy verification model for consensus-based auction protocols" Technical Report BU-CS-TR 2014-004, Computer Science Department, Boston University, July 15, 2014. [Available from: http://hdl.handle.net/2144/20812]
dc.identifier.urihttps://hdl.handle.net/2144/20812
dc.description.abstractMax Consensus-based Auction (MCA) protocols are an elegant approach to establish conflict-free distributed allocations in a wide range of network utility maximization problems. A set of agents independently bid on a set of items, and exchange their bids with their first hop-neighbors for a distributed (max-consensus) winner determination. The use of MCA protocols was proposed, e:g:, to solve the task allocation problem for a fleet of unmanned aerial vehicles, in smart grids, or in distributed virtual network management applications. Misconfigured or malicious agents participating in a MCA, or an incorrect instantiation of policies can lead to oscillations of the protocol, causing, e:g:, Service Level Agreement (SLA) violations. In this paper, we propose a formal, machine-readable, Max-Consensus Auction model, encoded in the Alloy lightweight modeling language. The model consists of a network of agents applying the MCA mechanisms, instantiated with potentially different policies, and a set of predicates to analyze its convergence properties. We were able to verify that MCA is not resilient against rebidding attacks, and that the protocol fails (to achieve a conflict-free resource allocation) for some specific combinations of policies. Our model can be used to verify, with a “push-button” analysis, the convergence of the MCA mechanism to a conflict-free allocation of a wide range of policy instantiations.en_US
dc.language.isoen_US
dc.publisherComputer Science Department, Boston Universityen_US
dc.relation.ispartofseriesBUCS Technical Reports;BUCS-TR-2014-004
dc.subjectMax Consensus-based Auction (MCA) modelen_US
dc.titleAn alloy verification model for consensus-based auction protocolsen_US
dc.typeTechnical Reporten_US


This item appears in the following Collection(s)

Show simple item record