Controller synthesis for IoT protocols verification

Abstract

Almost every modern device or artifact can now send and/or receive information and data. This hyper connected modern era is commonly denominated Internet of Things (IoT). Software Engineering tools and techniques must be adapted to manage the new challenges and requirements that the emergent paradigm of IoT imposes, especially regarding to communications, interactions and protocols between those artifacts. In this work we focus on a very well known formal technique called Controller Synthesis, which features interesting characteristics to formally verify IoT systems. In particular, we specified and synthesized the behavior of a key protocol for IoT, the MQQT protocol, employing the FVS formal verification framework.