Reachability and Verification of Assertions for IoT Applications
摘要
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.