IoT applications are typically developed on serverless platforms and deployed for use with an underlying cloud service provider. Such applications typically use JSON files to represent sensor data and communicate with the IoT core using protocols like MQTT, MQTT-SN, AMQP, HTTP, etc. The main functionality of an IoT application is implemented on the serverless platform including synchronous and asynchronous computations on the sensor data, notification services, accessing databases, data streaming, etc. We provide a framework to verify the requirements of these IoT applications specified as assertions. Our framework extends the notion of asynchronous call graphs of serverless applications to IoT applications by including notations for communication protocols, their QoS features, and message-passing properties, modeling both synchronous and asynchronous computations and services that support notifications, sensor actuation, etc. We then use this framework to verify assertions corresponding to correctness properties of the IoT applications.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Reachability and Verification of Assertions for IoT Applications

  • S. R. Nagalakshmi,
  • Meenakshi D’Souza

摘要

IoT applications are typically developed on serverless platforms and deployed for use with an underlying cloud service provider. Such applications typically use JSON files to represent sensor data and communicate with the IoT core using protocols like MQTT, MQTT-SN, AMQP, HTTP, etc. The main functionality of an IoT application is implemented on the serverless platform including synchronous and asynchronous computations on the sensor data, notification services, accessing databases, data streaming, etc. We provide a framework to verify the requirements of these IoT applications specified as assertions. Our framework extends the notion of asynchronous call graphs of serverless applications to IoT applications by including notations for communication protocols, their QoS features, and message-passing properties, modeling both synchronous and asynchronous computations and services that support notifications, sensor actuation, etc. We then use this framework to verify assertions corresponding to correctness properties of the IoT applications.