Wyniki wyszukiwania - Biblioteka Nauki

Nowa wersja platformy, zawierająca wyłącznie zasoby pełnotekstowe, jest już dostępna.
Przejdź na https://bibliotekanauki.pl

Ograniczanie wyników

2 Fundamenta Informaticae

2 1999

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Integrating Distributed Algorithms into distributed systems

100%

Kindler E. , Peuker S.

1999

tom Vol. 37, Nr 3

291-309

A distributed algorithm is often used as a part of a larger distributed system. Usually, the properties of an algorithm are proven for the algorithm in isolation. Then, it is not obvious how the algorithm behaves when integrated into a larger system. In this paper, we present a simple technique which allows to derive properties of an algorithm which is integrated into a distributed system from the properties of the algorithm in isolation. The technique exploits the fact that some actions of a distributed algorithm do not belong to the algorithm but are triggered by the environment. If these actions are distinguished and are adequately considered in the verification of the algorithm, basically all properties are still valid for the algorithm as a part of a larger distributed system. This result will be formalized in the setting of the Distributed Algorithms' Working Notation (DAWN). Based on this result, we will give a proof rule which allows to prove liveness properties of a system from liveness properties of the involved distributed algorithm.

ILF and DAWN for verifying distributed algorithms : an idea for a tool

100%

Baar T. , Kindler E.

1999

tom Vol. 37, Nr 3

201-211

The Distributed Algorithms Working Notation (DAWN) was designed for modeling and veri-fying algorithms in an intuitive way. Nevertheless, DAWN proofs are formal. In this paper, we show that it is possible to check correctness of a DAWN proof fully auto-matically. For each step in a DAWN proof, we can generate a set proof obligations which can automatically be checked by help of automated theorem provers. The verification tool ILF provides a uniform interface to many theorem provers - which makes it an ideal partner for DAWN and a basis for building a DAWN-tool.