摘要:

摘要:互模拟是并发系统分析和验证的一个重要概念.主要扩展了一种由Du和Deng提出的准局部算法，使其更加适用于一般的标记迁移系统.用Java实现扩展后的准局部算法与Fernandez和Mounier提出的局部算法.以VLTS为实验数据基准进行大量的实验，发现在大多数情况下，前者的性能比后者更好.同时，修改了算法使其能够验证模拟关系.最后，用Java实现对标记迁移系统进行转换，使算法同时可以验证弱互模拟关系.

摘要:提出了一种对递归数据结构的归纳性质进行自动化分析的框架.工作分为3个主要部分.首先，它将递归数据结构的归纳性质分为两个主要类别，并提出对应的处理模式，从而帮助简化对于程序中的递归数据结构上的相关性质的分析.其次，提出了一种称为分割与拼接的技术来发现和描述递归数据结构是如何被程序修改的：递归数据结构首先被分割为若干个互不相交的片段，然后，这些片段以新的方式重新拼接在一起，形成一个新的数据结构.这个技术的重点在于如何将程序原有的性质保留下来，从而为后面的分析过程所使用.最后，提出了一种调用上下文敏感的程序摘要过程间分析方法.案例分析和实验结果表明：分析框架可以有效地分析递归数据结构的归纳性质，并生成对程序证明过程有用的断言.

摘要:提出了基于抽象解释框架自动合成数组程序不变式的方法，它能够分析按照特定顺序访问一维或者多维数组的程序，然后合成不变式.该方法将性质（包括区间全称量词性质和原子性质）集合作为抽象域，通过前向迭代数据流分析合成数组性质.证明了该方法的正确性和收敛性，并通过一些实例展示了该方法的灵活性.开发了一种原型工具，该工具在各种数组程序（包括competition on software verification中的array-examples benchmark）上的实验展示了方法的可行性和有效性.

摘要:Petri网是形式化验证领域最重要的模型之一，具有重要的理论和应用价值.从验证算法分析的角度，Petri网可以被等价地抽象为向量加法系统.在对向量加法模型的研究中，人们又发展了一些重要的扩展模型.对近些年来国内外学者在向量加法系统验证领域取得的成果进行了系统总结.首先给出了向量加法系统及几个关键验证问题的形式化定义，并重点总结了一般向量加法系统模型上可达性问题的最新研究进展和关键技术；接着总结了当限定模型的维度为固定值时相关研究进展，重点给出了2维情况的核心定理；随后介绍了几个重要扩展模型，并总结了这些模型上验证问题研究的最新进展.在每一部分，都对未来研究方向及可能面临的挑战进行了展望.

摘要:模型检查作为一种自动化系统验证方法，已被应用于多智能体系统的验证.由此延伸出的规约描述语言——交替时态逻辑（ATL），也被给予了高度关注.根据智能体是否可以看到全局信息，分为不完全信息和完全信息；根据智能体是否可以记录历史信息，分为无记忆能力和无限记忆能力，提出了4种经典的策略类型.这些策略类型是通过ATL的语义进行刻画的.然而在一个多智能体系统中，考虑完全信息和无限记忆能力时，所有智能体都只能选择这一种策略类型；在考虑不完全信息或无记忆能力时，仅在联合模态操作<<A>>φ和[[A]]φ的A里出现的智能体具备这种策略类型，而其他智能体还是完全信息和无限记忆能力策略类型.这可能会导致嵌套联合模态操作中智能体策略类型的不一致，且智能体策略类型取决于逻辑公式和逻辑的语义.而在实际多智能体系统中，智能体的策略类型往往取决于系统本身，且不同智能体具有不同的策略类型，即，智能体策略类型是异构的，这种多智能体系统被称为异构多智能体系统.针对这些问题，提出了一种在语法层对智能体策略类型进行刻画的系统模型——带类型解释系统.带类型解释系统在已有的解释系统中为每个智能体引入策略类型这一属性，允许不同智能体具备不同的策略类型.带类型解释系统可用于异构多智能体系统的建模.针对提出的系统模型，对ATL语义进行了研究，设计了ATL模型检查算法，实现了相应的模型检查工具ShTMC.

