Performance analysis of computing systems, in particular distributed computing systems, is a complex process. Analysing the complex flows and interactions between a set of distributed processing nodes is a non-trivial...
详细信息
Aspect-oriented approaches have recently been proposed to address the problem of specifying dynamic object-basedsystems, by depicting the various roles of the objects separately. In this paper, we consider an approac...
详细信息
ISBN:
(纸本)9781475752687
Aspect-oriented approaches have recently been proposed to address the problem of specifying dynamic object-basedsystems, by depicting the various roles of the objects separately. In this paper, we consider an approach based on the observable behavior of objects and propose a specification formalism for reusable object interfaces with input/output-driven assumption-guarantee predicates. the formalism supports compositional reasoning and exchange of object identities between objects in an environment where the number of objects is unbounded.
the Internet Inter-ORB Protocol (IIOP) supports the interworking of object Request Brokers (ORBs) over TCP/IP. this paper creates a service specification for HOP by combining three interworking facilities identified i...
详细信息
ISBN:
(纸本)9781475752687
the Internet Inter-ORB Protocol (IIOP) supports the interworking of object Request Brokers (ORBs) over TCP/IP. this paper creates a service specification for HOP by combining three interworking facilities identified in ISO/IEC 14752. this is formalised using Coloured Petri nets, which are used to generate the set of global primitive sequences of the IIOP service.
distributedobject computing is a computing paradigm that allows objects to be distributed over a heterogeneous network. Infrastructures help to develop distributedobject applications by offering necessary services f...
详细信息
ISBN:
(纸本)9781475752687
distributedobject computing is a computing paradigm that allows objects to be distributed over a heterogeneous network. Infrastructures help to develop distributedobject applications by offering necessary services for distributed computing. Having a comprehensive infrastructure to hand, the development of complex distributedobjectsystems is feasible in principle. Flexibly evolving architectures as well as highly dynamic distributedobject structures are key requirements for nowadays distributed solutions. they can hardly be well designed on this level of programming, due to their complexity. A visual modeling framework is presented which offers a more abstract and intuitive approach to the relevant aspects of a distributedobject system. In this framework, network and object structures as well as their evolution are visualized in a diagrammatic style, e.g. in UML notation. Semantically, this approach relies on graphs and their transformation, i.e. it has a precise background useful for further reasoning.
the main contribution of this paper consists of a description of a front-end tool which supports the computer-aided specification and verification of a class of flowcharts which capture the basic dynamics of object-or...
详细信息
ISBN:
(纸本)9781475752687
the main contribution of this paper consists of a description of a front-end tool which supports the computer-aided specification and verification of a class of flowcharts which capture the basic dynamics of object-oriented programs. the specific emphasis of our approach is on the automated verification of flowcharts annotated with assertions which allow one to specify properties directly in terms of the source code itself instead of some particular model of its semantics.
Since parallel and distributed algorithms are subject to subtle errors that are unlikely to be detected in usual operation, only testing is not enough to reduce errors. thus, it is necessary to formally analyze such a...
详细信息
ISBN:
(纸本)9781475752687
Since parallel and distributed algorithms are subject to subtle errors that are unlikely to be detected in usual operation, only testing is not enough to reduce errors. thus, it is necessary to formally analyze such algorithms in order to confirm that they have desirable properties. this paper describes the case study that Suzuki&Kasami distributed mutual exclusion algorithm is formally analyzed. In the case study, the algorithm has been modeled using UNITY-like models called observational transition systems (OTS's), the model has been described in CafeOBJ, and it has been verified that the algorithm is mutually exclusive and lockout free withthe help of CafeOBJ system. In the verification that the algorithm is lockout free, we have found a hidden assumption necessary for the verification, which is not explicitly mentioned in the original paper written by Suzuki and Kasami.
In general few components are reused as they are. Often, available components are incompatible with what is required. this necessitates component adaptations or the use of adapters between components. In this paper we...
详细信息
ISBN:
(纸本)9781475752687
In general few components are reused as they are. Often, available components are incompatible with what is required. this necessitates component adaptations or the use of adapters between components. In this paper we develop algorithms for the synthesis of adapters, coercing incompatible components into meeting requirements. We concentrate on adapters for concurrent systems, where adapters are able to resolve synchronisation problems of concurrent components. A new interface model for components, which includes protocol information, allows us to generate these adapters semi-automatically.
Middleware such as Corba ORBs, DCOM, or Java Beans provide programming abstractions for interoperation of diverse components in an opendistributed setting. More recent middleware initiatives focus on resource managem...
详细信息
ISBN:
(纸本)9781475752687
Middleware such as Corba ORBs, DCOM, or Java Beans provide programming abstractions for interoperation of diverse components in an opendistributed setting. More recent middleware initiatives focus on resource management, security, and dependability services supporting a wide range of coordination and Quality of Service (QoS) requirements and allowing applications programmers to focus on functionality and intrinsic performance issues. As computer systems become more and more complex and ubiquitous it is increasingly important to have robust and powerful middleware that can achieve a high degree of reliability and assurance where needed. For example, as networks become more programmable it will be essential to minimize failures not only by simulation and testing, but also by formal modeling and analysis at many levels of abstraction. For adaptability and extensibility middleware services themselves need to be built from component services. Middleware services for resource management such as scheduling, protocols providing security and reliability, load balancing and stream synchronization, execute concurrently with each other and with application activities and can therefore potentially interfere with each other in subtle ways. the Two Level Actor Model (TLAM) is a mathematical framework designed for reasoning about the interaction and composition of resource management activities in opendistributedsystems, and their dynamic installation and modification. the TLAM is based on the actor model of object-baseddistributed computation. As the name suggests, in the TLAM, a system is composed of two kinds of actors, base-level actors and meta-level actors, distributed over a network of processing nodes. Base-level actors carry out application-level computation, while meta-level actors are part of the runtime system (middleware) that manages system resources and controls the runtime semantics of the base level. the TLAM model has been applied to reasoning about services s
We propose a new synchronous language called Behavior Expression, its semantics and compilation mechanism. We also present OMDD as intermediate code for its compilation. Dependency cycle, determinism arid composabilit...
详细信息
ISBN:
(纸本)0792379233
We propose a new synchronous language called Behavior Expression, its semantics and compilation mechanism. We also present OMDD as intermediate code for its compilation. Dependency cycle, determinism arid composability can be checked directly by analyzing OMDDs. Consequently, it allows partial compilation and automatic distribution. based on these benefits, we propose a new methodology for the development of real-time distributedsystems by integrating behavior expression into UML.
暂无评论