Writing and executing ODP computational viewpoint specifications using Maude

The Reference Model of Open Distributed Processing (RM-ODP) is a joint standardization effort by ITU-T and ISO/IEC for the specification of large open distributed systems. RM-ODP is becoming increasingly relevant now because the size and complexity of large distributed systems is challenging current software engineering methods and tools, and because international standards have become key to achieve the required interoperability between the different parties and organizations involved in the design and development of complex systems. RM-ODP defines five viewpoints for decomposing the design activity into separate areas of concern. One of the RM-ODP viewpoints, the computational viewpoint, focuses on the basic functionality of the system and its environment, independently of its distribution. Although several notations have been proposed to model the ODP computational viewpoint, either they are not expressive enough to faithfully represent all its concepts, or they tend to suffer from a lack of formal support. In this paper we introduce the use of Maude as a formal notation for writing and executing ODP computational viewpoint specifications. Maude is an executable rewriting logic language specially 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 computational viewpoint concepts, allows the execution of the specifications produced, and offers good tool support for reasoning about them.     

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.     

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.     

视频点播系统的开放式分布处理视点

1 引言分布式多媒体系统是计算机网络技术、通信技术、多媒体信息处理技术、分布计算技术、数据压缩技术等众多技术相互结合的产物,其应用已涉及相当多的领域,如教育、办公、新闻、出版、医疗、金融、计算机支持协同工作(CSCW)等。分布式多媒体系统中一个十分重要的应用是视频点播(VOD),它将远程视频服务器上的媒体信息,通过计算机网络或其它通信设施传送到本地的媒体处理器和媒体终点上。本文利用ODP(开放式分布处理)方法讨论了VOD实验系统的设计。     

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

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

Model-based specification

The classical specification formalism involving pre- and postconditions expressed in program variables cannot directly be applied to the specification of classes, interfaces, components, and design patterns, since the program variables involved are mostly invisible outside of (dynamically selected) implementation code. A more useful specification formalism, operating at the problem domain level rather than at the implementation level, is proposed and it is shown how this can be used for Dijkstra-style derivation of object-oriented code.     

ODP.NET访问ORACLE的方法

ODP.NET是专用的.NET访问ORACLE的高效方法.本文描述了ODP.NET的主要特性和结构并通过例子介绍了它的使用方法.     

Modular grammar specification

We establish a semantics for building grammars from a modularised specification in which modules are able to delete productions from imported nonterminals. Modules have import lists of nonterminals; some or all of an imported nonterminal's productions may be suppressed at import time. There are two basic import mechanisms which (a) reference or (b) clone an imported nonterminal's productions. One of our goals is to allow a precise answer to the question: ‘what character level language does this grammar generate’ in the face of difficult issues such as the mutual embedding of languages that have different whitespace and commenting conventions. Our technique is to automatically generate a character level grammar from grammars written at token level in the conventional way; the grammar is constructed from modules each of which may have its own whitespace convention.     

Practical interface specification

Although software development based on modules is now widely practiced and taught, specification of module interfaces has received far less acceptance. Languages such as Ada and Modula-2 require an interface specification, but it is syntactic, merely listing the exported procedures and functions and their signatures. No semantic information is given, leaving the effect of each call on the return value of other calls unspecified. Module users must either guess the interface semantics or infer them from the module implementation, seriously compromising the value of the modular approach. Formal methods, such as the algebraic and trace approaches, do specify interface semantics, but have proved difficult to teach and to apply in practice. In this paper we present the software cost reduction (SCR) method for specifying the syntax and semantics of the module interface. We describe the basic approach and illustrate it on simple, but complete examples. We describe and demonstrate the additional features and techniques we have introduced to handle more complex problems. We also show the precise relationship between the SCR and trace techniques by presenting a method for converting any SCR specification to an equivalent trace specification.     

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

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

ODAC: An Agent-Oriented Methodology Based on ODP

The ODAC methodology (Open Distributed Applications Construction) aims to provide a designer of agent-based systems with a set of methods and tools to allow him/her to control the construction process complexity of such systems. It enables software engineers to specify agent-based systems that will be implemented within an execution environment, for example a mobile agent platform. Our work is based on the Open Distributed Processing (ODP) standards and the agent paradigm.     

The burglar's viewpoint

Unwittingly, computing centre personnel may encourage potential burglars by supplying tools which threaten system integrity. Because system support staff and burglars seem to have goals in common, the activities of the former could give the latter a distinct advantage in violating security barriers. real-life examples will clarify the risks involved in customary computing centre practice. Aspects of an effective security policy will be presented.     

用ODP视点分析常见网络管理模型

本文运用ODP的分析方法对基于SNMP和CMIP以及分布式的网络管理系统模型进行分析,从信息和计算视点进行对比,找出各自的特点和不足,得出网络管理系统发展的一般趋势以及需要解决的问题,为以后网络管理系统的实施提供参考。     

Real-time specification using Lucid

A methodology is presented for transforming a functional specification written in Lucid to an equivalent specification that captures its real-time properties. The enhanced specification consists of a set of equations that can be solved for several properties, including execution time and external requirements, or may simply be checked for the existence of a solution. Lucid has a set of meaning-preserving transformations, and a proof system corresponding to a behavioral semantics has been constructed. Both of these tools can be used to reason about properties of the specification. The specification is executable and can be used as a prototype for the system being specified. It is possible to express architectural constraints within the same formal framework. Thus this type of specification can be used to guide the development of new real-time systems     

Improving the TCPA specification

The Trusted Computing Platform Alliance (TCPA) specification is a new computing platform for the next century that will provide for improved trust in the PC platform. Improving information security is an important and timely goal, but not at the cost of further weakening fair use doctrine, encouraging anticompetitive behavior, or eliminating privacy. Unfortunately, the current specification does not meet this standard.     

Incremental requirements specification withLotos

The importance of formally and incrementally specifying requirements is discussed. An approach based on LOTOS (Language Of Temporal Ordering Specification) is proposed that exploits desirable characteristics of the constraint-oriented style. The nature of constraint-oriented specification is discussed at some length, and guidelines for how to use it effectively with LOTOS are presented. Small introductory examples lead to the incremental specification of a file access system using the approach in the paper. It is shown how the requirements for the file access system can be gradually formalised, leading to a complete system specification.     

SoC系统级描述语言SpecC

讨论了SoC系统描述的要求,针对这些要求指出了目前系统级描述语言的不足之处,然后分别从层次化,同步、异常处理、时序等几个方面详细介绍一种能满足SoC系统所有描述要求的系统级描述语言--SpecC语言.将SpccC语言和其它系统级描述语言在系统描述能力和可综合性等多个方面进行比较,结果表明,SpecC语言在系统级描述方面具有明显的优势.     

Interpretable program specification language

In the paper, a domain-specific language of executable specifications is proposed. This language makes it possible to describe models of formalized subject domains in a graphical form, formulate computational problems on these models, and synthesize programs for solving these problems (including parallel ones) based on deductive inference in a special class of proposition calculus.