Using Maude to write and execute ODP information viewpoint specifications

The aim of the open distributed processing (ODP) information viewpoint is to describe the semantics of the information and of the information processing in a system, from a global point of view, without having to worry about other considerations, such as how the information will be finally distributed or implemented or the technology used to achieve such implementation. Although several notations have been proposed to model this ODP viewpoint, they are not expressive enough to faithfully represent all the information concepts, or they tend to suffer from a lack of (formal) support, or both. In this paper, we explore the use of Maude as a formal notation for writing ODP information specifications. Maude is an executable rewriting logic language especially well suited for the specification of object-oriented open and distributed systems. We show how Maude offers a simple, natural, and accurate way of modeling the ODP information viewpoint concepts, allows the execution of the specifications produced, and offers good tool support for reasoning about them.     

ODP enterprise viewpoint specification

The Open Distributed Processing (ODP) standardisation initiative has led to a framework by which distributed systems can be modelled using a number of viewpoints. These include an enterprise viewpoint, which focuses on the objectives and policies of the enterprise that the system is meant to support. Although the ODP reference model provides abstract languages of relevant concepts, it does not prescribe particular techniques that are to be used in the individual viewpoints. In particular, there is a need to develop appropriate notations for ODP enterprise specification, in order to increase the applicability of the ODP framework. In this paper, we tackle this concern and develop a specification language to support the current draft of the enterprise viewpoint. In doing so, we analyse the current definition of the ODP enterprise viewpoint language. Using the Unified Modelling Language (uml), a meta-model of the core concepts and their relationships is constructed, and we also investigate to what extent the uml can be used for enterprise viewpoint specification. We, then, focus on the expression of enterprise policies that govern the behaviour of enterprise objects. We develop a policy language, which is a combination of structured English and simple predicate logic and is built on top of the formal object-oriented specification language Object-Z, into which the complete language is translated. We illustrate the ideas in the paper with a case study that presents an enterprise specification of a library support system.     

An approach to a Z toolkit for the Reference Model of Open Distributed Processing

We discuss the usage of the (non-OO) Z specification language to represent some fundamental concepts of the ISO Reference Model of Open Distributed Processing (RM-ODP) and the ISO General Relationship Model (GRM). After discussing some of the difficulties involved, we offer suggestions on how Z can be used successfully for specifying and modeling open object-based distributed systems. Although fundamental specification concepts of RM-ODP and GRM are less well-known than “traditional” mathematics, we propose an RM-ODP toolkit somewhat analogous in its usage to the well-known mathematical toolkit in Z.     

开放分布式处理及其实例

迅速发展的计算机与通信技术使得构造大型分布式系统成为可能,尽管如此,互连系统特别是     

UML在分布式系统中的应用与研究

ＵＭＬ（Ｕｎｉｆｉｅｄ　 Ｍｏｄｅｌｉｎｇ 　Ｌａｎｇｕａｇｅ）是一种标准的、功能强大的建模语言。ＩＳＯ ＲＭ－ＯＤＰ（ＩＳＯ开放分布式处理参考模型）为开放、灵活的分布式系统提供了主框架。文章提出了一种用ＵＭＬ为ＯＤＰ系统建模的方法,它以ＯＤＰ的概念和ＵＭＬ的符号为基础。     

ODP系统中的观点及观点规范语言

开放分布式处理ＯＤＰ的目标是给应用程序间提供一个一致的接口模型，以实现分布透明性、互操作性和可移植性。开放分布式参考模型ＩＳＯ ＲＭ－ＯＤＰ提供了一个分布式系统的框架，从五个不同的观点描述ＯＤＰ系统，并提出相应的规范语言的概念和构造规则以便对该观点进行描述，本文首先介绍了这五种观点及相应的规范语言的概念和构造规则，并讨论了它们之间的关系。     

Semantics and pragmatics of Real-Time Maude

At present, designers of real-time systems face a dilemma between expressiveness and automatic verification: if they can specify some aspects of their system in some automaton-based formalism, then automatic verification is possible; but more complex system components may be hard or impossible to express in such decidable formalisms. These more complex components may still be simulated; but there is then little support for their formal analysis. The main goal of Real-Time Maude is to provide a way out of this dilemma, while complementing both decision procedures and simulation tools. Real-Time Maude emphasizes ease and generality of specification, including support for distributed real-time object-based systems. Because of its generality, falling outside of decidable system classes, the formal analyses supported—including symbolic simulation, breadth-first search for failures of safety properties, and model checking of time-bounded temporal logic properties—are in general incomplete (although they are complete for discrete time). These analysis techniques have been shown useful in finding subtle bugs of complex systems, clearly outside the scope of current decision procedures. This paper describes both the semantics of Real-Time Maude specifications, and of the formal analyses supported by the tool. It also explains the tool's pragmatics, both in the use of its features, and in its application to concrete examples.     

An application of the Reference Model for Open Distributed Processing to electronic brokerage

This paper presents the design of an Architecture for Electronic Brokerage Systems (AEBS). This architecture is based on the Reference Model for Open Distributed Processing (RM-ODP) model. It specifies a brokerage system from five RM-ODP viewpoints. AEBS include a generic model of electronic brokerage. It defines protocols and interfaces between actors. It enables communication between actors via an advanced object-oriented interface (defined in terms of the Common Object Request Broker Architecture (CORBA) technology) as well as using traditional trading protocols. These interfaces allow a broker to operate in both the rapidly developing object-oriented CORBA environment and the electronic markets based on customary protocols. CORBA was also used for the design of the internal object model and internal interfaces of a brokerage system. This paper focuses primarily on the specification of the AEBS architecture from the enterprise and computational viewpoints of the RM-ODP model.     

Maude: specification and programming in rewriting logic

