面向资源的物联网系统形式化建模与验证

Formal Modeling and Verification of Resource-oriented Internet of Things Systems

物联网系统的实施涉及到感知、传输和应用三层结构,部署之前的测试和验证过程需要比传统软件系统更多的测试和检验成本,同时其质量问题也包含更多属性的权衡.为了在保障质量的前提下,尽量减少物联网系统部署之前的测试和检验成本,提出一种面向资源的物联网系统形式化建模与验证方法.按照应用场景的要求,在对服务进行分类的基础上,提出物联网服务的按需提供框架;基于面向资源的思想,提出面向资源的物联网服务模型;针对特定应用场景,使用进程代数的方法 CSP(通信顺序进程)对物联网系统进行建模,并利用PAT模型检测工具,分别对无死锁性、可达性等五种性质的满足性进行了相关验证.实验中对这些性质满足性的验证过程,为物联网服务部署前的测试和验证提供有效支持.

Implementing Interact of Things （IoT ） system involves in three layers which are the perceptual layer, the transportlayer and the application layer. The cost that the IoT systems are tested and verified before deployment is much more than traditionalsoftwares, and to weigh the problem of quality contains more attributes. In order to guarantee the quality and reduce the cost of testingand verifying IoT systems as far as possible, a kind of resource oriented formal modeling and verifying method of IoT systems wasproposed. According to the requirements of specific scenario,the offered framework of IoT services was put forward on the basis ofclassifying services. And based on the resource oriented idea, a model of resource oriented IoT services was presented. For this scenar-io, the process algebra method CSP （communicating sequential process } was used to model IoT systems, and the systems were verifiedvia making use of the model checking tool PAT to verify the five relevant properties, including deadlockf＇ree, reachability and so on.The experiments on these properties provide effective support for the test and verification before deployment of IoT systems.