摘要
在时间自动机理论的基础上,提出一种物联网组合服务建模的方法,来对系统的部分约定属性进行建模、验证和分析。把物联网原子服务作为研究的对象,对时间自动机模型进行扩展,并将其应用于物联网原子服务和组合服务的分层建模中。在分析不同层所对应实体的部分特定属性之后,通过工具UPPAAL建立模型并对该模型进行验证和分析。利用提出的方法对智能室温自控系统进行建模并验证,通过实验验证了该方法的可行性。
A method on composite service modeling for internet of things based on timed automata was proposed,to verify system’s regular properties and specify formal model for internet of things.Atomic service was taken as study object,the mode for timed automata was extended,they were combined with composite service and applied to hierarchical modeling for internet of things,and the model checking tool UPPAAL was used to verify and analyze the specific attributes of corresponding entities by hierarchical modeling for internet of things.The proposed research method can be applied to actual modeling and verification of intelligent home temperature control system.Experimental results show that the proposed method has better practical feasibility.
作者
王曦
李培培
欧阳城添
WANG Xi;LI Pei-pei;OUYANG Cheng-tian(School of Information Engineering,Jiangxi University of Science and Technology,Ganzhou 341000,China)
出处
《计算机工程与设计》
北大核心
2019年第1期20-25,31,共7页
Computer Engineering and Design
基金
国家自然科学基金项目(61462034
61561024
11461031
61562037)
江西省自然科学基金项目(20151BAB207035)
江西省教育厅科学技术研究基金项目(GJJ160632
GJJ170517)
江西理工大学科研基金重点课题基金项目(NSFJ2014-K11)
关键词
时间自动机
物联网
组合服务
建模
验证
timed automata
internet of things
composite service
modeling
verification
