和与积数迷的符号化模型检测

和与积是一个著名的数迷问题.采用公告逻辑对该问题进行建模,将其Kripke模型符号化表示为多智能体有限状态程序,并在其上采用一种基于局部命题解释系统语义的知识逻辑符号化模型检测算法计算该问题的所有解.在时态逻辑模型检测器NuSMV基础上扩展实现了本文算法,然后在相同实验平台上用动态认知建模工具DEMO对该问题进行求解.实验表明,我们的算法不仅结果正确,而且在运行效率上与DEMO相比占有绝对优势.     

程序切片技术在并发程序模型检查中的应用

模型检查技术在硬件和协议设计方面已经取得很大成功,但在软件验证方面仍存在很多困难。其主要问题是如何从源代码中自动抽取验证所要模型并精简其状态空间。文中通过对程序切片技术的研究,来解决并发程序验证的建模问题,包括把验证公式映射到切片准则．并把得到的程序切片转化为验证所需的模型。经程序切片处理后,软件模型检查效率得到提高。     

基于SPIN的CSCW系统的验证

近年来,CSCW系统呈现出用户越来越多、权限关系越来越复杂、组织结构规模越来越大、处理的情况越来越复杂的趋势。因此,CSCW系统的访问控制策略以及访问控制策略的验证已成为国内外CSCW领域十分值得研究和探讨的问题。针对CSCW系统设计的特点,提出了一种验证策略。结合具体实例,使用RBAC模型描述CSCW系统的访问控制权限,利用SPIN工具将模型检测应用于验证CSCW系统属性。     

软件体系结构求精研究

为了保证软件质量,提高软件可靠性、可重用性和可维护性,软件体系结构这一概念自提出以来就得到广泛关注,成为软件工程的一项重要研究领域。软件体系结构求精作为体系结构从抽象到具体的形式化方法,连接了体系结构分析到具体实现之间的鸿沟,从而有效地保证了软件体系结构的层次性和可跟踪性。良好的软件体系结构求精方法使得软件开发自动化．加速软件产品的交付过程,降低软件成本,以及提高软件质量。针对体系结构求精研究的主要内容,较系统地阐述了几种体系结构求精分类方法,并对求精检测的相关内容作了介绍,最后是对体系结构求精以后工作的展望。     

A structural linearization principle for processes

In [11], an induction principle for processes was given which allows one to apply model-checking techniques to parameterized families of processes. A limitation of the induction principle is that it does not apply to the case in which one process depends directly upon a parameterized number of processes, which grows without bound. This would seem to preclude its application to families ofN processes interconnected in a star topology. Nonetheless, we show that if the dependency can be computed incrementally, then the direct dependency upon the parameterized number of processes may be re-expressed recursively in terms of a linear cascade of processes, yielding in effect a linearization of the inter-process dependencies and allowing the induction principle to apply.A previous version of this paper appears in the Proceedings of CAV 1993 (LNCS 697).     

基于空充暂态电流的线路保护CT极性校验方法

线路保护电流互感器(current transformer, CT)二次采样回路接线正确是保护正确动作的前提。针对线路投运启动过程中保护CT极性校验困难的问题,首先分析了在有限负荷和无负荷下利用线路稳态电流进行极性校验的边界限制条件。进而针对不满足限制条件下无负荷极性校验困难的问题,提出了一种基于空充暂态电流的线路保护CT极性校验方法。该方法先利用幅值较大的本端暂态电流对三相CT相对极性进行初判,再通过线路本端暂态电流和测量电压基于线路结构计算对端暂态电流来实现本端保护CT极性错误相识别,CT极性正确时对端计算电流理论上为零,CT极性错误时会呈现较大的幅值。该方法有效解决了传统极性校验方法在负荷不足时无法校验的问题。仿真和录波验证了该方法的有效性,并已纳入工程应用方案。     

AR-based deep learning for real-time inspection of cable brackets in aircraft

