this paper presents a hybrid method for verification and synthesis of parameterized self-stabilizing protocols where algorithmic design and mechanical verification techniques/tools are used hand-in-hand. the core idea...
详细信息
ISBN:
(纸本)9783319178226;9783319178219
this paper presents a hybrid method for verification and synthesis of parameterized self-stabilizing protocols where algorithmic design and mechanical verification techniques/tools are used hand-in-hand. the core idea behind the proposed method includes the automated synthesis of self-stabilizing protocols in a limited scope (i.e., fixed number of processes) and the use of theorem proving methods for the generalization of the solutions produced by the synthesizer. Specifically, we use the Prototype Verification System (PVS) to mechanically verify an algorithm for the synthesis of weakly self-stabilizing protocols. then, we reuse the proof of correctness of the synthesis algorithm to establish the correctness of the generalized versions of synthesized protocols for an arbitrary number of processes. We demonstrate the proposed approach in the context of an agreement and a coloring protocol on the ring topology.
this paper addresses the problem of synthesizing an asynchronous system from a temporal specification. We show that the cost of synthesizing a single-process implementation is the same for synchronous and asynchronous...
详细信息
ISBN:
(纸本)9783540714095
this paper addresses the problem of synthesizing an asynchronous system from a temporal specification. We show that the cost of synthesizing a single-process implementation is the same for synchronous and asynchronous systems (2EXPTIME-complete for CTL* and EXPTIME-complete for the mu-calculus) if we assume a full scheduler (i.e., a scheduler that allows every possible scheduling), and exponentially more expensive for asynchronous systems without this assumption (3EXPTIME-complete for CTL* and 2EXPTIME-complete for the mu-calculus). While multi-process synthesis for synchronous distributed systems is possible for certain architectures (like pipelines and rings), we show that the synthesis of asynchronous distributed systems is decidable if and only if at most one process implementation is unknown.
We show how to combine the two most powerful approaches for automated termination analysis of logicprograms (LPs): the direct approach which operates directly on LPs and the transformational approach which transforms...
详细信息
ISBN:
(纸本)9783642125911
We show how to combine the two most powerful approaches for automated termination analysis of logicprograms (LPs): the direct approach which operates directly on LPs and the transformational approach which transforms LPs to term rewrite systems (TRSs) and tries to prove termination of the resulting TRSs. To this end, we adapt the well-known dependency pair framework from TRSs to LPs. Withthe resulting method;one can combine arbitrary termination techniques for LPs in a completely modular way and one call use both direct and transformational techniques for different parts of the same LP.
We present a type theory characterizing the mobility and locality of program terms in a distributed computation. the type theory of our calculus is derived from logical notions of necessity (square A) and possibility ...
详细信息
ISBN:
(纸本)3540266550
We present a type theory characterizing the mobility and locality of program terms in a distributed computation. the type theory of our calculus is derived from logical notions of necessity (square A) and possibility (lozenge A) of the modal logic S4 via a Curry-Howard style isomorphism. logical worlds are interpreted as sites for computation, accessibility corresponds to dependency between processes at those sites. Necessity (square A) describes terms of type A which have a structural kind of mobility or location-independence. Possibility (lozenge A) describes terms of type A located somewhere, perhaps at a remote site. the modalities square and lozenge are defined in a clean, orthogonal manner, leading to a simple account of mobility and higher-order functions. For illustration, we assume an execution environment with each location distinguished by a mutable store. Here modal types ensure that store addresses never escape from the location where they are defined, eliminating a source of runtime errors. We speculate as to other advantages or trade-offs of this disciplined style of distributed programming.
Type information has many applications;it can e.g. be used in optimized compilation, termination analysis and error detection. However, logicprograms are typically untyped. A well-typed program has the property that ...
详细信息
ISBN:
(纸本)9783642005145
Type information has many applications;it can e.g. be used in optimized compilation, termination analysis and error detection. However, logicprograms are typically untyped. A well-typed program has the property that it behaves identically on well-typed goals with or without type checking. Hence the automatic inference of a well-typing is worthwhile. Existing inferences are either cheap and inaccurate, or accurate and expensive. By giving up the requirement that all calls to a predicate have types that are instances of a unique polymorphic type but instead allowing multiple polymorphic typings for the same predicate, we obtain a novel strongly-connected-component-based analysis that provides a good compromise between accuracy and computational cost.
the increasing availability of smart objects demands for flexible mechanisms to orchestrate different types of these objects to smart environments. As smart objects are typically not aware of each other, an orchestrat...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
the increasing availability of smart objects demands for flexible mechanisms to orchestrate different types of these objects to smart environments. As smart objects are typically not aware of each other, an orchestrating platform has to manage common resources, to harmonize the individual behavior of the acting objects, and to combine their activities to an intelligent team work. this paper presents a corresponding framework to implement such an orchestrating platform. It provides a concurrent programming language representing states in Description logics and state transitions as logical updates enabling deductive support to infer non-explicitly represented knowledge. It uses temporal logic to suspend execution of a process for a particular evolution of the global state that is specified by a LTL formula. Since a process can fork into subprocesses this provides a mechanism for runtime verification by splitting a process into a subprocess executing some critical program and another parallel subprocess monitoring the first one by waiting for the desired evolution of states specified in its LTL formula.
An offline approach to narrowing-driven partial evaluation (a partial evaluation scheme for first-order functional and functional logicprograms) has recently been introduced. In this approach, program annotations (i....
详细信息
ISBN:
(纸本)9783540714095
An offline approach to narrowing-driven partial evaluation (a partial evaluation scheme for first-order functional and functional logicprograms) has recently been introduced. In this approach, program annotations (i.e., the expressions that should be generalised at partial evaluation time to ensure termination) are based on a simple syntactic characterisation of quasi-terminating programs. this work extends the previous offline scheme by introducing a new annotation strategy which is based on a combination of size-change graphs and binding-time analysis. Preliminary experiments point out that the number of program annotations is significantly reduced compared to the previous approach, which means that faster residual programs are often produced.
We provide an approach to formally analyze the computational behavior of coroutines in logicprograms and to compile these computations into new programs, not requiring any support for coroutines. the problem was alre...
详细信息
ISBN:
(纸本)9783319178226;9783319178219
We provide an approach to formally analyze the computational behavior of coroutines in logicprograms and to compile these computations into new programs, not requiring any support for coroutines. the problem was already studied near to 30 years ago, in an analysis and transformation technique called Compiling Control. However, this technique had a strong ad hoc flavor: the completeness of the analysis was not well understood and its symbolic evaluation was also very ad hoc. We show how Abstract Conjunctive Partial Deduction, introduced by Leuschel in 2004, provides an appropriate setting to redefine Compiling Control. Leuschel's framework is more general than the original formulation, it is provably correct, and it can easily be applied for simple examples. We also show that the Abstract Conjunctive Partial Deduction framework needs some further extension to be able to deal with more complex examples.
the traditional stepwise refinement basedprogram derivation methodologies are primarily top-down. Strictly following the top-down program derivation approach may require backtracking resulting in rework. Moreover, th...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
the traditional stepwise refinement basedprogram derivation methodologies are primarily top-down. Strictly following the top-down program derivation approach may require backtracking resulting in rework. Moreover, the top down approach does not directly help in suggesting the next course of action in case of a failed derivation attempt. In this work we seamlessly incorporate a bottom up assumption propagation technique into a primarily top down derivation methodology. We present new tactics for back-propagating the assumptions made during the top-down phase. these tactics help in reducing the guesswork during the derivations. We have implemented these tactics in a program derivation system. Withthe help of simple examples, we show how this approach is useful for avoiding backtracking thereby simplifying the derivations.
Among other objectives, rewriting programs serves as a useful technique to improve numerical accuracy. However, this optimization is not intuitive and this is why we switch to automatic transformation techniques. We a...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
Among other objectives, rewriting programs serves as a useful technique to improve numerical accuracy. However, this optimization is not intuitive and this is why we switch to automatic transformation techniques. We are interested in the optimization of numerical programs relying on the IEEE754 floating-point arithmetic. In this article, our main contribution is to study the impact of optimizing the numerical accuracy of programs on the time required by numerical iterative methods to converge. To emphasize the usefulness of our tool, we make it optimize several examples of numerical methods such as Jacobi's method, Newton-Raphson's method, etc. We show that significant speedups are obtained in terms of number of iterations, time and flops.
暂无评论