Maude is a high-level language and a high-performance system supporting executable specification and declarative programming in rewriting logic. Since rewriting logic contains equational logic, Maude also supports equational specification and programming in its sublanguage of functional modules and theories. The underlying equational logic chosen for Maude is membership equational logic, that has sorts, subsorts, operator overloading, and partiality definable by membership and equality conditions. Rewriting logic is reflective, in the sense of being able to express its own metalevel at the object level. Reflection is systematically exploited in Maude endowing the language with powerful metaprogramming capabilities, including both user-definable module operations and declarative strategies to guide the deduction process. This paper explains and illustrates with examples the main concepts of Maude's language design, including its underlying logic, functional, system and object-oriented modules, as well as parameterized modules, theories, and views. We also explain how Maude supports reflection, metaprogramming and internal strategies. The paper outlines the principles underlying the Maude system implementation, including its semicompilation techniques. We conclude with some remarks about applications, work on a formal environment for Maude, and a mobile language extension of Maude.     

An RM-ODP enterprise view for spatial data infrastructures

Spatial Data Infrastructures (SDIs) are large, open, distributed and standards-based information systems which intend to facilitate and promote the use of spatial data and spatial services on the Internet. Spatial data describe information tied with locations on Earth, while spatial services allow to manipulate spatial data following a Service Oriented Architecture. This paper proposes to model SDIs as federations of autonomous communities following the enterprise language of the ITU-T and ISO/IEC ‘Reference Model of Open Distributed Processing’ (RM-ODP), and the recently approved ‘Use of UML for ODP Systems Specifications’ (UML4ODP). The enterprise language of the RM-ODP provides a conceptual foundation to address several aspects of SDIs not previously considered from a systems architecture point of view. The use of UML4ODP provides a modeling language to facilitate the exchange of knowledge about SDI, and it is an opportunity to try this recent standard for a class of large and complex systems.     

Specification and design of shared resource arbitration

The specification, modular design and verification of distributed communicating systems is demonstrated by an example. The scheduling of the access to a common shared resource by a finite number of devices with priorities is a well known problem from hardware and operating systems design. Using the concepts of stream processing continuous function a variety of formal requirement and design specifications for this problem are given and the design specifications are proven correct w.r.t the requirement specifications. From the design specifications one can immediately read off applicative programs implementing the requirement specifications. Special attention is paid to the aspect of modelling time.     

Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude

This paper describes the application of the Real-Time Maude tool and the Maude formal methodology to the specification and analysis of the AER/NCA suite of active network multicast protocol components. Because of the time-sensitive and resource-sensitive behavior, the presence of probabilistic algorithms, and the composability of its components, AER/NCA poses challenging new problems for its formal specification and analysis. Real-Time Maude is a natural extension of the Maude rewriting logic language and tool for the specification and analysis of real-time object-based distributed systems. It supports a wide spectrum of formal methods, including: executable specification; symbolic simulation; breadth-first search for failures of safety properties in infinite-state systems; and linear temporal logic model checking of time-bounded temporal logic formulas. These methods complement those offered by network simulators on the one hand, and timed-automaton-based tools and general-purpose theorem provers on the other. Our experience shows that Real-Time Maude is well-suited to meet the AER/NCA modeling challenges, and that its methods have proved effective in uncovering subtle and important errors in the informal use case specification.

FDTs for ODP

This paper discusses the use and integration of formal techniques into the Open Distributed Processing (ODP) standardization initiative.

The ODP reference model is a natural progression from OSI. Multiple viewpoints are used to specify complex ODP systems. Formal methods are playing an increasing role within ODP.

We provide an overview of the ODP reference model, before discussing the ODP requirements on FDTs, and the role such techniques play. Finally, we discuss the use of formalisms in the central problem of maintaining cross viewpoint consistency.     

基于MDA的ODP互操作性软件过程研究

利用RM-ODP概念架构，提出了基于MDA的ODP软件过程，将互操作性的实现贯穿于整个系统的开发过程之中：在PIM中设计，在PSM中实现。为了使系统建立在正确的完整的PIM之上，在需求分析阶段采用了EDOC模式进行可视化的建模，在功能设计阶段采用了ELOTOS形式化描述得到PIM。因此，本软件过程实现了ODP系统基于可测试业务模型的互操作性。     

Achieving dependability throughout the development process: adistributed software experiment

Distributed software engineering techniques and methods for improving the specification and testing phases are considered. To examine these issues, an experiment was performed using the design diversity approach in the specification, design, implementation, and testing of distributed software. In the experiment, three diverse formal specifications were used to produce multiple independent implementations of a distributed communication protocol in Ada. The problems encountered in building complex concurrent processing systems in Ada were also studied. Many pitfalls were discovered in mapping the formal specifications into Ada implementations     

用于开放式分布处理的中间件的标准和规范

中间件使得开放式分布处理系统中异种机上的应用可以相互协同工作。     

开放分布式处理ODP参考模型

本文论述开放分布式处理参考模型（ＲＭ－ＯＤＰ）与开放系统互连（ＯＳＩ）参考模型的关系，介绍ＲＭ－ＯＤＰ的主要内容、视图描述方案及一般的建模方法，提供了视图语言的简要概念和规则。最后指出ＯＤＰ五种视图的一致性问题并以实例进行说明     

An Operational Approach to Requirements Specification for Embedded Systems

The approach to requirements specification for embedded systems described in this paper is called "operational" because a requirements specification is an executable model of the proposed system interacting with its environment. The approach is embodied by the language PAISLey, which is motivated and defined herein. Embedded systems are characterized by asynchronous parallelism, even at the requirements level; PAISLey specifications are constructed by interacting processes so that this can be represented directly. Embedded systems are also characterized by urgent performance requirements, and PAISLey offers a formal, but intuitive, treatment of performance.