Algorithmic skeletons are a well-known approach for implementing parallel and distributed applications. Declarative versions typically use higher-order functions in functional languages. We show here a different appro...
详细信息
ISBN:
(纸本)9783540729198
Algorithmic skeletons are a well-known approach for implementing parallel and distributed applications. Declarative versions typically use higher-order functions in functional languages. We show here a different approach based on object-oriented parameterized modules in Maude, that receive the operations needed to solve a concrete problem as a parameter. Architectures are conceived separately from the skeletons that are executed on top of them. the object-oriented methodology followed facilitates nesting of skeletons and the combination of architectures. Maude analysis tools allow to check at different abstraction levels properties of the applications built by instantiating a skeleton.
Rewriting logic provides a powerful, flexible mechanism for language definition and analysis. this flexibility in design can lead to problems during analysis, as different designs for the same language feature can cau...
详细信息
ISBN:
(纸本)9783540729198
Rewriting logic provides a powerful, flexible mechanism for language definition and analysis. this flexibility in design can lead to problems during analysis, as different designs for the same language feature can cause drastic differences in analysis performance. this paper describes some of these design decisions in the context of KOOL, a concurrent, dynamic, object-oriented language. Also described is a general mechanism used in KOOL to support model checking while still allowing for ongoing, sometimes major, changes to the language definition.
We present a novel approach, based on probabilistic formalmethods, to developing cross-layer resource optimization policies for resource limited distributedsystems. One objective of this approach is to enable system...
详细信息
ISBN:
(纸本)9783540729198
We present a novel approach, based on probabilistic formalmethods, to developing cross-layer resource optimization policies for resource limited distributedsystems. One objective of this approach is to enable system designers to analyze designs in order to study design tradeoffs and predict the possible property violations as the system evolves dynamically over time. Specifically, an executable formal specification is developed for each layer under consideration (for example, application, middleware, operating system). the formal specification is then analyzed using statistical model checking and statistical quantitative analysis, to determine the impact of various resource management policies for achieving desired end-to-end QoS properties. We describe how existing statistical approaches have been adapted and improved to provide analyses of given cross-layered optimization policies with quantifiable confidence. the ideas are tested in a multi-mode multi-media case study. Experiments from boththeoretical analysis and Monte-Carlo simulation followed by statistical analyses demonstrate the applicability of this approach to the design of resource-limited distributedsystems.
the success of distributed event-based infrastructures such as SIENA and Elvin is partially due to their ease of use. Even novice users of these infrastructures not versed in distributed programming can quickly compre...
详细信息
ISBN:
(纸本)9783540729198
the success of distributed event-based infrastructures such as SIENA and Elvin is partially due to their ease of use. Even novice users of these infrastructures not versed in distributed programming can quickly comprehend the small and intuitive interfaces that these systems typically feature. However, if these users make incorrect assumptions about how the infrastructure services work, a mismatch between the infrastructure and its client applications occurs, which may manifest itself in erroneous client behaviour. We propose a framework for automatically model checking distributed event-basedsystems in order to discover mismatch between the infrastructure and its clients. Using the SIENA event service as an example, we implemented and evaluated our framework by customizing the Bandera/Bogor tool pipeline. Two realistic Java applications are implemented to test and evaluate the framework.
A session type is an abstraction of a sequence of heterogeneous values sent over one channel between two communicating processes. Session types have been introduced to guarantee consistency of the exchanged data and, ...
详细信息
ISBN:
(纸本)9783540729198
A session type is an abstraction of a sequence of heterogeneous values sent over one channel between two communicating processes. Session types have been introduced to guarantee consistency of the exchanged data and, more recently, progress of the session, i.e. the property that once a communication has been established, well-formed programs will never starve at communication points. A relevant feature which influences progress is whether the communication is synchronous or asynchronous. In this paper, we first formulate a typed asynchronous multi-threaded object-oriented language withthread spawning, iterative and higher order sessions. then we study its progress through a new effect system. As far as we know, ours is the first session type system which assures progress in asynchronous communication.
the proceedings contain 20 papers from the formalmethods for openobject-baseddistributedsystems: 7thifip WG 6.1 internationalconference, FMOODS 2005. the topics discussed include: pattern matching over a dynamic...
详细信息
the proceedings contain 20 papers from the formalmethods for openobject-baseddistributedsystems: 7thifip WG 6.1 internationalconference, FMOODS 2005. the topics discussed include: pattern matching over a dynamic network of tuple spaces;a dynamic class construct for asynchronous concurrent objects;checking the validity of scenarios in UML models;a semantics for UML-RT active classes via mapping into circus;tracing integration analysis in component-basedformal specifications;guaranteeing resource bounds for component software;detecting errors in multithreaded programs by generalized predictive analysis of executions;and a distributed implementation of mobile nets as mobile agents.
the proceedings contain 20 papers. the special focus in this conference is on Models, Calculi, UML, Security, Composition, Verification, Analysis of Java Programs and Web Services. the topics include: A dynamic class ...
ISBN:
(纸本)9783540261810
the proceedings contain 20 papers. the special focus in this conference is on Models, Calculi, UML, Security, Composition, Verification, Analysis of Java Programs and Web Services. the topics include: A dynamic class construct for asynchronous concurrent objects;an abstract machine for the kell calculus;a typed process calculus for XML messaging;checking the validity of scenarios in UML models;towards an integrated formal analysis for security and trust;tracing integration analysis in component-basedformal specifications;guaranteeing resource bounds for component software;specification and verification of encapsulation in java programs;detecting errors in multithreaded programs by generalized predictive analysis of executions;a distributed implementation of mobile nets as mobile agents and property-driven development of a coordination model for distributed simulations.
We use a distributed, enriched A-calculus for describing networks of services. Both services and their clients can protect themselves, by imposing security constraints on each other9;s behaviour. then, service inte...
详细信息
ISBN:
(纸本)354034893X
We use a distributed, enriched A-calculus for describing networks of services. Both services and their clients can protect themselves, by imposing security constraints on each other's behaviour. then, service interaction results in a call-by-propbrty mechanism, that matches the client requests with service's. A static approach is also described, that determines how to compose services while guaranteeing that their execution is always secure, without resorting to any dynamic check.
Modern applications distributed across networks such as the Internet may need to evolve without compromising application availability. objectsystems are well suited for runtime update, as encapsulation clearly separa...
详细信息
ISBN:
(纸本)354034893X
Modern applications distributed across networks such as the Internet may need to evolve without compromising application availability. objectsystems are well suited for runtime update, as encapsulation clearly separates internal structure and external services. this paper considers a type-safe asynchronous mechanism for dynamic class upgrade, allowing class hierarchies to be updated in such a way that the existing objects of the upgraded class and of its subclasses gradually evolve at runtime. New external services may be introduced in classes and old services may be reprogrammed while static type checking ensures that asynchronous class updates maintain type safety. A formalization is shown in the Creol language which, addressing distributed and object-oriented systems, provides a natural framework for dynamic upgrades.
In this paper we describe an application of the theory of graph transformations to the practise of language design. In particular, we have defined the static and dynamic semantics of a small but realistic object-orien...
详细信息
ISBN:
(纸本)354034893X
In this paper we describe an application of the theory of graph transformations to the practise of language design. In particular, we have defined the static and dynamic semantics of a small but realistic object-oriented language (called TAAL) by mapping the language constructs to graphs (the static semantics) and modelling their effect by graph transformation rules (the dynamic semantics). this gives rise to execution models for all TAAL-programs, which can be used as the basis for formal verification. this work constitutes a first step towards a method for defining all aspects of software languages, besides their concrete syntax, in a consistent and rigorous manner. Such a method facilitates the integration of formal correctness in the software development trajectory.
暂无评论