基于UML活动图的用例识别

在面向对象的软件开发过程中,统一建模语言(unified modeling language, UML)的用例图用于捕获用户的需求.传统描述用例的方法一般是开发者根据自己的经验,从需求中人工获取用例.然而,如何自动生成准确的用例仍然是一个待解决的问题.本文提出了一种通过用UML活动图半自动生成用例的方法.首先通过引入形式化模型——统一结构来描述用例图与活动图,其次给出分解活动图的算法,然后根据分解活动图得到的依赖链生成对应的用例的事件流,从而得到用例模型,最后通过所开发的原型CASE工具进行案例的演示,验证了本文所提出的方法的可行性。     

基于K Framework的向量化机器学习指令语义形式化

ARM针对ARMv8.1-M微处理器架构推出基于M-Profile向量化扩展方案的技术,并命名为ARM Helium,声明能为ARM Cortex-M处理器提升达15倍的机器学习性能.随着物联网的高速发展,微处理器指令执行正确性尤为重要.指令集的官方手册作为芯片模拟程序,片上应用程序开发的依据,是程序正确性基本保障.主要介绍利用可执行语义框架K Framework对ARMv8.1-M官方参考手册中向量化机器学习指令的语义正确性研究.基于ARMv8.1-M的官方参考手册自动提取指令集中描述向量化机器学习指令执行过程的伪代码,并将其转换为形式化语义转换规则.通过K Framework提供的可执行框架利用测试用例,验证机器学习指令算数运算执行的正确性.     

Measuring code maintainability with deep neural networks

The maintainability of source code is a key quality characteristic for software quality. Many approaches have been proposed to quantitatively measure code maintainability. Such approaches rely heavily on code metrics, e.g., the number of Lines of Code and McCabe’s Cyclomatic Complexity. The employed code metrics are essentially statistics regarding code elements, e.g., the numbers of tokens, lines, references, and branch statements. However, natural language in source code, especially identifiers, is rarely exploited by such approaches. As a result, replacing meaningful identifiers with nonsense tokens would not significantly influence their outputs, although the replacement should have significantly reduced code maintainability. To this end, in this paper, we propose a novel approach (called DeepM) to measure code maintainability by exploiting the lexical semantics of text in source code. DeepM leverages deep learning techniques (e.g., LSTM and attention mechanism) to exploit these lexical semantics in measuring code maintainability. Another key rationale of DeepM is that measuring code maintainability is complex and often far beyond the capabilities of statistics or simple heuristics. Consequently, DeepM leverages deep learning techniques to automatically select useful features from complex and lengthy inputs and to construct a complex mapping (rather than simple heuristics) from the input to the output (code maintainability index). DeepM is evaluated on a manually-assessed dataset. The evaluation results suggest that DeepM is accurate, and it generates the same rankings of code maintainability as those of experienced programmers on 87.5% of manually ranked pairs of Java classes.     

拟态路由器TCP代理设计实现与形式化验证研究

拟态路由器基于拟态防御的动态异构冗余架构进行设计,对于未知漏洞后门具有良好的防御能力。协议代理在拟态路由器中处于内外联络的枢纽位置,协议代理的安全性和功能正确性对于拟态路由器有着重要意义。本文设计实现了拟态路由器的TCP协议代理,并采用形式化方法,对其安全性和功能正确性进行了验证。TCP协议代理嗅探邻居和主执行体之间的TCP报文,模拟邻居和从执行体建立TCP连接,并向上层应用层协议代理提供程序接口。基于分离逻辑与组合思想,采用Verifast定理证明器,对TCP协议代理的低级属性,包括指针安全使用、无内存泄露、无死代码等,进行了验证;同时,还对TCP协议代理的各主要功能模块的部分高级属性进行了形式化验证。搭建了包含3个执行体的拟态路由器实验环境,对实现结果进行了实际测试,结果表明所实现的TCP代理实现了预期功能。TCP协议代理实现总计1611行C代码,其中形式化验证所需人工引导定理检查器书写的证明共计588行。实际开发过程中,书写代码实现与书写人工证明所需的时间约为1:1。本文对TCP协议代理的实现与形式化验证工作证明了将形式化验证引入拟态路由器的关键组件开发中是确实可行的,且证明代价可以接受。     

