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.     

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.     

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.     

Embedding domain-specific modelling languages in Maude specifications

We propose a formal approach for the definition and analysis of domain-specific modelling languages (dsml). The approach uses standard model-driven engineering artifacts for defining a language’s syntax (using metamodels) and its operational semantics (using model transformations). We give formal meanings to these artifacts by translating them to the Maude language: metamodels and models are mapped to equational specifications, and model transformations are mapped to rewrite rules between such specifications, which are also expressible in Maude due to Maude’s reflective capabilities. These mappings provide us, on the one hand, with abstract definitions of the mde concepts used for defining dsml, which naturally capture their intended meanings; and, on the other hand, with equivalent executable definitions, which can be directly used by Maude for formal verification. We also study a notion of operational semantics-preserving model transformations, which are model transformations between two dsml that ensure that each execution of a transformed instance is matched by an execution of the original instance. We propose a semi-decision procedure, implemented in Maude, for checking the semantics-preserving property. We also show how the procedure can be adapted for tracing finite executions of the transformed instance back to matching executions of the original one. The approach is illustrated on xspem, a language for describing the execution of activities constrained by time, precedence, and resource availability.     

开放分布式处理及其实例

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

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.     

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

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

Specification Diagrams for Actor Systems

Specification diagrams (SD's) are a novel form of graphical notation for specifying open distributed object systems. The design goal is to define notation for specifying message-passing behavior that is expressive, intuitively understandable, and that has formal semantic underpinnings. The notation generalizes informal notations such as UML's Sequence Diagrams and broadens their applicability to later in the design cycle. Specification diagrams differ from existing actor and process algebra presentations in that they are not executable per se; instead, like logics, they are inherently more biased toward specification. In this paper we rigorously define the language syntax and semantics and give examples that show the expressiveness of the language, how properties of specifications may be asserted diagrammatically, and how it is possible to reason rigorously and modularly about specification diagrams.     

基于重写逻辑的Web服务事务处理形式化描述

Web服务的事务处理研究越来越活跃,对于Web服务中的长、短事务进行形式化描述与验证是很重要的,但目前还没有成熟的方法．该文提出了一种基于重写逻辑的Web服务事务处理形式化描述方法,采用重写逻辑工具Maude,对于描述Web事务的细胞膜演算,给出一个事务处理的通用框架,采用重写逻辑中的规则描述事务的具体活动,并且引入事务补偿机制刻画长事务的运行;并应用该模型形式化描述文中的Web事务经典例子,得到一个可执行的重写逻辑模型,便于以后采用Maude线性时序逻辑分析器进行形式化分析．     

Realizing a TMN

A functional partitioning of a TMN in terms of management functional areas and functional layers is proposed. This new method for classifying TMN functions is used to suggest logical expansions of the function decomposition in ITU-T Recommendation M. 3400. The method is also shown to be a useful tool for graphically comparing the functionality of Operations Systems that are already deployed, showing how they are positioned within a real TMN. Further, the new classification scheme is applied to the representation, in tabular form, of the functions of a particular example of a deployed OS.Industry standard open interfaces using the Common Management Information Service Element (CMISE) in the context of Open Systems Interconnections (OSI) protocols and the Generic Network Information Model are also being implemented. An example of a Q3 interface (between Operations Systems and Network Elements) and an example of an X interface (between different administrative jurisdictions) are discussed.Progress is being made on infrastructure software components that will ease implementations of TMN functions in a distributed processing environment. Future directions, such as the use of evolving Open Distributed Processing (ODP) specifications in distributed network management, are discussed.     

An Overview of the Runtime Verification Tool Java PathExplorer

We present an overview of the Java PathExplorer runtime verification tool, in short referred to as JPAX. JPAX can monitor the execution of a Java program and check that it conforms with a set of user provided properties formulated in temporal logic. JPAX can in addition analyze the program for concurrency errors such as deadlocks and data races. The concurrency analysis requires no user provided specification. The tool facilitates automated instrumentation of a program's bytecode, which when executed will emit an event stream, the execution trace, to an observer. The observer dispatches the incoming event stream to a set of observer processes, each performing a specialized analysis, such as the temporal logic verification, the deadlock analysis and the data race analysis. Temporal logic specifications can be formulated by the user in the Maude rewriting logic, where Maude is a high-speed rewriting system for equational logic, but here extended with executable temporal logic. The Maude rewriting engine is then activated as an event driven monitoring process. Alternatively, temporal specifications can be translated into automata or algorithms that can efficiently check the event stream. JPAX can be used during program testing to gain increased information about program executions, and can potentially furthermore be applied during operation to survey safety critical systems.     

Monitoring Java Programs with Java PathExplorer

We present recent work on the development of Java PathExplorer (JPaX), a tool for monitoring the execution of Java programs. JPaX can be used during program testing to gain increased information about program executions, and can potentially furthermore be applied during operation to survey safety critical systems. The tool facilitates automated instrumentation of a program's byte code, which will then emit events to an observer during its execution. The observer checks the events against user provided high level requirement specifications, for example temporal logic formulae, and against lower level error detection procedures, usually concurrency related such as deadlock and data race algorithms. High level requirement specifications together with their underlying logics are defined in rewriting logic using Maude, and then can either be directly checked using Maude rewriting engine, or be first translated to efficient data structures and then checked in Java.     

Prototyping SOS Meta-theory in Maude

We present a prototype implementation of SOS meta-theory in the Maude term rewriting language. The prototype defines the basic concepts of SOS meta-theory (e.g., transition formulae, deduction rules and transition system specifications) in Maude. Besides the basic definitions, we implement methods for checking the premises of some SOS meta-theorems (e.g., GSOS congruence meta-theorem) in this framework. Furthermore, we define a generic strategy for animating programs and models for semantic specifications in our meta-language. The general goal of this line of research is to develop a general-purpose tool that assists language designers by checking useful properties about the language under definition and by providing a rapid prototyping environment for scrutinizing the actual behavior of programs according to the defined semantics.     

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.     

Towards formal open standards: formalizing a standard’s requirements

Open standardization seems to be very popular among software developers as it simplifies the standard’s adoption by the software engineering. Formal specification methods, while very promising, are being adopted slowly as the industry seems to have little motivation to move into this territory. In this paper the authors present (1) the idea of applying formal specification techniques to open standards’ specifications, and (2) an example of a formal specification of the Rich Site Summary (RSS) v2.0 open standard. The authors provide evidence for the advantages of the open standards formal specification over natural language documentations: formal specifications are more concise, less ambiguous, more complete with respect to the original documentation and, when using certain kinds of specification languages, executable and reusable as they support module inheritance. The merging of formal specification methods and open standards allows (1) a more concrete standard design; (2) an improved understanding of the environment under design; (3) an enforced certain level of precision into the specification, and also (4) provides software engineers with extended property checking/verification capabilities, especially if they opt to use any algebraic specification language. The authors showcase how the RSS standard can be formally specified using an algebraic specification language and demonstrate how can that be beneficial.     

A formal description of open distributed processing (ODP) trading based on guidelines for the definition of managed objects (GDMO)

New requirements of growing computer networks and information systems have an influence on extended client/server models with increased functionality. This forms the basis for service management in distributed systems which is realized by a service trading concept. This paper studies the requirements derived from the Open Distributed Processing (ODP) Reference Model in order to consider an open service market. Furthermore, it examines management possibilities for describing the service trading scenario. Because of similar architectures and properties ODP services, service offers, types, exporters and traders are mapped onto management components and modeled as managed objects. Therefore, the Guidelines for the Definition of Managed Objects (GDMO) are used. The final concept allows a precise and unambiguous study of the service trading scenario and provides means for exporting and importing of service offers in a distributed environment.     

Reduction Semantics and Formal Analysis of Orc Programs

Orc is a language for orchestration of web services developed by J. Misra that offers simple, yet powerful and elegant, constructs to program sophisticated web orchestration applications. The formal semantics of Orc poses interesting challenges, because of its real-time nature and the different priorities of external and internal actions. In this paper, building upon our previous SOS semantics of Orc in rewriting logic, we present a much more efficient reduction semantics of Orc, which is provably equivalent to the SOS semantics thanks to a strong bisimulation. We view this reduction semantics as a key intermediate stage towards a future, provably correct distributed implementation of Orc, and show how it can naturally be extended to a distributed actor-like semantics. We show experiments demonstrating the much better performance of the reduction semantics when compared to the SOS semantics. Using the Maude rewriting logic language, we also illustrate how the reduction semantics can be used to endow Orc with useful formal analysis capabilities, including an LTL model checker. We illustrate these formal analysis features by means of an online auction system, which is modeled as a distributed system of actors that perform Orc computations.     

An algebraic semantics for MOF

In model-driven development, software artifacts are represented as models in order to improve productivity, quality, and cost effectiveness. In this area, the meta-object facility (MOF) standard plays a crucial role as a generic framework within which a wide range of modeling languages can be defined. The MOF standard aims at offering a good basis for model-driven development, providing some of the building concepts that are needed: what is a model, what is a metamodel, what is reflection in the MOF framework, and so on. However, most of these concepts are not yet fully formally defined in the current MOF standard. In this paper we define a reflective, algebraic, executable framework for precise metamodeling based on membership equational logic (mel) that supports the MOF standard. Our framework provides a formal semantics of the following notions: metamodel, model, and conformance of a model to its metamodel. Furthermore, by using the Maude language, which directly supports mel specifications, this formal semantics is executable. This executable semantics has been integrated within the Eclipse modeling framework as a plugin tool called MOMENT2. In this way, formal analyses, such as semantic consistency checks, model checking of invariants and LTL model checking, become available within Eclipse to provide formal support for model-driven development processes.     

Controllability and observability in distributed testing

In developing distributed systems, current trends are towards creating open distributed environments supporting interworking, interoperability, and portability, in spite of heterogeneity and autonomy of related systems. Several reference models, architectures and frameworks such as ODP, CORBA, and TINA, have already been designed and proposed. However, even though models, architectures, and frameworks, provide a good basis for developing working open distributed applications, conformance testing approaches are required for gaining confidence in final products and guaranteeing their integration and interoperability within open distributed environment. ODP provides some preliminary statements on conformance assessment in open distributed systems, but considerable work needs to be done before reaching a workable and accepted conformance testing methodology for open distributed processing. Further, ISO, ITU, OMG, and TINA-C, have recently recognized the urgent need for conformance testing. In this paper, we examine ideas gained from our experience with protocol testing, which may contribute to the design of such a framework. Our methodology is essentially guided by two features that have a great influence on all aspects of the testing process: controllability and observability.