摘要:时钟约束语言CCSL是一种用于描述实时嵌入式系统中事件之间约束的形式化语言，它是UML针对实时嵌入式系统建模的扩展包MARTE （modeling and analysis of real-time and embedded systems）中用于对时间建模的一个子语言.给定一组由CCSL定义的时钟约束条件，需要判断是否存在某种调度策略满足约束、是否所有满足这些约束的行为都不会导致系统死锁等分析.目前已经有一定的针对CCSL的形式化分析研究工作，如基于状态迁移系统与时间自动机的方法等.但这些方法要么只针对某种特定的分析，要么只适用于部分CCSL约束，要么分析效率较低.提出了基于SMT的统一且高效的CCSL形式化分析方法.统一性体现在其可用于有效性证明、迹分析、死锁检测、LTL模型检测等方面的验证与分析.基于该方法开发了原型工具，同时支持上述4种验证功能.工具集成了当前最高效的SMT求解器Z3和CVC4.得益于SMT求解器的高效性，实验中大部分的验证可以在短时间内完成.

摘要:建模、仿真和验证语言（MSVL）是一种时序逻辑编程语言，它是投影时序逻辑（PTL）的可执行子集.MSVL和PTL可用于并发系统的建模和性质验证.然而，MSVL缺少一种消息传递的通信机制，这种机制对于并发分布式系统的建模和验证至关重要.说明了如何在MSVL中开发和实现合适的机制来对分布式系统进行建模和验证.该机制首先定义了通道结构，对通信语句和进程结构进行形式化描述；接着介绍了这些通信语句的实现机制；最后提供了一个关于电子合同签名协议的建模和验证实例，说明消息传递在MSVL中的工作原理.

摘要:运行时验证是提升普适计算应用可靠性的重要手段.这类应用的很多性质同时涉及时间关系和空间位置关系，这样的时空性质给运行时的验证带来了特有挑战：一方面，传统的时态逻辑难以描述空间性质；另一方面，适合描述空间性质的Ambient Logic在真值不确定等情况下不能很好地支持有限轨迹中时间性质的描述.为支持普适计算应用时空性质的运行时验证，引入三值逻辑语义，提出了AL₃（3-valued ambient logic）；并在此基础上设计实现了基于AL₃的性质检验算法和运行时监控器.最后，通过案例分析和运行效率实验阐明了所提方法的有效性和可行性.

摘要:交替投影时序逻辑（alternating projection temporal logic，简称APTL）公式简单易懂，表达能力强；不仅可以描述经典时序逻辑LTL可以描述的性质，而且可以描述与区间相关的顺序和循环性质以及开放系统和多智能体系统中与博弈相关的性质.在验证系统是否满足所给的APTL公式所描述的性质之前需要检查公式的可满足性.根据检查APTL公式的可满足性的方法，开发实现了工具APTL2BCG.具体细节如下：首先，利用公式P的范式构造P的标记范式图（labeled normal form graph，简称LNFG）；然后，将LNFG转化为广义的基于并发博弈结构的交替Büchi自动机（generalized alternating Büchi automaton over concurrent game structure，简称GBCG）；最后，将GBCG转化为基于并发博弈结构的交替Büchi自动机（alternating Büchi automaton over concurrent game structure，简称BCG）并且化为最简形式并检查公式P的可满足性.

摘要:数据作为软件系统的主要处理对象，其规范性有助于软件系统的设计开发和软件系统之间的数据交换.面向行业数据规范及其验证，提出了一种基于类型理论的领域数据建模语言（DDML）和领域建模方法（DDMM）.DDML语言通过定义类型和项的语法和语义，描述领域数据类型和对象的结构，通过定义类型规则及其类型检查算法判定任意项t：T?.DDMM给出了领域数据建模的方法，即构建κ₁（原子类型）、κ₂（数据元）、κ₃（数据元目录）三层框架，生成表示κ₃层数据元目录之间关系的类型规则.在此基础上，给出了数据元目录序列的定义及其正确性判定算法.基于上述方法，实现了一种领域数据建模工具原型系统，并通过领域数据建模与自动验证的一个实际案例，完成了一个较大规模行业数据规范的制定与验证.

