摘要：描述和设计计算机网络通信协议时，使用抽象的同步通信机制最为方便。但在实际中，使用异步通信机制将不可避免。基于霍尔的“通信顺序进程”和其他对通信协议描述与设计的理论研究结果，本文提出一个形式化方法。

摘要：针对网络故障的复杂性和多样性,对网络故障管理的形式化描述进行了研究。基于霍尔的“通信顺序进程”和相关的网络形式化的理论研究结果,提出了一种网络故障管理的形式化方法。该方法通过添加新的概念和定义扩充了“通信顺序进程”,为描述复杂的故障信息提供数据类型支持,同时建立故障模型对网络故障采集和网络故障分析进行了精确的形式化描述,为故障管理系统的设计正确性和可验证性提供了可靠的数学依据。

摘要：针对实时系统软件设计难以有效兼顾功能与非功能需求的问题,提出了一种支持实时软件资源建模与分析的方法.首先,通过在通信顺序进程上扩展资源信息,得到资源通信顺序进程,并将实时系统指令使用的资源映射为资源通信顺序进程的资源.利用资源通信顺序进程对实时软件资源建模,并进行量化分析.然后,通过提出一系列资源优化检查算法,对建模结果进行资源可满足性检查,并计算出当前系统所需的最少资源量.最后,对机载防撞告警系统进行建模与分析,以说明该方法的有效性.结果表明,该方法能够分析影响实时系统资源使用的关键软件设计要素,评估软件优化对系统资源使用的影响,从而在很大程度上提高了实时系统资源计算和分析的可信性.该计算结果有助于实时系统资源的量化分析和资源优化设计.

摘要：IEC 61850智能电子设备(IED)间的互操作是IEC 61850实施的关键。为解决在IED生产后对其进行互操作性测试成本高和测试周期长的问题,提出了基于形式化方法行为树(BT)的IED互操作性描述与验证方法,在IED设计阶段对其互操作性进行描述和验证。首先对参与交互应用的IED的外部行为特征及分布式功能的交互模型采用图形化BT进行建模,然后将交互模型的BT模型转化为通信顺序进程(CSP)模型,进而采用过程分析工具(PAT)对交互模型进行死锁及可达性等交互性验证。以变电站定时过流保护IED交互模型为例进行了建模与验证,结果表明该方法能有效检测IED设备设计中存在的交互性缺陷。

摘要：模型检测是通信顺序进程(communicating sequential processes,简称CSP)形式化验证的重要手段.当前,CSP模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用CSP语言进行描述,虽然有利于精炼检测(refinement checking),但描述能力较弱,通用性不强.鉴于此,提出了一种新的CSP指称语义模型——关键迹模型(critical-trace model)及基于该指称语义模型的CSP模型检测方法,并证明了其验证的可靠性,避免了上述问题.关键迹模型采用递归策略计算,待验证性质采用线性时态逻辑(linear temporal logic,简称LTL)描述.基于回答集程序设计(answer set programming,简称ASP)实现了关键迹模型的自动生成及LTL的自动验证,并开发了一个CSP模型检测原型系统——T_ASP.实验结果表明:与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,且可同时验证多条性质,在性质不满足时还可提供多条反例.

摘要：IEC 61850将变电站智能电子设备(IED)的功能抽象成若干逻辑节点,以达到信息交换的目的。IED及其逻辑节点之间的交互关系复杂,如何正确地设计并实现这种复杂的行为是IEC 61850实施的关键。形式化方法为此提供了良好的途径。提出采用进程代数方法对各种功能在IED之间、IED内部逻辑节点之间的交互关系、系统行为进行严谨地描述并进行自动验证,以保证分布式功能的正确性。以定时过电流保护功能为例,建立了基于IEC 61850的IED交互模型,采用在通信顺序进程(CSP)上加入时间相关操作形成的形式化语言Timed CSP描述其交互功能及系统行为,在验证工具——进程分析工具包(PAT)环境中进行了验证。结果表明,所提出的方法能有效地检测出描述中潜在的缺陷,有利于指导IED交互系统的设计并节约开发成本。

摘要：在不干扰理论的基础上,提出扩展不干扰模型ENISM及其验证方法,用以描述和分析操作系统中的信息流策略.工作包括:(1)依据系统功能模块定义多个执行域,以即将执行的可能动作序列集合与可读取的数据存储值集合一同作为ENISM定义执行域安全状态的基础;(2)给出判定系统中不存在违反策略的执行轨迹和数据流动的条件ENISM-CC;(3)基于通信顺序进程给出ENISM-CC的语义及操作系统模块设计的形式化描述和验证方法.

摘要：Webservices组合是Webservices领域的研究热点,虽然已经提出了很多组合的方法,但从体系结构方面去研究Webservices组合,则是一个新的研究角度.BPEL4WS是当前工业界主流的Webservices组合描述语言.给出了基于BPEL4WS的Webservices组合系统体系结构风格,并针对这种风格设计了体系结构描述语言WSC/ADL(Webservicescomposition/architecturedescriptionlanguage),WSC/ADL是基于体系结构的、自顶向下的Webservices组合开发的研究基础,其组成包含描述Webservices的服务构件、描述Webservices之间交互的连接件以及建立服务构件和连接件实例联系的配置.给出了WSC/ADL的详细分析介绍和实例说明,并与相关工作进行了比较.

摘要：对一个开源的、主流的虚拟机监控器Xen进行了优化研究。用通信顺序进程(CSP)和软件体系结构等形式化方法描述了Xen的块设备I/O体系结构,增加了约束其构件并发交互行为的设计准则,理论上确保了并发交互不死锁,提高了系统的可靠性。以这些设计准则为指导,重新优化设计了相关程序。实验表明优化虽然减小了I/O吞吐量,但系统的可靠性得到了增强,优化仍具有价值。

摘要：软件定义网络(SDN)为网络赋予了可编程性,降低了网络管理的复杂性,促进了新型网络技术的发展。SDN交换机作为数据转发与策略执行的设备,其权限不应被未经授权的实体窃取。然而,SDN交换机并不总是执行控制器下发的命令,恶意攻击者通过侵蚀SDN交换机对网络进行隐秘而致命的攻击,严重影响用户的端到端通信质量。通信顺序进程(CSP)作为针对并发系统设计的建模语言,可对SDN交换机-交换机,以及交换机-主机间的交互进行准确的描述。文中使用CSP对SDN交换机、终端主机进行建模,对两种异常交换机定位方法进行理论分析,并在实例化的模型系统中验证检测方法在边缘交换机作为出口交换机恶意转发时的有效性,结果表明无法检测该异常行为。针对这一问题,提出了边缘交换机异常检测方法,主机记录统计信息并通过构造特殊的数据包触发packet_in消息完成与控制器之间的信息传递,控制器收集统计信息并利用边缘交换机与主机之间的统计信息一致性检测边缘交换机的异常传输行为。最后,基于ryu控制器在mininet平台上进行实验,实验结果表明,边缘交换机异常检测方法可以成功检测异常行为。