Предыдущая страница реферата | 11  12  13  14  15  16  17  18  19  20  21 | Следующая страница реферата

Возможно включить условия справедливости в формальную модель явно, как это сделано Манна и Пнули [MP88]. Большинство алгоритмов, с которыми мы имеем дело в этой книге, не полагаются на эти условия; поэтому мы решили не включать их в модель, а устанавливать эти условия явно, когда они используются для конкретного алгоритма или проблемы. Также, существует спор, приемлемо ли включать предположение справедливости в модели распределенных систем. Было выдвинуто утверждение, что предположение справедливости не должны производиться, более того алгоритмы не должны разрабатываться с учетом этих предположений. Дискуссия по некоторым запутанным вопросам, относящимся к предположению справедливости может быть найдена в [Fra86].

2.2 Доказательство свойств систем перехода

Рассматривая распределенный алгоритм для некоторой проблемы, необходимо продемонстрировать, что алгоритм есть корректное решение этой проблемы.
Проблема указывает, какие свойства требуемый алгоритм должен иметь; должно быть показано, что решение обладает этими свойства. Вопрос проверки распределенных алгоритмов получил значительное внимание и есть большое количество статей, обсуждающих формальные методы проверки; см. [CM88,
Fra86, Kel76, MP88]. В этом разделе обсуждаются некоторые простые, но часто используемые методы для демонстрации правильности распределенных алгоритмов. Эти методы полагаются только на определение системы переходов.

Многие из требуемых свойств распределенных алгоритмов попадают в один из двух типов: требования безопасности и требования живости. Требования безопасности накладывают ограничение, что определенное свойство должно выполняться для каждого исполнения системы в каждой конфигурации, достигаемой в этом исполнении. Требования живости определяют, что определенное свойство должно выполняться для каждого исполнения системы в некоторых конфигурациях, достигаемых в этом исполнении. Эти требования могут также встречаться в ослабленной форме, например, они могут удовлетворяться с некоторой фиксированной вероятностью над множеством возможных исполнений. Другие требования к алгоритмам могут включать ограничения, которые основываются только на использовании некоторого данного знания (см. подраздел 2.4.4), что они гибки по отношен ию к нарушениям в некоторых процессах (см. часть 3), что процессы равны (см. главу 9), и т.д.

Методы проверки, описанные в этом разделе, базируются на истинности утверждений в конфигурациях, достигаемых в исполнении. Такие методы называются методами проверки утверждений. Утверждение это унарное отношение на множестве конфигураций, то есть, предикат, который принимает значение истина на одном подмножестве конфигураций и ложь – на другом.

2.2.1 Свойства безопасности

Свойство безопасности алгоритма это свойство в форме «Утверждение P истина в каждой конфигурации каждого исполнения алгоритма». Неформально это формулируется как «Утверждение Р всегда истина». Основной метод для того, чтобы показать, что утверждение Р всегда истина, это продемонстрировать, что Р инвариант согласно следующим определениям. Нотация P((), где ( это конфигурация, есть булево выражение, чье значение истина, если Р выполняется в (, и ложь в противном случае.

Определения зависят от данной системы переходов S = (C, (, I). Далее, мы будем писать {P} ( {Q}, чтобы обозначить, что для каждого перехода ( ( (
(системы S), если Р(() то Q((). Таким образом {P} ( {Q} означает, что, если
Р выполняется перед любым переходом, то Q выполняется после этого перехода.

Определение 2.9 Утверждение Р инвариант системы S, если

1) для всех ( ( I, и

2) {P} ( {P}.

Определение говорит, что инвариант выполняется в каждой начальной конфигурации, и сохраняется при каждом переходе. Из этого следует, что он сохраняется в каждой достигаемой конфигурации, как и формулируется в следующем теореме.

Теорема 2.10 Если Р это инвариант системы S, то Р выполняется для каждой конфигурации каждого исполнения системы S.

Доказательство. Пусть Е = ((0, (1, (2, ...) исполнение системы S. Будет показано по индукции, что Р((i) выполняется для каждого i. Во-первых, Р((0) выполняется, потому что (0 ( I и по первому предложению определения 2.9. Во- вторых, предположим P((i ) выполняется и (i ( (i+1 есть переход, который встречается в E. По второму предложению определения 2.9 P((i+1) выполняется, что и завершает доказательство. (

И наоборот, утверждение, которое выполняется в каждой конфигурации каждого исполнения, есть инвариант (см. упражнение 2.2). Отсюда не каждое свойство безопасности может быть доказано применением теоремы 2.10. В этом случае, однако, каждое утверждение, которое всегда истинно, включено в инвариант; отсюда может быть показано, применением следующей теоремы, что утверждение всегда истинно. (Нужно помнить, однако, что часто очень трудно найти подходящий инвариант Q, к которому можно применить теорему.)

Теорема 2.11 Пусть Q будет инвариантом системы S и положим Q ( P (для каждого ( ( С). Тогда Р выполняется в каждой конфигурации каждого исполнения системы S.

Доказательство. По теореме 2.10, Q выполняется в каждой конфигурации, и так как Q включает P, то P выполняется в каждой конфигурации также. (

Иногда полезно доказать сначала слабый инвариант, и впоследствии использовать его для доказательства более сильного инварианта. Как можно сделать инвариант более сильным демонстрируется в следующем определении и теореме.

Определение 2.12 Пусть S будет системой переходов и P, Q будут утверждениями. Р называется Q-производным, если

1) для всех ( ( I, Q(() ( Р((); и

2) {Q ( Р} ( {Q ( Р}.

Теорема 2.13 Если Q есть инвариант и Р – Q-производное, то Q ( P есть инвариант.

Доказательство. Согласно определению 2.9, должно быть показано, что

1) для всех ( ( I, Q(() ( Р((); и

2) {Q ( Р} ( {Q ( Р}.

Рекомендуем скачать другие рефераты по теме: педагогические рефераты, реферат машини.





Предыдущая страница реферата | 11  12  13  14  15  16  17  18  19  20  21 | Следующая страница реферата