共查询到20条相似文献,搜索用时 31 毫秒
1.
A formal approach based on UML and B for the specification and development of database applications 总被引:1,自引:0,他引:1
This article describes a formal approach to specify and develop database applications. This approach consists of two complementary
phases. In the first phase, B specifications are automatically generated from UML class, state and collaboration diagrams
describing the data and the transactions of the system we are developing. In the second phase, these specifications are successively
refined until they become close enough to a relational implementation. The tool supporting this approach is implemented as
an extension of the Rational Rose tool to develop and visualize graphical (UML) and formal (B) notations in a single environment. 相似文献
2.
The development of user interfaces for safety critical systems is driven by requirements specifications. Because user interface
specifications are typically embedded within complex systems requirements specifications, they can be intractable to manage.
Proprietary requirements specification tools do not support the user interface designer in modelling and specifying the user
interface. In this paper, a new way of working with embedded user interface specifications is proposed, exploiting sequence
diagrams with a hypertext structure for representing and retrieving use cases. This new tool concept is assessed through an
application to the requirements specification for the Airbus A380 air traffic control Datalink system; engineers involved
in the development of the Airbus cockpit used a prototype of the tool concept to resolve a set of user interface design anomalies
in the requirements specification. The results of the study are positive and indicate the user interface to requirements specification
tools which user interface designers themselves need. 相似文献
3.
4.
5.
实时系统动态行为模型的一种形式分析方法* 总被引:1,自引:0,他引:1
提出了一种基于统一建模语言UML 2.0的实时系统动态行为模型的形式分析方法。首先给出了UML顺序图的形式化描述,分析了UML顺序图中事件之间的关系;在此基础上,给出一种对象自动机来描述每个对象在UML顺序图描述的场景中所参与的事件序列的方法,并将该方法扩展到带有组合片段的UML 2.0顺序图;最后通过分析UML 2.0顺序图中的时间建模机制,给出了从UML 2.0顺序图中提取时间约束得到时间自动机的算法。 相似文献
6.
UMLTGF:一个基于灰盒方法从UML活动图生成测试用例的工具 总被引:8,自引:0,他引:8
UML已经成为建模语言的事实标准,如何从UML分析设计模型生成测试用例也为面向对象软件测试带来了新的挑战.为了从UML设计模型中的活动图直接生成测试用例,给出了UML活动图的形式化定义和灰盒测试方法.该方法首先分析UML活动图上的所有执行路径(每条路径称为一个测试场景),然后根据测试场景中的节点和转换所代表的活动及其输入/输出变量、相关约束条件等生成测试用例.并根据该方法实现了一个自动生成测试用例的工具UMLTGF,它可以从Rational Rose的规约文件中提取活动图信息并生成相应的测试用例.该工具能够提高软件测试的效率,降低测试成本. 相似文献
7.
用UML和Object-Z描述交互式系统的接口规格说明 总被引:4,自引:0,他引:4
随着图形用户界面的普及,交互已成为目前软件系统的一个重要特征。与传统的基于字符界面的软件系统相比,基于图形用户界面的软件系统,从某种程序上可看作是一个交互式系统。形式化的规格说明具有精确性,无二义性和一致性等优点,用形式化说明语言来描述交互式系统用户接口的规格说明有很强的实用价值。由于形式化的规格说明的可读很差,因此可以采用标准的对象建模UML来帮助对形式化规格说明的理解。 相似文献
8.
Round-Trip Prototyping Based on Integrated Functional and User Interface Requirements Specifications
Requirements engineering in the new millennium is facing an increasing diversity of computerised devices comprising an increasing
diversity of interaction styles for an increasing diversity of user groups. Thus the incorporation of user interface requirements
into software requirements specifications becomes more and more mandatory. Validating these requirements specifications with
hand-made, throw-away prototypes is not only expensive, but also bears the danger that validation results are not accurately
fed back into the requirements specification. In this paper, we propose an enhancement of the requirements specification method
SCORES for an explicit capturing of user interface requirements. The advantages of the approach are threefold. First, the
user interface requirements specification is UML-compliant and integrated into the functional requirements specification.
Second, prototypes for validation purposes can semi-automatically be generated. Third, the model-based generation of prototypes
allows for ‘round-trip prototyping’ such that manual changes of the prototype during the validation process are automatically
fed back into the requirements specification. 相似文献
9.
This paper addresses the graphical representation of static aspects of B specifications, using UML class diagrams. These diagrams
can help understand the specification for stakeholders who are not familiar with the B method, such as customers or certification
authorities. The paper first discusses some rules for a preliminary derivation of a class diagram. It then studies the consistency
of the concepts preliminarily identified from an object oriented point of view. A formal concept analysis technique is used
to distinguish between consistent classes, attributes, associations and operations. The proposed technique is to incrementally
add operations to the formal specification which automatically result in evolutions of the class diagram. 相似文献
10.
Using formal metamodels to check consistency of functional views in information systems specification 总被引:1,自引:0,他引:1
UML notations require adaptation for applications such as Information Systems (IS). Thus we have defined IS-UML. The purpose of this article is twofold. First, we propose an extension to this language to deal with functional aspects of IS. We use two views to specify IS transactions: the first one is defined as a combination of behavioural UML diagrams (collaboration and state diagrams), and the second one is based on the definition of specific classes of an extended class diagram. The final objective of the article is to consider consistency issues between the various diagrams of an IS-UML specification. In common with other UML languages, we use a metamodel to define IS-UML. We use class diagrams to summarize the metamodel structure and a formal language, B, for the full metamodel. This allows us to formally express consistency checks and mapping rules between specific metamodel concepts. 相似文献
11.
带OCL约束条件的类图到Object-Z规格说明的转换 总被引:1,自引:0,他引:1
如何提高软件的可靠性是目前软件研究领域的一个热点。将形式化方法和主流的软件开发方法相结合是一个可行的方法。本文研究UML语言和Object-Z语言相结合的方法,为主流的软件开发人员所使用的图形化规格说明技术与形式方法提供的精确的分析和验证技术架起了一座桥梁。本文定义如何将带0CL约束条件的类图转换到Object-Z规格说明的方法。这样不仅可以通过支持Object-Z语言的工具采对UML语言描述的系统性质进行验证和确认,而且能够帮助规格说明人员方便地构造Object-Z规格说明。 相似文献
12.
Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker 总被引:8,自引:0,他引:8
Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modelling
Language (UML). In this paper we present a translation from a subset of UML Statechart Diagrams - covering essential aspects
of both concurrent behaviour, like sequentialisation, parallelism, non-determinism and priority, and state refinement - into
PROMELA, the specification language of the SPIN model checker. SPIN is one of the most advanced analysis and verification
tools available nowadays. Our translation allows for the automatic verification of UML Statechart Diagrams. The translation
is simple, proven correct, and promising in terms of state space representation efficiency.
Received September 1999 / Accepted in revised form February 2000 相似文献
13.
J. Milhau A. Idani R. Laleau M. A. Labiadh Y. Ledru M. Frappier 《Innovations in Systems and Software Engineering》2011,7(4):303-313
Combination of formal and semi-formal methods is more and more required to produce specifications that can be, on the one
hand, understood and thus validated by both designers and users and, on the other hand, precise enough to be verified by formal
methods. This motivates our aim to use these complementary paradigms in order to deal with security aspects of information
systems. This paper presents a methodology to specify access control policies starting with a set of graphical diagrams: UML
for the functional model, SecureUML for static access control and ASTD for dynamic access control. These diagrams are then
translated into a set of B machines. Finally, we present the formal specification of an access control filter that coordinates
the different kinds of access control rules and the specification of functional operations. The goal of such B specifications
is to rigorously check the access control policy of an information system taking advantage of tools from the B method. 相似文献
14.
Cyber physical systems (CPSs) can be found nowadays in various fields of activity. The increased interest for these systems as evidenced by the large number of applications led to complex research regarding the most suitable methods for design and development. A promising solution for specification, visualization, and documentation of CPSs uses the Object Management Group (OMG) unified modeling language (UML). UML models allow an intuitive approach for embedded systems design, helping end-users to specify the requirements. However, the UML models are represented in an informal language. Therefore, it is difficult to verify the correctness and completeness of a system design. The object constraint language (OCL) was defined to add constraints to UML, but it is deficient in strict notations of mathematics and logic that permits rigorous analysis and reasoning about the specifications. In this paper, we investigated how CPS applications modeled using UML deployment diagrams could be formally expressed and verified. We used Z language constructs and prototype verification system (PVS) as formal verification tools. Considering some relevant case studies presented in the literature, we investigated the opportunity of using this approach for validation of static properties in CPS UML models. 相似文献
15.
D. Mouheb D. Alhadidi M. Nouh M. Debbabi L. Wang M. Pourzandi 《Innovations in Systems and Software Engineering》2016,12(1):41-67
Aspect-oriented modeling (AOM) emerged as a promising paradigm for handling crosscutting concerns, such as security, at the software modeling level. Most existing AOM contributions are presented from a practical perspective and lack formal syntax and semantics. In this paper, we present a practical and formal AOM framework for software security hardening. Our contributions are threefold. First, we define an AOM approach for the specification of security aspects at the unified modeling language (UML) design level. Second, we design and implement the matching and the weaving processes into UML design models. Third, we elaborate formal specifications for aspect matching and weaving in UML activity diagrams. Finally, we demonstrate the viability and the relevance of our propositions using a case study. The proposed framework is supported by a tool built on top of IBM-Rational Software Modeler. 相似文献
16.
An approach to applying SOFL for agile process and its application in developing a test support tool
Shaoying Liu 《Innovations in Systems and Software Engineering》2010,6(1-2):137-143
Structured Object-Oriented Formal Language (SOFL) is a representative formal engineering method for software development. It offers a three-step specification approach to constructing formal specifications, and specification-based inspection and testing for verification and validation. In this paper, we describe a novel approach to applying the SOFL method to achieve agile development process. This approach results from our experience in several collaboration projects with industry, and aims to strike a balance between the fast delivery of software product and the assurance of its quality. We have tested the approach in developing a prototype test support tool. 相似文献
17.
Andreas Bollin 《Innovations in Systems and Software Engineering》2011,7(4):283-292
Due to their accuracy in describing systems, formal specifications can play an important role during forward as well as reverse
engineering activities. However, besides dense mathematical expressions, their lack in visually appealing notations impedes
their use and exchange among different stakeholders. One solution to this problem is to enrich the specification by other
views, in most cases Unified Modelling Language (UML) diagrams. But the mapping is not trivial, and existing approaches have
their impediments, among them the assignment of methods to classes—which has to be re-done by hand quite often. By the example
of Z, this paper demonstrates that the situation can be improved. The new approach combines existing mapping strategies, but
additionally lets the assignment of methods rest on quality-related measures. The basic idea is to balance the values of coupling
for all methods within and between the UML classes. With that, two issues are addressed: firstly, the mapping of sets, types,
and operations (to UML classes and UML methods) is based on reproducible measures that are intuitively comprehensible. Secondly,
implementations based on the resulting UML class diagrams very likely also have comparable quality-related properties. 相似文献
18.
基于一致性测试理论的Statechart描述的测试用例自动生成 总被引:1,自引:0,他引:1
本文研究Statechart描述的测试语义和测试用例的自动生成.基于Tretmans的从标记转换系统描述自动生成测试用例的方法,我们研究如何从Statechart描述自动生成测试用例.本文的主要贡献在于建立了基于Statechart描述的一致性测试和测试用例生成的形式化基础.为Statechart描述建立了形式化测试语... 相似文献
19.
20.
在基于组件的软件开放方式(CBD)下,软件系统是一些盯互联系的可重用组件的集合,因此需要对系统的每一个组件以及组件之间的相互关系有很好的理解。UML作为一种标准建模语言,不仅可以支持面向对象的分析与设计,而且能够有力地支持从需求分析开始的软件开发全过程。但是UML对组件建模的支持并不理想,这就需要开发一种能很好支持组件建模的方法。本文提出一种用UML描述组件规格说明的方法。将组件规格说明分解成组件接口规格说明。通过对组件的每个接口和组件接口之间的相互关系加以形式描述,从而达到组件规格说明的清晰性和精确性。 相似文献