基于UML和OCL的类间交互测试用例生成算法研究

针对面向对象软件的类、封装、继承、动态连接等特性,对对象建模语言(UML模型)中的顺序图添加对象约束语言(OCL约束),做类间交互的软件测试。提出执行图EG生成算法,将顺序图SD转换为EG,解决UML2.0顺序图新增特性中的alt,loop,opt,break这4种常见组合片段及其嵌套和多态性问题;为得到最小完备的测试路径,提出EG的遍历策略和测试路径生成算法;确定测试场景,生成测试用例。经实例分析,它可以基于UML顺序图与OCL作系统地测试。     

基于UML顺序图的测试场景自动生成研究

UML顺序图直观地展现了对象之间的消息动态交互过程,适合于作为面向对象软件交互测试用例生成的依据。本文针对测试用例中的测试场景生成问题进行了研究,在将顺序图转化为消息交互流程图的基础上,根据对象覆盖、消息对覆盖、消息覆盖和逻辑路径覆盖等准则,分别给出了不同的测试场景生成算法,最后探讨了测试场景的健壮性。     

一个基于UML顺序图的场景测试用例生成方法

UML顺序图是基于UML开发的软件设计模型的重要组成部分，它描述了软件系统的动态行为，是软件集成测试过程中的一个重要的信息来源。本文提出了一个基于UML顺序图的场景测试方法，它以UML顺序图为主要测试模型，结合UML状态图和类图生成所有的测试场景，最后使用范畴一划分方法找到与每一场景相关的环境条件并将它与方法序列、输入、输出合理组合作为覆盖该场景的测试用例，用于测试该场景中对象之间的交互。由于UML已广泛用于软件分析和设计阶段，通过UML模型生成测试用例可充分利用已有的设计结果，减少测试阶段所需的费用，对于已使用UML的工业界有着重要的意义。     

一种基于UML动态视图的测试场景生成方法

本文提出一种基于UML动态视图的测试场景生成方法。通过将状态图中对象的状态信息加入顺序图,构建一个基于UML动态视图的测试模型,将其转化为扩展的十字链表结构的有向图;针对测试模型中存在的普通、条件、循环消息类型提出相应的处理方法,采用深度优先算法遍历生成测试场景。在将复杂的UML图转化为测试模型的过程中,应用该方法可以提高所生成场景路径的完整性,同时降低生成场景的冗余度。     

UML2．0顺序图的XYZ／E时序逻辑语义研究

UML2．0顺序图适合于描述软件体系结构的各个组件之间和复合组件内部各个子组件之间的动态交互行为，但由于UML2．0顺序图的语义不够精确，使得它的描述结果不利于进一步的分析和验证。基于此，本文在定义UML2．0顺序图的语法和语法约束的基础上，给出了UML2．0顺序图的XYZ／E时序逻辑语义，为使用UML2．0顺序图与XYZ／E相结合的方式来描述软件体系结构的动态交互行为奠定了基础。     

面向基于场景规约的Web服务消息流分析与验证

采用UML顺序图构成基于场景的规约、WS-BPEL作为Web服务的描述语言,提出了一种面向基于场景规约对Web服务消息流进行分析与验证的方法:首先,对WS-BPEL消息流进行分析并将其自动抽象为基于Petri网的模型;同时,为了缩小状态空间、提高验证效率,在不影响消息交互顺序的前提下,对WS-BPEL源码和基于Petri网的模型分别进行化简,即面向基于场景规约将与验证无关的活动和元素删除;最后,通过遍历基于Petri网的模型以验证WS-BPEL消息流与基于场景的规约之间的一致性(消息交互顺序的存在/强制一致性).文中通过一个贯穿整个分析与验证过程的实例加以说明.该方法已经实现成为一个原型工具.     

UML2.0顺序图的时序描述逻辑语义

针对UML2.0顺序图用于对象间交互行为建模时存在动态语义缺乏精确形式化描述的问题,提出一种基于时序描述逻辑的UML2.0顺序图形式化方法。对描述逻辑进行时序扩展,得到可表示动态和时序语义的形式化规范——时序描述逻辑,根据UML2.0新增的交互操作符将UML2.0顺序图分成一个或多个最大顺序片段,通过形式化最大顺序片段和交互操作符得到UML2.0顺序图的时序描述逻辑语义。实例检验结果表明,该方法具有可行性。     

实时系统动态行为模型的一种形式分析方法*

提出了一种基于统一建模语言UML 2.0的实时系统动态行为模型的形式分析方法。首先给出了UML顺序图的形式化描述,分析了UML顺序图中事件之间的关系;在此基础上,给出一种对象自动机来描述每个对象在UML顺序图描述的场景中所参与的事件序列的方法,并将该方法扩展到带有组合片段的UML 2.0顺序图;最后通过分析UML 2.0顺序图中的时间建模机制,给出了从UML 2.0顺序图中提取时间约束得到时间自动机的算法。     

UML2．0顺序图的一种有穷自动机模型

