nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Formal Verification of a Programmable Hypersurface

verfasst von : Panagiotis Kouvaros, Dimitrios Kouzapas, Anna Philippou, Julius Georgiou, Loukas Petrou, Andreas Pitsillides

Erschienen in: Formal Methods for Industrial Critical Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

A metasurface is a surface that consists of artificial material, called metamaterial, with configurable electromagnetic properties. This paper presents work in progress on the design and formal verification of a programmable metasurface, the Hypersurface, as part of the requirements of the VISORSURF research program (HORIZON 2020 FET-OPEN). The Hypersurface design is concerned with the development of a network of switch controllers that are responsible for configuring the metamaterial. The design of the Hypersurface, however, has demanding requirements that need to be delivered within a context of limited resources. This paper shares the experience of a rigorous design procedure for the Hypersurface network, that involves iterations between designing a network and its protocols and the formal evaluation of each design. Formal evaluation has provided results that, so far, drive the development team in a more robust design and overall aid in reducing the cost of the Hypersurface manufacturing.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Checking Consistency of Real-Time Requirements on Distributed Automotive Control Software Early in the Development Process Using UPPAAL

Nächstes Kapitel Modelling and Analysing ERTMS Hybrid Level 3 with the mCRL2 Toolset

VisorSurf: a hardware platform for software-driven functional metasurfaces. http://www.visorsurf.eu/

Benini, L., DeMicheli, G.: Networks on chips: a new SoC paradigm. IEEE Comput. 35(1), 70–78 (2002)CrossRef

Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. J. ACM 49(4), 538–576 (2002)MathSciNetCrossRef

Bloem, R., et al.: Decidability of Parameterized Verification. Morgan and Claypool Publishers, San Rafael (2015)

Bulychev, P.E., et al.: UPPAAL-SMC: statistical model checking for priced timed automata. In: Proceedings of QAPL 2012, vol. 85. EPTCS, pp. 1–16 (2012)

Chawade, S., Gaikwad, M., Patrikar, R.: Review of XY routing algorithm for network-on-chip architecture. Int. J. Comput. Appl. 43, 20–23 (2012)

Clarke, E., Talupur, M., Touili, T., Veith, H.: Verification by network decomposition. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 276–291. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28644-8_18CrossRef

Dal Corso, A., Macedonio, D., Merro, M.: Statistical model checking of Ad Hoc routing protocols in lossy grid networks. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 112–126. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9_9CrossRef

Dally, W.J., Towles, B.: Route packets, not wires: on-chip interconnection networks. In: Proceedings of DAC 2001, pp. 684–689. ACM (2001)

10.

Dombrowski, C., Junges, S., Katoen, J., Gross, J.: Model-checking assisted protocol design for ultra-reliable low-latency wireless networks. In: Proceedings of SRDS 2016, pp. 307–316. IEEE Computer Society (2016)

11.

Fehnker, A., van Glabbeek, R., Höfner, P., McIver, A., Portmann, M., Tan, W.L.: Automated analysis of AODV using UPPAAL. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 173–187. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28756-5_13CrossRefMATH

12.

Höfner, P., Kamali, M.: Quantitative analysis of AODV and its variants on dynamic topologies using statistical model checking. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 121–136. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40229-6_9CrossRef

13.

Höfner, P., McIver, A.: Statistical model checking of wireless mesh routing protocols. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 322–336. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38088-4_22CrossRef

14.

Kouvaros, P., Lomuscio, A.: Parameterised verification for multi-agent systems. Artif. Intell. 234, 152–189 (2016)MathSciNetCrossRef

15.

Li, M., Zeng, Q., Jone, W.: DyXY: a proximity congestion-aware deadlock-free dynamic routing method for network on chip. In: Proceedings of DAC 2006, pp. 849–852. ACM (2006)

16.

Maxemchuk, N.F.: Regular mesh topologies in local and metropolitan area networks. AT&T Tech. J. 64(7), 1659–1685 (1985)CrossRef

17.

Patooghy, A., Miremadi, S.: XYX: a power and performance efficient fault- tolerant routing algorithm for network on chip. In: Proceedings of PDP 2009, pp. 245–251. IEEE Computer Society (2009)

18.

Sen, K., Viswanathan, M., Agha, G.A.: VESTA: a statistical model-checker and analyzer for probabilistic systems. In: Proceedings of QEST 2005, pp. 251–252. IEEE Computer Society (2005)

19.

Wu, J.: A fault-tolerant and deadlock-free routing protocol in 2D meshes based on odd-even turn model. IEEE Trans. Comput. 52(9), 1154–1169 (2003)

20.

Younes, H.S.: Verification and planning for stochastic processes with asynchrounous events. Ph.D. thesis, Carnegie Mellon University (2004)

Titel: Formal Verification of a Programmable Hypersurface
verfasst von: Panagiotis Kouvaros
Dimitrios Kouzapas
Anna Philippou
Julius Georgiou
Loukas Petrou
Andreas Pitsillides
Verlag: Springer International Publishing
Buch: Formal Methods for Industrial Critical Systems
Print ISBN: 978-3-030-00243-5

Electronic ISBN: 978-3-030-00244-2

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-030-00244-2_6

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner