摘要:形式化方法以严格的数学化和机械化方法为基础来规约、设计、构建、验证、演进计算系统,是改善和确保计算系统质量的重要方法,其模型、技术和工具已延伸成为计算思维的重要载体,在国内外持续被关注和研究.在各种领域需求的推动下,形式化方法的相关理论、技术和工具越来越受重视,并在多种关键领域的应用中取得显著成效. 本专刊主要关注国内形式化方法的最新研究进展及其在特定领域的应用,共征得投稿37篇,其中36篇通过特约编辑形式审查进入到评审阶段.每篇稿件经过2位专家的评审,有16篇进入到复审阶段并在第一届全国形式化方法与应用会议（FMAC 2016）上宣读,最后有13篇文章通过终审被收录到本专刊.

摘要:采用形式化方法证明软件的正确性，是保障软件可靠性的有效方法.而对循环语句的分析与验证，是形式化证明中的关键，对循环语句的处理一直是程序分析与验证中的一个难点问题.提出使用循环语句修改的内存和这些内存中存放的新值来描述循环语句的执行效果，并将该执行效果定义为循环摘要.同时，提出一种自动生成循环摘要的方法，可以为操作常用数据结构的循环自动生成循环摘要，包含嵌套循环.此外，基于循环摘要，可以自动生成循环语句的规约，包括循环不变式、循环的前置条件以及循环的后置条件.已经实现了自动生成循环摘要以及循环规约的方法，并将它们集成到验证工具Accumulator中.实验结果表明，该方法可以有效地生成循环摘要，并生成多种类型的规约，从而辅助软件程序的形式化证明，提高验证的自动化程度和效率，减轻验证人员的负担.

摘要:正则模型是非正规模态逻辑的模型，通过定义正则模型的不相交并、C2t_-互模拟、生成子模型、C2t_-超滤扩张等模型上的运算，可以证明一个正则模型类在时态语言中可定义当且仅当它在不相交并、满C2t_-互模拟像、C2t_-超滤扩张下封闭，并且它的补类在C2t_-超滤扩张下封闭.该刻画定理说明了时态语言在正则模型类上的表达力.

摘要:已有的实时系统模型无法动态创建新进程.为此，基于时间自动机模型，提出了异步多进程时间自动机模型，将每个进程抽象为进程时间自动机，其部分状态能够触发新进程.考虑到队列会导致模型图灵完备，进程都被缓存在集合中，但仍可建模许多实时系统.通过将其编码到可读边时间Petri网，证明了该模型的可覆盖性问题可判定.

摘要:从系统诊断的角度来看，可诊断性是离散事件系统的一个重要性质.其要求系统发生故障后经过有限步的观测可以检测并隔离故障.为简单起见，对离散事件系统可诊断性的研究大都假定观测是确定的，即观测到的事件序列与系统实际发生的可观测事件序列一致.而在实际应用中，由于感知器的精度、信息传输通道的噪声等原因，所获取的观测往往是不确定的.重点研究观测不确定条件下离散事件系统的可诊断性问题.首先扩展了传统可诊断性的定义，定义了观测不确定条件下的可诊断性；然后，分别给出各类观测不确定条件下的可诊断性判定方法；在更一般的情况下，各类观测不确定可能共同存在，因此，最后给出一般情况下的可诊断性判定方法.

摘要:轨迹静态简化技术是在确保与原轨迹等价的前提下，通过随机减少程序执行时线程切换的数量，达到提高程序员调试并发程序效率的目的.然而，轨迹中可减少的线程切换分布往往是不均匀的，因此，随机简化策略难以有效地发现可简化的线程切换.为此，提出了面向收敛的合并算法致力于这个问题.该算法的基本思想是：不断地随机选择一线程执行区间作为中心，在同一线程内，采用面向收敛的合并算法迭代地寻找可与其合并的前置执行区间和后置执行区间.实验结果表明，该方法可以高品质地减少执行轨迹中的线程切换数量，进而有助于程序员快速发现引发错误的线程交错.

摘要:近年来，伴随着人工智能领域的浪潮，机器人越来越多地出现在我们的日常生活中，例如足球机器人、无人机、无人车等.如何保证这些自治机器人尤其是多个机器人在移动过程中的安全，成为人们一直很关心的问题.混成通信顺序进程（hybrid communicating sequential process，简称HCSP）是一种针对混成系统的形式化建模语言，在通信顺序进程（communicating sequential process，简称CSP）的基础上引入了微分方程以描述混成系统中的连续行为和控制逻辑，可以方便而高效地对大型控制系统，尤其是在有通信事件发生时的情形进行形式化建模.用HCSP建模多机器人的路径控制算法，并用定理证明工具HProver进行形式化验证，结果表明，在满足一定的初始条件下，机器人团队在整个运行途中不会发生碰撞.

摘要:随着计算机与物理环境的交互日益密切，信息-物理融合系统（cyber-physical system，简称CPS）在健康医疗、航空电子、智能建筑等领域具有广泛的应用前景，CPS的正确性、可靠性分析已引起人们的广泛关注.统计模型检测（statistical model checking，简称SMC）技术能够对CPS进行有效验证，并为系统的性能提供定量评估.然而，随着系统规模的日益扩大，如何提高统计模型检测技术验证CPS的效率，是目前所面临的主要困难之一.针对此问题，首先对现有SMC技术进行实验分析，总结各种SMC技术的受限适用范围和性能缺陷，并针对贝叶斯区间估计算法（Bayesian interval estimate，简称BIE）在实际概率接近0.5时需要大量路径才能完成验证的缺陷，提出一种基于抽象和学习的统计模型检测方法AL-SMC.该方法采用主成分分析、前缀树约减等技术对仿真路径进行学习和抽象，以减少样本空间；然后，提出了一个面向CPS的自适应SMC算法框架，可根据不同的概率区间自动选择AL-SMC算法或者BIE算法，有效应对不同情况下的验证问题；最后，结合经典案例进行实验分析，实验结果表明，自适应SMC算法框架能够在一定误差范围内有效提高CPS统计模型检测的效率，为CPS的分析验证提供了一种有效的途径.

摘要:信息-物理融合系统是一种新型嵌入式系统计算模式.它集成了控制计算过程和受控对象，二者相互影响并有机结合.随着信息技术在现实世界中更加广泛、深入的应用，智能化程度不断提升，在具有信息-物理紧密耦合特点的嵌入式系统中，嵌入式控制软件的功能比重急剧上升，作用更加突出.作为安全攸关的系统，需要引入形式化验证方法来保证嵌入式控制应用软件的安全性.基于自动机理论建立统一的系统验证模型，并针对系统的可达性、安全性（safety）和活性（liveness）等属性要求，提出了对该模型进行形式化验证的算法：基于有界模型检验方法，基于可达性将对系统模型的相关属性验证问题转换为可满足性判定问题.将活性转换为Büchi自动机，并基于四值语义进行判断.在求解过程中，通过偏序规约等手段化简了问题求解的规模，提高了可验证系统的规模.另外，结合协同仿真技术，灵活配置验证的场景，提高验证的可用性.实验结果表明，结合仿真，形式化协同验证方法可以有效地对系统进行验证.

摘要:面向动作的上下文感知（activity-oriented context-aware，简称AOCA）应用组织环境中的资源，为用户动作的顺利进行提供支持.为应对环境和动作相关需求的开放性，这类应用采用轻量级、增量式的开发方法进行开发.相对于在开发阶段描述全局信息的开发方法，AOCA应用的开发可能由不同开发者在不同时间共同参与，这可能会导致较多的不一致等问题，且难以在开发阶段被发现.围绕使用运行时验证手段提高AOCA应用可靠性这一目标展开研究.给出了对于AOCA应用运行状态进行形式化规约、对于系统级和应用级性质进行描述的方法.进一步地设计实现了AOCA应用监控器.最后，通过案例分析以及性能评估证实了该方法的有效性.

摘要:基于通信的列车控制系统（communication based train control system，简称CBTC）已经成为世界范围内建造轨道交通信号系统的标准制式.CBTC采用更加灵活和精确的列车控制，并提供连续的安全列车间隔保证和超速防护，在很大程度上提高了轨道交通运输的效率和安全性.尽管CBTC能够精确地实施实时控制，但由于CBTC涉及计算、通信与控制这3个方面的实时协同，系统设计与实现异常复杂.由设计缺陷而导致严重的灾难、事故和损失屡见不鲜.作为一个典型的安全攸关系统，如何保证CBTC的可信构造已成为领域研发人员关注的焦点与面临的最大挑战.鉴于在软硬件领域的成功经验，形式化方法目前已被公认为是保障CBTC可信性的一种有效方案.围绕CBTC的可信构造，从其生命周期的3个重要阶段，即系统需求分析、设计建模与底层实现入手，针对CBTC在可信方面的典型特征，梳理分析了CBTC系统在可信构造方面面临的挑战、国内外研究现状和发展趋势，全面介绍了形式化方法在CBTC可信构造中扮演的角色.

摘要:内存管理系统位于操作系统内核的最底层，为上层提供内存分配和回收机制.在航天器这类安全攸关的关键系统中，其可靠性和安全性至关重要，必须要考虑到强实时性、有限空间限制、高分配效率以及各种边界条件约束.因此，系统通常采用较为复杂的数据结构和算法来管理内存空间，同时需要采用非常严格的形式化方法来保证航天器这类安全攸关系统的高可信性.对复杂内存管理系统的形式化验证也会比之前的验证工作带来更多难题，主要体现在：内存管理模块中的复杂数据结构的形式化描述，操作的规范语义，行为的建模，内部函数的规范及断言定义与循环不变式的定义，实时性验证等方面.针对这些问题，深入分析实际的航天器操作系统内存管理系统的特性；探索基于分层迭代的语义描述与验证的一般性方法与理论，并应用这些理论方法来验证一个具有实际应用的航天嵌入式操作系统的内存管理系统.该研究成果有望直接应用于我国新一代的航天器系统.

摘要:部分求值技术在程序优化及软件自动生成等方面起着极为重要的作用.将部分求值技术应用到编译器测试中.为此，设计了一种C语言的子集peC语言，给出了该语言的部分求值策略的形式化描述，实现了peC语言的部分求值器，设计了基于部分求值技术的编译器测试框架.通过实验，该方法可以检测出大部分之前其他方法发现的GCC，LLVM编译器中的错误，此外还发现了其他方法不能发现的错误，这表明，将部分求值技术应用到编译器测试中是有效的.

摘要:同步数据流语言（如Lustre）近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好“误编译”问题，近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证，取得了很大的成功，如CompCert C编译器.L2C是基于这种方法开发的可信编译器.它以扩展的Lustre语言为源语言，以Clight（CompCert中的C语言子集）为目标语言.L2C是面向实际工业应用的同步数据流语言编译器.重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验.

摘要:软件非功能需求的实现涉及软件质量这一重要问题，非功能需求的满足程度，直接影响软件质量的满足程度.针对一直以来对软件质量的一贯重视以及软件非功能需求权衡的重要性，借鉴微观经济学领域的生产理论、替代弹性原理和线性规划方法，提出了软件非功能需求权衡代价分析方法并开发了辅助工具.首先，对项目组前期完成的可信软件非功能需求可满足性分析方法进行改进，提出了利益相关者通过协商获取非功能需求评估数据的方法，建立了非功能需求本体概念并构建本体知识库；针对实现非功能需求的策略，使用前期已完成的策略推理方法，对推理产生矛盾的策略提出权衡代价分析方法；通过分析策略实施代价，为软件开发及演化提供具有实际可操作的权衡决策依据，从更加符合产业化需要的角度解决软件非功能需求权衡问题；最后，基于可信第三方认证中心软件案例的维护及演化需要，对推理出矛盾的策略进行权衡代价分析，并给予决策建议，说明所提出方法的可行性.

摘要:深网查询在Web上众多的应用，需要查询大量的数据源才能获得足够的数据，如多媒体数据搜索、团购网站信息聚合等.应用的成功，取决于查询多数据源的效率和效果.当前研究侧重查询与数据源的相关性而忽略数据源之间的重叠关系，使得不同数据源上相同结果的数据被重复查询，增加了查询开销及数据源的工作负载.为了提高深网查询的效率，提出一种元组水平的分层抽样方法来估计和利用查询在数据源上的统计数据，选择高相关、低重叠的数据源.该方法分为两个阶段：离线阶段，基于元组水平对数据源进行分层抽样，获得样本数据；在线阶段，基于样本数据迭代地估计查询在数据源上的覆盖率和重叠率，并采用一种启发式策略以高效地发现低重叠的数据源.实验结果表明，该方法能够显著提高重叠数据源选择的精度和效率.

摘要:针对大规模IP网络拥塞链路丢包率范围推断算法中存在的不足，提出一种贪婪启发式拥塞链路丢包率范围推断算法.借助多时隙路径探测，避开单时隙探测对时钟同步的强依赖；通过学习各链路拥塞先验概率，借助贝叶斯最大后验定位拥塞链路；提出了聚类拥塞链路相关、性能相近路径集合的策略，通过对聚类路径集合中性能相似系数求解，循环推断拥塞链路丢包率范围.实验验证了算法的准确性及鲁棒性.

摘要:智能无人车软件系统通常由多个功能模块组成，在模块间高效、可靠地传输传感器数据以及决策和控制信息等，是智能无人车系统运行的重要保障.目前，国内外大多数智能无人车软件系统所使用的消息传输机制均基于套接字（socket），其容易部署在分布式的控制器环境中，且能满足在较小数据量下的消息快速传输.但是，随着智能无人车集成控制器性能的提升以及环境感知手段的发展，对功能模块间传输的数据量以及带宽提出了更高的要求.现有基于套接字的消息传输机制因其受网络协议的限制，需要分块传输大数据包，不仅增加了收发双方的开销，而且还增加了消息传输延迟.提出一种基于共享内存（shared memory）的智能无人车进程间消息异步传输机制，模块间通过共享内存空间进行数据交互.共享内存空间由超级块和数据块构成，通过环形队列管理数据块收发；同时，采用原子操作提高整体性能，实现图像等大数据包的有效传输.该设计应用于智能无人车模块间通信，可以明显降低数据传输时延，提高系统吞吐量.实验结果表明，该方法针对典型大数据包（如3MB）的平均传输时延为2.5ms，低于LCM的12ms以及ROS中Sharedmem_transport的3.9ms.另外，该系统的最大吞吐量达到1.1GB/s，高于LCM的180MB/s以及Sharedmem_transport的600MB/s.