BigraphTalk: Verification Design of IoT Applications

Archibald Blair, Min-Zheng Shieh*, Yu-Hsuan Hu, Sevegnani Michele, Yi-Bing Lin

*Corresponding author for this work

    Research output: Contribution to journalArticlepeer-review

    4 Scopus citations


    Graphical IoT device management platforms, such as IoTtalk, make it easy to describe interactions between IoT devices. Applications are defined by dragging-and-dropping devices and specifying how they are connected, e.g. a door sensor controlling a light. While this allows simple and rapid development, it remains possible to specify unwanted device configurations – such as using the same device to drive a motor up and down simultaneously, risking damaging the motor. We propose BigraphTalk, a verification framework for IoTtalk that utilizes formal techniques, based on bigraphs, to statically guarantee that unwanted configurations do not arise. In particular, we check for invalid connections between devices, as well as type errors, e.g. passing a float to a boolean switch. To the best of our knowledge, BigraphTalk is the first platform to support the graphical specification of correct-by-design IoT applications. BigraphTalk provides fully automated verification and feedback without end-users ever needing to specify a bigraph. This means any application, specifiable in IoTtalk, is guaranteed, so long as verification succeeds, not to violate the given configuration constraints when deployed; with no extra cost to the user.
    Original languageEnglish
    Pages (from-to)2955-2967
    Number of pages13
    JournalIEEE Internet of Things Journal
    Issue number4
    StatePublished - Apr 2020


    • Application platform
    • bigraphs
    • device management
    • model verification


    Dive into the research topics of 'BigraphTalk: Verification Design of IoT Applications'. Together they form a unique fingerprint.

    Cite this