共查询到20条相似文献,搜索用时 0 毫秒
1.
2.
UML状态机的形式语义 总被引:18,自引:1,他引:18
许多大型系统在进行分析和设计时,均采用UML作为需求描述语言,尤其是一些对安全性要求较高的系统,更是广泛采用UML的动态行为描述机制--状态机来描述协议及控制机制.但是,由于UML没有形式化的动态语义,不利于对其所描述的需求进行形式化验证和证明.为了解决这一问题,采用以下方法为UML状态机构建形式语义.把UML状态机中的状态映射到一种项代数上,用归纳的状态项表示状态机的状态.然后,把状态项映射到一种加标记的变迁系统LTS上,LTS-状态是状态机的状态项,LTS-变迁是UML状态机的微步.最后,用Plotk 相似文献
3.
为UML建模元素提供坚实的形式化语义基础是目前的研究热点之一,在这方面也有了不少探索。文章在过去的研究的基础上,给出了UML模型到COOZ规约的一种系统的转化方法。将UML模型转换到COOZ规约后,UML模型的推理验证就可以通过相应COOZ规约的推理验证实现。该方法不但为UML提供了精确的形式化语义基础,而且,提供了一种UML模型推理的合理的机制。 相似文献
4.
规约变异测试从软件功能的角度,对规约进行分析,从而揭示规约中存在的问题。本文提出一种基于UML状态图的变异测试方法,针对每种变异算子,分析其是否会引入冲突,进而有效避免不合理的变异操作;分析了每种变异算子产生等价变异体的条件,能够在生成变异体的同时检测并移除等价变异体,进而减少其对测试过程的影响;给出了杀掉每种变异体所需满足的条件,可在此基础上产生杀掉特定变异体所需的测试用例,从而提高测试用例集的质量。在此基础上,根据变异算子的实际功能,整合了功能相同的算子,减少了变异算子的数量,从而进一步降低了变异测试的开销。实验结果表明,本方法能够较好地提高测试用例的质量,进而提升测试的效率。 相似文献
5.
基于知识的UML图形文档自动生成 总被引:2,自引:0,他引:2
基于领域本体的需求获取使得用领域术语描述用户需求,并进行应用模型的自动分析成为可能,以尽可能地保证需求描述的正确性和完整性。从以领域概念为背景的应用模型,到以软件概念为基础的应用软件模型,是需求工程要完成的一个实质性跨越。UML是目前软件需求描述的一个实际上的标准。该文主要论述了从基于领域本体的应用需求描述到基于UML的软件需求文档的自动转换过程,文章提出建立从领域本体概念到UML概念映射规则库,以及根据UML概念填写用XML表示的UML图元模板的规则库,设计并实现了一个基于规则的,从应用需求概念到UML图元模板的自动转换工具。 相似文献
6.
现有基于L*算法的协议状态机主动推断方法忽略了协议特有的域知识,将协议报文抽象为相互独立、无意义的符号,并完全随机地生成测试样本进行状态机等价判定,导致产生大量的无效询问和测试样本,在真实网络环境下推断效率较低。在L+M算法的基础上提出了一种基于域知识的协议状态机主动推断算法L+N,其改进主要体现在:依据会话样本集提取各报文之间的强顺序约束关系来过滤无效的输出询问,构建会话样本集对应的扩展前缀树接受器(Extended Prefix Tree Accepter,EPTA)对输出询问进行预响应,提出了一种基于正例样本变异的等价询问近似判定算法以提升寻找反例的效率。实验结果表明,L+N算法能够大幅提高推断效率,并且具有与L+M算法相同的推断准确度。 相似文献
7.
8.
In the requirements engineering community, consistency and completeness have been identified as important properties of system specifications. Custom algorithms to verify these properties automatically have been devised for a number of specification languages, including SCR, RSML, and Statecharts. In this paper, we provide means to automatically verify completeness and consistency of Abstract State Machine (ASM) specifications. The verification is performed using a widely available tool, a SAT solver. The use of a SAT solver removes the need for designing and fine tuning language specific verification algorithms. Furthermore, the use of a SAT solver automates the verification procedure and produces a counterexample automatically when a specification is incomplete or inconsistent. We provide an algorithm to translate ASM specifications to a SAT problem instance. The translation is illustrated using the TASM toolset in conjunction with the “production cell system” case study. 相似文献
9.
针对目前飞机维修培训中拆装流程复杂,系统模型繁多的问题,采用层
次化分析法和UML 状态机相结合的建模方法,建立飞机组件的拆装过程模型。运用UML
状态机建立拆卸组件的状态、迁移和约束模型,规范拆卸零部件模型的统一性表达,提高建
模的效率。利用层次化方法对零部件进行层次规划,实现拆卸目标组件的有序逻辑表述,实
时监测拆卸零部件的状态,从而建立仿真程度高的训练模型。最后,以维修培训平台中飞机
某组件的拆装为例,验证层次化UML 状态机拆卸过程仿真方法的有效性。 相似文献
10.
Test Synthesis from UML Models of Distributed Software 总被引:1,自引:0,他引:1
Pickin S. Jard C. Jeron T. Jezequel J.-M. Le Traon Y. 《IEEE transactions on pattern analysis and machine intelligence》2007,33(4):252-269
The object-oriented software development process is increasingly used for the construction of complex distributed systems. In this context, behavior models have long been recognized as the basis for systematic approaches to requirements capture, specification, design, simulation, code generation, testing, and verification. Two complementary approaches for modeling behavior have proven useful in practice: interaction-based modeling (e.g., UML sequence diagrams) and state-based modeling (e.g., UML statecharts). Building on formal V&V techniques, in this article we present a method and a tool for automated synthesis of test cases from scenarios and a state-based design model of the application, remaining entirely within the UML framework. The underlying "on the fly" test synthesis algorithms are based on the input/output labeled transition system formalism, which is particularly appropriate for modeling applications involving asynchronous communication. The method is eminently compatible with classical OO development processes since it can be used to synthesize test cases from the scenarios used in early development stages to model global interactions between actors and components, instead of these test cases being derived manually. We illustrate the system test synthesis process using an air traffic control software example 相似文献
11.
The model-based analysis is receiving a wide acceptance as compare to code-based analysis in the context of prioritizing and guiding the testing effort and speeding up the development process. Ordinarily, system analysts as well as developers follow Unified Modeling Language (UML) activity diagrams to render all realizable flows of controls commonly recognized as scenarios of use cases. This paper applies a bio-inspired algorithm to produce test scenarios for the concurrent section in UML activity diagram. Here, the heuristic draws its inspiration from the internal mechanism of the slime mould Physarum Polycephalum, a large single-celled amoeboid organism. Simulations are performed using eight subject systems taken from the LINDHOLMEN data-set, two models taken from real life student projects and five synthetic models. The results obtained through different approaches are validated through the statistical analysis which demonstrates that our proposed approach is better than the existing Ant Colony Optimization (ACO) and Genetic Algorithm (GA) by a number of feasible test scenarios generated. 相似文献
12.
在大规模的分布环境下,尤其是当部分网络处于偶联的状态下,数据的分布和访问引发了相当的理论和实践问题.本文从全国人口信息系统的范例出发,提出并定义了数据的典型树状结构的分布,并对该分布模型作出了详细的规范说明. 相似文献
13.
14.
15.
16.
云计算在简化用户访问资源方式的同时导致了支撑系统开发部署的复杂,软件错误、部署管理失误导致的拜占庭故障已经成为影响系统可靠性的重要原因.对于在大部分运行周期都满足良性故障模型的系统,拜占庭容错协议在通信复杂度、安全等方面的开销以及其在攻击场景下性能鲁棒性方面的缺陷都限制了其在实际系统中的使用.如何满足实际系统对多种故障模型的需求,已经成为系统设计的一个重要问题.针对这一现状,设计了Nova-BFT,一种有效支持多种故障模型的副本状态机协议,通过牺牲部分峰值吞吐率的方式满足拜占庭容错协议对性能鲁棒性的要求,采用配置参数方式自适应满足良性故障的性能需求.实验表明,Nova-BFT在拜占庭故障模型下吞吐率为4~5 kop/s,同时其对良性故障模型的支持可以有效满足大多数实际应用的需求. 相似文献
17.
分布式状态机(DSM)是一个分布式计算模型,特别适用于反应系统,有广泛的用途,但一般其正确性证明与模型检验的复杂性却很高,不易实用。作者曾提出了一个DSM的代数模型及其模型检验算法,复杂较低,但模型推导过程有点问题。该文加强了对DSM模型检验问题的提法,研究了解的结构特征,证明了可将DSM模型检验问题归结为不动点计算问题,并将Cleaveland和Steffen求不动点的方法用于同步模型不动点计算过程,然后将Bertsekas关于欧氏空间上的异步收敛定理推广到完备格上,从而将求解异步DSM方程不动点问题转化为求解同步方程不动点问题,证明了在适当的条件下,有vgEA=vgES,vgES与vgEA分别是DSM同步方程与异步方程的大不同动点,该同步算法的复杂性为O(|S|log|TRAN|),S为状态集,TRAN为转移关系式集,利用本文结果,可以有效地克服了DSM进程之间的并发干扰所带来的各种困难,对分布式反应系统的可靠设计有很大的帮助。 相似文献
18.
针对目前互联网核心路由器所遇到的计算能力和存储压力过大等问题,本文设计了一种分布式BGP协议的实现框架。通过使用该技术,符合C-BGP内部通信规范的多个BGP实体将构成一个集合。该集合对外表现成一台单独的完整的BGP路由器,在内部则把邻居会话分别分配到不同的BGP实体上,从而充分利用集群的分布式计算资源和存储资源,以提高协议的性能。 相似文献
19.
分布式SCADA系统的UML建模分析与设计 总被引:3,自引:0,他引:3
对一个分布式SCADA系统的控制中心的软件系统,运用面向对象的方法,采用UML作为建模语言进行分析设计,开发了分布式的、面向对象的、可维护性好的系统.研究了应用UML开发大型分布式SCADA系统过程中的一些关键策略. 相似文献
20.
Motahari-Nezhad Hamid R. Saint-Paul R gis Benatallah Boualem Casati Fabio 《Knowledge and Data Engineering, IEEE Transactions on》2008,20(12):1683-1698
Understanding the business (interaction) protocol supported by a service is very important for both clients and service providers: it allows developers to know how to write clients that interact with a service, and it allows development tools and runtime middleware to deliver functionality that simplifies the service development lifecycle. It also greatly facilitates the monitoring, visualization, and aggregation of interaction data. This paper presents an approach for discovering protocol definitions from real-world service interaction logs. It first describes the challenges in protocol discovery in such a context. Then, it presents a novel discovery algorithm, which is widely applicable, robust to different kinds of imperfections often present in realworld service logs, and able to derive protocols of small sizes, also thanks to heuristics. As finding the most precise and the smallest model is algorithmically not feasible from imperfect service logs, finally, the paper presents an approach to refine the discovered protocol via user interaction, to compensate for possible imprecision introduced in the discovered model. The approach has been implemented and experimental results show its viability on both synthetic and real-world datasets. 相似文献