In the process of aircraft assembly, there exist numerous and ubiquitous cable brackets that shall be installed on frames and subsequently need to be manually verified with CAD models. Such a task is usually performed by special operators, hence is time-consuming, labor-intensive, and error-prone. In order to save the inspection time and increase the reliability of results, many researchers attempt to develop intelligent inspection systems using robotic, AR, or AI technologies. However, there is no comprehensive method to achieve enough portability, intelligence, efficiency, and accuracy while providing intuitive task assistance for inspectors in real time. In this paper, a combined AR+AI system is introduced to assist brackets inspection in a more intelligent yet efficient manner. Especially, AR-based Mask R-CNN is proposed by skillfully integrating markerless AR into deep learning-based instance segmentation to generate more accurate and fewer region proposals, and thus alleviates the computation load of the deep learning program. Based on this, brackets segmentation can be performed robustly and efficiently on mobile devices such as smartphones or tablets. By using the proposed system, CAD model checking can be automatically performed between the segmented physical brackets and the corresponding virtual brackets rendered by AR in real time. Furthermore, the inspection results can be directly projected on the corresponding physical brackets for the convenience of maintenance. To verify the feasibility of the proposed method, experiments are carried out on a full-scale mock-up of C919 aircraft main landing gear cabin. The experimental results indicate that the inspection accuracy is up to 97.1%. Finally, the system has been deployed in the real C919 aircraft final-assembly workshop. The preliminary evaluation reveals that the proposed real-time AR-assisted intelligent inspection approach is effective and promising for large-scale industrial applications.     

可信执行环境访问控制建模与安全性分析

可信执行环境(TEE)的安全问题一直受到国内外学者的关注. 利用内存标签技术可以在可信执行环境中实现更细粒度的内存隔离和访问控制机制, 但已有方案往往依赖于测试或者经验分析表明其有效性, 缺乏严格的正确性和安全性保证. 针对内存标签实现的访问控制提出通用的形式化模型框架, 并提出一种基于模型检测的访问控制安全性分析方法. 首先, 利用形式化方法构建基于内存标签的可信执行环境访问控制通用模型框架, 给出访问控制实体的形式化定义, 定义的规则包括访问控制规则和标签更新规则; 然后利用形式化语言B以递增的方式设计并实现该框架的抽象机模型, 通过不变式约束形式化描述模型的基本性质; 再次以可信执行环境的一个具体实现TIMBER-V为应用实例, 通过实例化抽象机模型构建TIMBER-V访问控制模型, 添加安全性质规约并运用模型检测验证模型的功能正确性和安全性; 最后模拟具体攻击场景并实现攻击检测, 评估结果表明提出的安全性分析方法的有效性.     

事件日志的批量迹与过程模型的多视角对齐方法

在业务过程发现的一致性检测中,现有事件日志与过程模型的多视角对齐方法一次只能获得一条迹与过程模型的最优对齐;并且最优对齐求解中的启发函数计算复杂,以致最优对齐的计算效率较低。为此,提出一种基于迹最小编辑距离的、事件日志的批量迹与过程模型的多视角对齐方法。首先选取事件日志中的多条迹组成批量迹,使用过程挖掘算法得到批量迹的日志模型;进而获取日志模型与过程模型的乘积模型及其变迁系统,即为批量迹的搜索空间;然后设计基于Petri网变迁序列集合与剩余迹的最小编辑距离的启发函数来加快A*算法;最后设计可调节数据和资源视角所占权重的多视角代价函数,在乘积模型的变迁系统上提出批量迹中每条迹与过程模型的多视角最优对齐方法。仿真实验结果表明,相比已有工作,在计算批量迹与过程模型间的多视角对齐时,所提方法占用更少的内存空间和使用更少的运行时间。该方法提高了最优对齐的启发函数计算速度,可以一次获得批量迹的所有最优对齐,进而提高了事件日志与过程模型的多视角对齐效率。     

智能手机能耗多目标优化机制研究

智能手机的网络请求导致其续航能力下降,合并转发技术可有效降低能耗,但设置最优的合并转发时间仍是技术发展的关键,通过大量人工实验解决该问题耗时耗力。因此,基于统计模型检验,使用工具UPPAAL-SMC,以概率时间自动机对安卓设备中用户请求以及WiFi模块进行仿真建模,量化能耗、延迟、用户满意度等属性,进而利用统计模型检验,对不同请求频率的场景进行蒙特卡洛模拟,获得延迟对能耗以及用户满意度的影响。最终进行多目标优化,求得通用最优合并转发延迟时间为22 s,在满足用户体验的前提下平均降低了20%的能耗。该方法可在不同的使用场景下模拟得到通用最优合并转发延迟时间,为开发者提供参考。