为了在软件开发早期阶段对UML2．0顺序图模型进行分析和验证,本文给出了UML2．0顺序图的一种有穷自动机模型。首先给出了顺序图在语法和语义上的形式化描述,然后提出了一种使有穷自动机来描述每个对象在顺序图描述的场景中所参与的事件序列的方法,并将该方法扩展到带有组合片段的UML2．0顺序图,最后分析了UML2．0顺序图中的时间建模机制,设计了从UML2．0顺序图中提取时间约束的算法。以上工作为使用模型检测工具UPPAAL对顺序图模型进行进一步的分析与验证奠定了基础。     

场景驱动的服务行为调控

提出了一个场景驱动的服务行为调控途径.首先,用UML顺序图模型作为场景规约以描述用户对服务行为的需求,并且基于目标服务的BPEL行为规约,构造表示服务行为的BPEL-Petri网模型(简称BPN模型);其次,基于并发变迁分析BPN模型上表示服务行为的路径,并通过遍历BPN模型获取包含UML顺序图描绘场景的服务行为集合;最后,根据行为分析的结果构建了调控服务,通过在运行时监听、检查并过滤用户与目标服务的消息交互,从目标服务中抽取或过滤顺序图描绘的场景.在此基础上,开发了原型工具BASIS,以支撑场景驱动的服务行为调控途径,并通过实例研究展示了该方法的可行性.     

Towards an Efficient Path-Oriented Tool for Bounded Reachability Analysis of Linear Hybrid Systems using Linear Programming

The existing techniques for reachability analysis of linear hybrid automata do not scale well to problem sizes of practical interest. Instead of developing a tool to perform reachability check on all the paths of a linear hybrid automaton, a complementary approach is to develop an efficient path-oriented tool to check one path at a time where the length of the path being checked can be made very large and the size of the automaton can be made large enough to handle problems of practical interest. This approach of symbolic execution of paths can be used by design engineers to check important paths and thereby, increase the faith in the correctness of the system. Unlike simple testing, each path in our framework represents a dense set of possible trajectories of the system being analyzed. In this paper, we develop the linear programming based techniques towards an efficient path-oriented tool for the bounded reachability analysis of linear hybrid systems.     

基于场景构件式实时软件设计的一致性检验

在复杂的实时软件系统中使用构件式设计方法,已成为目前软件工程中的研究热点.如何有效地验证实时软件的设计是否满足给定的时间规约,是实时计算领域中的主要挑战之一.通过在接口自动机模型中添加时间区间标记,来扩展其对实时系统接口行为的表达能力;使用实时接口自动机网络来描述实时软件系统的构件式设计模型;使用带布尔不等式时间约束的UML顺序图表示基于场景的需求规约,对系统设计阶段实时软件构件的动态行为进行形式化分析与检验.通过对实时接口自动机网络状态空间的分析,构造了其可兼容的整型状态等价类空间的可达图,并在此基础上给出了验证算法,以检验构件式实时软件系统的设计与带时间约束的场景式规约之间的一致性.     

Optimal reachability for multi-priced timed automata

In this paper, we prove the decidability of the minimal and maximal reachability problems for multi-priced timed automata, an extension of timed automata with multiple cost variables evolving according to given rates for each location. More precisely, we consider the problems of synthesizing the minimal and maximal costs of reaching a given target location. These problems generalize conditional optimal reachability, i.e., the problem of minimizing one primary cost under individual upper bound constraints on the remaining, secondary, costs, and the problem of maximizing the primary cost under individual lower bound constraints on the secondary costs. Furthermore, under the liveness constraint that all traces eventually reach the goal location, we can synthesize all costs combinations that can reach the goal.

The decidability of the minimal reachability problem is proven by constructing a zone-based algorithm that always terminates while synthesizing the optimal cost tuples. For the corresponding maximization problem, we construct two zone-based algorithms, one with and one without the above liveness constraint. All algorithms are presented in the setting of two cost variables and then lifted to an arbitrary number of cost variables.     

How to stop time stopping

Zeno-timelocks constitute a challenge for the formal verification of timed automata: they are difficult to detect, and the verification of most properties (e.g., safety) is only correct for timelock-free models. Some time ago, Tripakis proposed a syntactic check on the structure of timed automata: if a certain condition (called strong non-zenoness’ SNZ) is met by all the loops in a given automaton, then zeno-timelocks are guaranteed not to occur. Checking for SNZ is efficient, and compositional (if all components in a network of automata are strongly non-zeno, then the network is free from zeno-timelocks). Strong non-zenoness, however, is sufficient-only: There exist non-zeno specifications which are not strongly non-zeno. A TCTL formula is known that represents a sufficient-and-necessary condition for non-zenoness; unfortunately, this formula requires a demanding model-checking algorithm, and not all model-checkers are able to express it. In addition, this algorithm provides only limited diagnostic information. Here we propose a number of alternative solutions. First, we show that the compositional application of SNZ can be weakened: some networks can be guaranteed to be free from Zeno-timelocks, even if not every component is strongly non-zeno. Secondly, we present new syntactic, sufficient-only conditions that complement SNZ. Finally, we describe a sufficient-and-necessary condition that only requires a simple form of reachability analysis. Furthermore, our conditions identify the cause of zeno-timelocks directly on the model, in the form of unsafe loops. We also comment on a tool that we have developed, which implements the syntactic checks on Uppaal models. The tool is also able to derive, from those unsafe loops in a given automaton (in general, an Uppaal model representing a product automaton of a given network), the reachability formulas that characterise the occurrence of zeno-timelocks. A modified version of the carrier sense multiple access with collision detection protocol is used as a case-study.     

