物联网交互系统的量化验证方法研究

发布时间：2020-09-26 21:33

　　随着新一代网络技术和硬件设备的实现,物联网(Internet of Things)技术得到了空前地研究和发展,其应用也逐步进入市场化阶段,从智慧城市,野外考察工作站,到微型心率控制系统等。地球上的任何一个物体都可以成为物联网的组成部分,因此物联网的规模将会相当庞大,其实现难度以及交互机制的复杂性也会急剧增加。在设计层保证物联网应用的正确性成为关键和难点。本文从软件工程角度出发,根据“高内聚低耦合”的设计原则,将物联网各个组成单元抽象为具有接口的独立组件,侧重于组件之间通信交互的正确性、合理性,研究由此形成的物联网交互系统。人们通常从测试的角度研究一个系统的可执行性,但这样并不能保证该系统的正确性。本文使用形式化方法,针对物联网交互系统具有的特征进行建模,并从概率、时间、代价、数据流等非功能性需求方面对系统应满足的性质进行量化验证分析,从而保证系统运行的正确性。以此提供了一种对物联网交互系统进行分析验证的形式化方法。本文主要工作和创新点有以下四个方面:1.建立了物联网交互系统的形式化描述模型。针对物联网交互系统灵活多变的网络拓扑结构,以及以通信交互为主的特性,本文在Reo通信模型基础上扩展概率、时间、代价等方面的表达能力,提出物联网交互系统的形式化描述模型——Reo。进一步给出该模型的语义模型——pPTCA。人们可以很方便地通过描述模型对物联网交互系统进行建模,同时利用对应的语义模型进行相关的形式化验证分析。2.构建了物联网交互系统性质的逻辑表达系统。为了规范代价约束、概率性、时间性等物联网交互系统的特征,本文选取作为基础逻辑。考虑到物联网交互系统中资源的重要性以及通信交互的数据驱动性,在该逻辑上分别扩展数据流及代价行为的表达能力,构建了物联网交互系统性质的刻画逻辑——pPTDL。为了集成Modest工具进行自动化验证,本文研究了从pPTCA的反应式模型到支持动作集的随机时间自动机的转换机制,为该工具的使用提供了理论支撑。3.研究了物联网交互系统模型的互模拟等价。物联网交互系统规模的庞大必然导致形式化模型的复杂,这将给量化验证分析带来极大的困难。为了合理约减模型的规模,本文从是否考虑系统内部行为的角度,分别对强互模拟以及弱互模拟进行研究。针对强互模拟,本文研究具有概率、时间、代价等特征的约束自动机模型的行为等价。针对弱互模拟,本文侧重于概率模型,并考虑到发散行为(即无限内部行为)所带来的重要影响,从三个角度研究了保发散弱概率互模拟的相关理论以及对应的验证方法。通过结合归纳思想以及经典剖分精化方法,本文设计了计算最大保发散弱概率互模拟的多项式时间算法。4.介绍了偏远环境下独立工作的小型野外工作站物联网交互系统案例。通过应用本文提出的模型与逻辑,对该物联网交互系统进行建模并对其具有的性质进行逻辑规范,在此基础上完成量化验证与分析,从而表明了本文提出物联网交互系统量化验证方法的有效性。
【学位单位】：华东师范大学
【学位级别】：博士
【学位年份】：2019
【中图分类】：TP391.44;TN929.5
【文章目录】：
摘要
abstract
主要命名中英对照表
主要标号说明
主要符号索引
第一章绪论
    1.1 研究背景与动机
    1.2 研究现状与相关工作
    1.3 本文工作与主要创新点
    1.4 组织结构
    1.5 本章小结
第二章预备知识
    2.1 数学符号
    2.2 概率理论
    2.3 形式化模型Reo
    2.4 约束自动机理论
    2.5 时态逻辑
    2.6 本章小结
第三章物联网交互系统模型
    3.1 引言
    3.2 代价概率时间Reo模型
    3.3 代价概率时间约束自动机
    3.4 代价概率时间约束自动机语义
        3.4.1 概率时间系统
        3.4.2 自动机语义
    3.5 本章小结
第四章物联网交互系统性质规范
    4.1 代价概率时间数据流逻辑
    4.2 代价概率时间数据流逻辑解释
        4.2.1 逻辑解释
        4.2.2 模型性质可满足性
        4.2.3 逻辑表达能力分析
        4.2.4 一体化还是组合化的逻辑依据
    4.3 工具自动化验证
        4.3.1 pPTCA的简化模型
        4.3.2 支持动作集的STA模型
        4.3.3 spPTCA到MSTA的转换
    4.4 本章小结
第五章模型行为等价研究
    5.1 强互摸拟研究
        5.1.1 经典强互模拟
        5.1.2 代价约束的强互摸拟
        5.1.3 代价约束的强概率互模拟
    5.2 弱互摸拟研究
        5.2.1 概率模型
        5.2.2 经典弱概率互模拟
        5.2.3 定性保发散弱互摸拟
        5.2.4 定性保等价发散弱互模拟
        5.2.5 定量保发散弱互模拟
        5.2.6 概率系统与非概率系统一致性
    5.3 最大保发散弱互模拟的计算算法
        5.3.1 定性保等价发散弱互模拟的判定算法
        5.3.2 最大定性保等价发散弱互模拟的计算算法
    5.4 本章小结
第六章应用案例分析
    6.1 野外工作站物联网交互系统建模
        6.1.1 物理场景需求分析
        6.1.2 物联网交互系统建模
    6.2 野外工作站物联网交互系统性质分析
        6.2.1 升级前的系统
        6.2.2 升级后的系统
    6.3 本章小结
第七章总结与展望
    7.1 本文工作总结
    7.2 后续工作展望
参考文献
致谢
发表论文和科研情况

【参考文献】