Shifting role for human factors in an ‘unmanned’ era

Human factors practitioners (HFPs) play many different roles in the design, creation, operation and maintenance of engineered systems. Less well known are the methods which are aimed at helping with the early stages of design, which are more systems-oriented and often involve questions of the concept of operation in which the engineered system will be fielded. Emerging from the field of cognitive engineering, these methods, including simulation, cognitive work analysis, cognitive task analyses and hierarchical task analysis, will be important as autonomous systems become increasingly capable. Even the most capable systems will continue to interact with humans, and it is at these interfaces between humans and engineered systems that HFP will continue to be needed. This paper describes recent work to leverage these methods to inform concepts of operation in aviation and space, machine learning algorithms and goal-oriented human–machine collaboration.     

Undivided and Indistinguishable Histories in Branching-Time Logics

In the tree-like representation of Time, two histories are undivided at a moment t whenever they share a common moment in the future of t. In the present paper, it will first be proved that Ockhamist and Peircean branching-time logics are unable to express some important sentences in which the notion of undividedness is involved. Then, a new semantics for branching-time logic will be presented. The new semantics is based on trees endowed with an indistinguishability function, a generalization of the notion of undividedness. It will be shown that Ockhamist and Peircean semantics can be viewed as limit cases of the semantics developed in this paper.     

型构兼容的继承及其语义

本文揭示了在面向对象程序设计语言中,若劲旅子类重定义其继承的分类方法以发迹这些方法的规约,并且采用类似于Ｓｍａｌｔａｌｋ－８０中的继承机制的语义,将导致封将与继承之间的一个新总是为此,本文提出了一种新的继承机制－型构兼容的继承,以代替传统的增量继承。型构兼容的继承是一种灵活的代码复用机制,并且能够充分支持封装。     

A semantics of introspection in a reflective prototype-based language

In Malenfant et al. [19], we have described a reflective model for a prototype-based language based on thelookup o apply reflective introspection protocol. In this paper, we augment our previous protocol by converting it to handle continuations reified as first-class objects. First-class continuations provide much more control over the current computation; during the introspection phase fired by message sending, they make it possible not only to change the behavior of the program for that message but also for the entire future computation. In this paper, we provide this introspection protocol with a formal semantics. This result is obtained by exhibiting a mapping from program configurations to priority rewrite systems (PRS) as well as a mapping from message expressions to ground first-order terms used to query the PRS. Other advantages of this approach are: to ensure the termination of the introspection using the smallest set of formally justified conditions and to provide a clear declarative account of this reflective protocol. The PRS also appears as a meta-level to the base language, independent of the implementation, but from which we derive fundamental clues to obtain an efficient language processor. By our new model, we finally highlight the link between reflection in object-oriented languages and the one originally proposed by 3-Lisp [24], although object-orientation provides reusability to reflection, making it easier to use.     

基于ProVerif的安全协议形式化分析与验证

形式化方法是分析与验证安全协议属性的强有力的工具.在对一阶定理证明器ProVerif深入研究的基础上,对简化的Needham-Schroeder认证协议进行了形式化分析.     

UML状态图的测试用例自动生成

现有的研究在对UML状态图生成测试用例时,为简化问题而忽略了对伪状态的支持。针对这一问题,首先对UML状态图的伪状态概念进行分析,并讨论了其对相关测试用例生成算法的影响;改进了UMLstatechart语义对伪状态的定义,对伪状态进行适当的转换,同时扩充现有算法对伪状态的支持;提出了一套可以处理伪状态的UML状态图平坦化算法以及相应的测试用例生成方法,并对实际应用效果进行了验证。