基于场景规约的构件式系统设计分析与验证

使用接口自动机及接口自动机网络来描述构件式系统的行为设计模型,使用UML顺序图表示基于场景的需求规约,对系统设计阶段的构件交互行为的动态兼容性进行形式化分析和检验.通过对接口自动机网络状态空间的分析,给出了一系列算法以检验系统行为的存在一致性以及几种不同形式的强制一致性性质,包括前向强制一致性、逆向强制一致性以及双向强制一致性等.     

Path-oriented bounded reachability analysis of composed linear hybrid systems

The existing techniques for reachability analysis of linear hybrid systems do not scale well to the problem size of practical interest. The performance of existing techniques is even worse for reachability analysis of a composition of several linear hybrid automata. In this paper, we present an efficient path-oriented approach to bounded reachability analysis of composed systems modeled by linear hybrid automata with synchronization events. It is suitable for analyzing systems with many components by selecting critical paths, while this task was quite insurmountable before because of the state explosion problem. This group of paths will be transformed to a group of linear constraints, which can be solved by a linear programming solver efficiently. This approach of symbolic execution of paths allows design engineers to check important paths, and accordingly increase the faith in the correctness of the system. This approach is implemented into a prototype tool Bounded reAchability CHecker (BACH). The experimental data show that both the path length and the number of participant automata in a system checked using BACH can scale up greatly to satisfy practical requirements.     

BACH:线性混成系统有界可达性模型检验工具

混成自动机的模型检验问题非常困难,即使是其中相对简单的一个子类--线性混成自动机,它的可达性问题仍然是不可判定的.现有的相关工具大都使用多面体计算来判定线性混成自动机状态空间的可达集,复杂度高、效率低,无法解决实际应用规模的问题.描述了一个面向线性混成系统有界可达性模型检验工具--BACH(bounded reacha...     

SAT–LP–IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata

As discrete jumps and continuous flows tangle in the behavior of linear hybrid automata (LHA), the bounded model checking (BMC) for reachability of LHA is a challenging problem. Current works try to handle this problem by encoding all the discrete and continuous behaviors in the bound into a set of SMT formulas which can then be solved by SMT solvers. However, when the system size is large, the object SMT problem could be huge and difficult to solve. Instead of encoding everything into one constraint set, this paper proposes a SAT–LP–IIS joint-directed solution to conduct the BMC for reachability of LHA in a layered way. First, the bounded graph structure of LHA is encoded into a propositional formula set, and solved by SAT solvers to find potential paths which can reach the target location on the graph. Then, the feasibility of certain path is encoded into a set of linear constraints which can then be solved by linear programming (LP) efficiently. If the path is not feasible, irreducible infeasible set (IIS) technique is deployed to locate an infeasible path segment which will be fed to the SAT solver to accelerate the enumerating process. Experiments show that by this SAT–LP–IIS joint-directed solution, the memory usage of the BMC of LHA is well-controlled and the performance outperforms the state-of-the-art SMT-style competitors significantly.     

Discrete reachability of hybrid systems

This paper concerns hybrid systems subject to discrete-event supervisory control. It investigates the discrete reachability, where the hybrid system should be moved from a discrete initial state z init into a given discrete goal state z goal by a sequence of discrete inputs. The reachability analysis is carried out in three steps. First, a discrete-event model of the hybrid system is set up. Stochastic automata are used to describe all state sequences which may be generated by the hybrid system. Such a model is called complete. Second, methods for the reachability analysis of stochastic automata are elaborated which concern a weak and a strong condition for reachability. Third, these methods are applied to the hybrid system. It is shown that the reachability of the automaton implies the discrete reachability of the hybrid system, because the model is complete. Therefore, the weak and the strong condition for reachability of the stochastic automaton yield a necessary and a sufficient condition for discrete reachability of the hybrid system.     

网构软件的资源自适应性的形式化分析与验证

针对基于构件的网构软件系统对环境资源变化的自适应性特征的可信分析与验证展开研究.具体工作包括:在网构软件的系统模型层次,使用带资源语义信息的接口自动机对软件构件的行为进行形式化建模,其包含了构件在完成特定功能的过程中对环境资源的使用特征;使用资源接口自动机网络来描述构件组装实体的组合行为;使用基于场景的UML顺序图模型来描述具有多功能的组合系统规约;分别研究了检验组合系统的所有行为是否都满足给定的资源约束以及检验指定的系统行为是否满足资源约束这两个具体问题:通过对资源自动机网络状态空间的分析,构造其相应的可达图,在此基础上给出了相应的检验资源可满足性、最小资源需求量以及检验指定功能合法性等算法.