摘要:在嵌入式系统和各类操作系统中，中断机制是确保实时响应各类异步事件的重要方法.通常在处理一个中断事件的过程中，往往会有更紧迫的中断事件请求响应，因而发生中断嵌套.建模并验证嵌套中断系统是具有挑战性的工作.提出一种建模和验证嵌套中断系统的方法.首先，提出基于投影时序逻辑（projection temporal logic，简称PTL）的定义，并将这种定义推广到包含任意多中断事件的中断系统上，从而得出嵌套中断系统基于投影时序逻辑的形式化模型；其次，使用投影时序逻辑定义的基本中断语句扩充建模仿真和验证语言（modeling，simulation andverification language，简称MSVL），并扩展MSVL语言的解释器，使其可以对嵌套中断系统进行建模仿真和验证；最后，通过一个实例展现所提出方法的正确性和实用性.

摘要:实时嵌入式系统多采用中断和上下文切换实现多任务间调度，在对此类系统进行可调度性分析时，在任务的最差响应时间计算中必须包含中断和上下文切换开销.现有包含这些开销的方法是将中断作为高优先级任务，同时将上下文切换开销加入到任务最差执行时间中进行分析，然而这些方法过于粗略，缺乏对实际系统细节的考虑，计算得到的最差响应时间并不精确.首先，对中断和上下文切换的机制和时间流程进行详细的阐述，进而分析中断和上下文切换对任务关键性时刻的影响；接着，给出包含上述开销的更加精确的响应时间计算方法；最后进行仿真验证.扩展了包含系统调度开销的响应时间计算方法，可用于资源受限的硬实时系统中需要精确计算响应时间的场合.

摘要:高速串行现场总线（controller area network，简称CAN）被广泛部署到机器人通信系统中.而服务机器人任务具有并发性和高实时性的特点，因此，如何根据总线协议规范和应用需求精化设计模型，保证系统设计的正确性和实时性要求，避免设计阶段的漏洞十分必要.针对传统方法的局限性，提出使用形式化方法对基于CAN现场总线型控制系统进行建模分析.首先，对系统进行模型抽象和形式表达；其次进行形式建模和自动验证，在UPPAAL中实现主控制器、关节控制器、收发器、仲裁器和CAN总线的时间自动机模型；最后对机器人通信系统进行正确性验证和实时性分析.实时性分析发现：随着总线上关节节点数的增多，低优先级节点的最坏仲裁时延的增长速率加大.针对这个问题，在形式模型中加入了改进的动态优先级策略.实验结果表明：部署动态优先级策略后不仅减小了低优先级节点的仲裁时延，而且还可以加大CAN总线的节点负载量，为系统设计提供有效的指导和参考.

摘要:API （application programming interface，应用程序编程接口）在现代软件开发过程中被广泛使用.开发人员通过调用API快速构建项目，节省了大量的时间.但由于API数量众多、文档不够完善、维护更新不及时等原因，开发人员在学习使用API的过程中面临着严峻的挑战.一旦API使用不正确，程序可能会出现缺陷甚至严重的安全问题.通过对API相关文献的深入调研，对近些年来国内外学者在该研究领域取得的成果进行了系统总结.首先，介绍了API的基本概念并分析出影响API使用的3个关键问题：API文档质量不高、调用规约不完整以及API调用序列难以确定；接着，从API文档、调用规约和API推荐这3个主要方面对研究成果进行全面的分析；最后，对未来研究可能面临的挑战进行了展望.

摘要:用户为使用服务组合提供的功能，需要提供必要的个人隐私数据.由于组合的业务逻辑对用户是透明的，且用户与成员服务之间缺乏隐私数据使用的相关协议，如何保证组合执行过程中不发生用户隐私信息的非法泄露，成为当前服务计算领域的研究热点之一.针对隐私保护特征，提出一种服务组合安全隐私信息流静态分析方法.首先，从服务信誉度、隐私数据使用目的及保留期限这3个维度提出一种面向服务组合的隐私信息流安全模型；其次，采用支持隐私信息流分析的隐私工作流网（privacy workflow net，简称PWF-net）构建服务组合模型，并通过静态分析算法分析组合执行路径，检测组合的执行是否会发生用户隐私信息的非法泄露；最后，通过实例分析说明了方法的有效性，并对方法性能进行了实验分析.与现有的相关工作相比，针对隐私保护特征提出了隐私信息流安全模型，且分析方法考虑了隐私数据项聚合问题，从而能够更为有效地防止用户隐私信息非法泄露.

摘要:缺陷定位是软件调试的重要阶段，依赖程序频谱信息实现软件缺陷定位，是当前比较行之有效的方法.基于频谱缺陷定位方法应用的前提是，程序频谱和执行结果之间存在的潜在关联.通过经验性分析两者之间的内在关联，借助于统计学的条件概率思想，构建了用以量化分析两者关系强弱的P模型，并基于此提出了基于条件概率的缺陷定位方法.以Siemens套件中的7个程序、Space程序和3个Unix工具程序为基准评测对象，与已有的15种经典缺陷定位方法进行了对比实验.实证研究结果表明，该方法总体上具有更好的缺陷定位效果.

摘要:评述了MapReduce与Spark两种大数据计算算法和架构，从背景、原理以及应用场景进行分析和比较，并对两种算法各自优点以及相应的限制做出了总结.当处理非迭代问题时，MapReduce凭借其自身的任务调度策略和shuffle机制，在中间数据传输数量以及文件数目方面的性能要优于Spark；而在处理迭代问题和一些低延迟问题时，Spark可以根据数据之间的依赖关系对任务进行更合理的划分，相较于MapReduce，有效地减少了中间数据传输数量与同步次数，提高了系统的运行效率.

摘要:子图匹配是图论中最基本的操作.研究子图匹配的一个变种，即：在一个节点拥有若干元素的大图数据库中，找到与给定查询图结构同构并且对应节点元素的加权集合包含度大于给定值的所有子图，称作基于包含度的子图匹配（subgraph matching with inclusion degree，简称SMID）.该查询能够应用于多种场景，包括论文检索、社区发现、企业招聘等.为高效实现SMID，设计了同时包含节点元素和图结构信息的数据签名与查询签名，在离线处理阶段，利用数据签名为数据图建立动态签名树（DS-Tree），以加快在线处理时图节点的匹配过程.为解决DS-Tree占用空间大的问题，设计了一种DS-Tree压缩方法，在对查询效率影响不大的情况下减小了索引空间.为进一步加快查询效率，还提出了支配子图查询算法.在真实数据和人工数据上的实验结果表明，所提出的方法在效率和扩展性方面优于现有其他方法.

摘要:第五代（fifth gneration，简称5G）移动通信网络（简称5G网络或5G），是为构建网络型社会并实现万物互联的宏伟目标而提出的下一代移动网络.随着LTE等第四代移动通信网络进入规模化商用阶段，5G网络的研究已成为世界各国的关注焦点.5G网络的实现，需要依赖于系统架构和核心技术的变革与创新.目前，5G网络还处于技术和标准的初级研究阶段.5G网络的新架构、新业务、新技术对安全提出了新的挑战.简述了5G的性能指标、关键技术、应用场景及标准制定的进展，分析了5G网络的安全需求及其所面临的技术挑战.基于目前已有的研究工作和标准研制情况，提炼了5G安全框架，归纳并阐述了若干安全关键问题及其解决方案，展望了5G网络安全的未来研究方向.