The RAISE language,method and tools

This paper presents the RAISE¹ software development method, its associated specification language, and the tools supporting it. The RAISE method enables the stepwise development of both sequential and concurrent software from abstract specification through design to implementation. All stages of RAISE software development are expressed in the wide-spectrum RAISE specification language. The RAISE tools form an integrated tool environment supporting both language and method.The paper surveys RAISE and furthermore, more detailed presentations of major RAISE results are provided. The subjects of these are (a) an example of the use of the RAISE method and language, and (b) a presentation of the mathematical semantics of the RAISE specification language.     

基于RSL的协议形式化描述与验证方法

讨论使用RAISE规范语言（RSL）描述6种协议元素的方法。在RSL描述的基础上,借助操作符的运算规则、并行扩展规则和同步会合事件隐藏规则,对协议的相关性质进行验证,以一个简化的停止等待协议规范的描述和验证实例证明,与其他形式化方法相比,RSL表现出较强的描述能力。     

Study of Copper Substitute in High Copper Price Market Environment

【正】The high price of copper drives up industry cost,also it is difficult for terminal products to raise price to transfer the cost pressure brought by increase ...     

Specification,proof, and model checking of the Mondex electronic purse using RAISE

This paper describes how the communication protocol of Mondex electronic purses can be specified and verified against desired security properties. The specification is developed by stepwise refinement using the RAISE formal specification language, RSL, and the proofs are made by translation to PVS and SAL. The work is part of a year-long project contributing to the international grand challenge in verified software engineering. J. C. P. Woodcock     

UML状态机模型元素的RSL形式化定义

UML状态机作为UML动态描述机制的重要组成部分,在描述系统及模型的动态行为时扮演着重要的角色,但已有的UML动态语义缺乏准确的形式化描述。首先将UML状态机抽象成图;再将图通过传统的有穷自动机进行语义扩展,同时增加状态分层,形成一个基于UML状态机的有穷自动机;然后用RAISE规约语言RSL对扩展后的自动机进行形式化定义,使UML状态机中的模型元素的语义更加清晰、精确,为后期的UML状态机的操作语义形式化研究打下基础。     

形式化与可视化结合的FDOOM软件开发方法

It is an important issue in Software Engineering that combines the formal development method with the vi-sual development method. This study is based on the transform method and rules between the UML model and the RAISE model.We developes a new software development Method FDOOM (Formal Development based on Object Oriented Modeling) that combine the UML with the RAISE together. And there is a demo in the end.     

D-Ocean: an unstructured data management system for data ocean environment

Together with the big datamovement,many organizations collect their own big data and build distinctive applications. In order to provide smart services upon big data, massive variable data should be well linked and organized to form Data Ocean, which specially emphasizes the deep exploration of the relationships among unstructured data to support smart services. Currently, almost all of these applications have to deal with unstructured data by integrating various analysis and search techniques upon massive storage and processing infrastructure at the application level, which greatly increase the difficulty and cost of application development.This paper presents D-Ocean, an unstructured data management system for data ocean environment. D-Ocean has an open and scalable architecture, which consists of a core platform, pluggable components and auxiliary tools. It exploits a unified storage framework to store data in different kinds of data stores, integrates batch and incremental processing mechanisms to process unstructured data, and provides a combined search engine to conduct compound queries. Furthermore, a so-called RAISE process modeling is proposed to support the whole process of Repository, Analysis, Index, Search and Environment modeling, which can greatly simplify application development. The experiments and use cases in production demonstrate the efficiency and usability of D-Ocean.     

Developing a Domain Model for Relay Circuits

In this paper we stepwise develop a domain model for relay circuits as used in railway control systems. First we provide an abstract, property-oriented model of networks consisting of components that can be glued together with connectors. This model is strongly inspired by a network model for railways made by Bj.rner et. al., however our model is more general: the components can be of any kind and can later be re.ned to e.g. railway components or circuit components. Then we show how the abstract network model can be re.ned into an explicit model for relay circuits. The circuit model describes the statics as well as the dynamics of relay circuits, i.e. how a relay circuit can be composed legally from electrical components as well as how the components may change state over time. Finally the circuit model is transformed into an executable model, and we show how a concrete circuit can be de.ned, checked to be legal, and the reaction to an input can be simulated.     

使用延时演算的时间化RSL的指称语义

使用扩展的持续时间演算(EDC)模型,给出了时间化的RAISE描述语言(RSL)的一个子集的指称语义.在扩展的持续时间演算模型中加入了一些新的特征,并探究了它们的代数定律.这些定律在形式化实时程序和验证实时性质中起着重要作用.最后还给出了时间化RSL的一些代数定律.这些定律可以从其指称语义证明,并用于程序的转化和优化.     

结合UML和RAISE的软件开发方法研究

面向对象方法形象、直观、使用方便,但难以消除二义性。形式化方法严密、可靠、可验证,但软件规约不直观,不符合开发人员的使用习惯,探讨一种结合面向对象方法UML和形式化方法RAISE的软件开发方法。