6533b820fe1ef96bd1279102

RESEARCH PRODUCT

Verification of Symbolic Distributed Protocols for Networked Embedded Devices

Gloria MartorellaDaniele PeriSalvatore GaglioA. AugelloGiuseppe Lo ReRosolino D'antoni

subject

Settore ING-INF/05 - Sistemi Di Elaborazione Delle InformazioniSymbolic programmingExecutable Code ExchangeSource codeCorrectnessbusiness.industryComputer scienceDistributed protocolSymbolic programmingmedia_common.quotation_subject020208 electrical & electronic engineering02 engineering and technologyResource (project management)Embedded system0202 electrical engineering electronic engineering information engineeringResource-constrained Device020201 artificial intelligence & image processingEmbedded SystemModeling and verificationDistributed applicationbusinessProtocol (object-oriented programming)media_commonAbstraction (linguistics)

description

The availability of versatile and interconnected embedded devices makes it possible to build low-cost networks with a large number of nodes running even complex applications and protocols in a distributed manner. Common tools used for modeling and verification, such as simulators, present some limitations as application correctness is checked off-board and only focuses on source code. Execution in the real network is thus excluded from the early stages of design and verification. In this paper, a system for modeling and verification of symbolic distributed protocols running on embedded devices is introduced. The underlying methodology is rooted in a symbolic programming paradigm that makes it possible to model protocols with a high level of abstraction still permitting their execution on resource-constrained devices. The preliminary experimental results shown in this paper concern verification of a distributed averaging protocol in a simulated network at increasing number of nodes. The results support the feasibility of the approach to test distributed applications running on large networks of resource- constrained nodes.

yearjournalcountryeditionlanguage
2020-09-01
10.1109/etfa46521.2020.9212134http://hdl.handle.net/10447/437998