Свойства безопасности и живучести

Свойства выполнения компьютерной программы — особенно для параллельных и распределенных систем — уже давно сформулированы путем задания свойств безопасности («плохие вещи не случаются») и свойств живучести («хорошие вещи случаются»). ^{[ 1 ]}

Программа полностью корректна относительно предусловия. $P$ и постусловие $Q$ если какое-либо выполнение началось в состоянии, удовлетворяющем $P$ завершается в состоянии, удовлетворяющем $Q$ . Полная корректность — это сочетание свойства безопасности и свойства живучести: ^{[ 2 ]}

Свойство безопасности запрещает эти «плохие вещи»: казни, которые начинаются в состоянии, удовлетворяющем $P$ и завершиться в конечном состоянии, которое не удовлетворяет $Q$ . Для программы $C$ , это свойство безопасности обычно записывается с помощью тройки Хоара $\{P\}C\{Q\}$ .
Свойство живучести, «хорошая вещь», заключается в том, что выполнение начинается в состоянии, удовлетворяющем $P$ заканчивается.

Обратите внимание, что плохая вещь дискретна, ^{[ 3 ]} поскольку это происходит в определенном месте во время исполнения. «Хорошая вещь» не обязательно должна быть дискретной, но свойство жизнеспособности завершения дискретно.

Формальные определения, которые в конечном итоге были предложены для свойств безопасности. ^{[ 4 ]} и жизненные свойства ^{[ 5 ]} продемонстрировал, что эта декомпозиция не только интуитивно привлекательна, но и полна: все свойства исполнения представляют собой совокупность свойств безопасности и живучести. ^{[ 5 ]} Более того, проведение декомпозиции может быть полезным, поскольку формальные определения позволяют доказать, что для проверки свойств безопасности и для проверки свойств живучести необходимо использовать разные методы. ^{[ 6 ]}^{[ 7 ]}

Безопасность

Свойство безопасности запрещает возникновение отдельных плохих событий во время выполнения. ^{[ 1 ]} Таким образом, свойство безопасности характеризует то, что разрешено, путем указания того, что запрещено. Требование, чтобы плохая вещь была дискретной, означает, что плохая вещь , происходящая во время выполнения, обязательно происходит в какой-то идентифицируемой точке. ^{[ 5 ]}

Примеры дискретных плохих вещей , которые можно использовать для определения свойства безопасности, включают: ^{[ 5 ]}

Выполнение, которое начинается в состоянии, удовлетворяющем заданному предварительному условию, завершается, но конечное состояние не удовлетворяет требуемому постусловию;
Выполнение двух параллельных процессов, где программные счетчики для обоих процессов обозначают операторы в критической секции ;
Выполнение двух параллельных процессов, где каждый процесс ожидает изменения состояния другого (так называемая взаимоблокировка ).

Выполнение программы можно формально описать, задав бесконечную последовательность состояний программы, возникающую по мере выполнения: где последнее состояние завершающей программы повторяется бесконечно. Для интересующей программы пусть $S$ обозначают множество возможных состояний программы, $S^{*}$ обозначаем множество конечных последовательностей состояний программы, и $S^{\omega }$ обозначают множество бесконечных последовательностей состояний программы. Отношение $\sigma \leq \tau$ справедливо для последовательностей $\sigma$ и $\tau$ если только $\sigma$ является префиксом $\tau$ или $\sigma$ равно $\tau$ . ^{[ 5 ]}

Свойством программы является набор разрешенных исполнений.

Основная характеристика свойства безопасности $SP$ является: Если какое-то исполнение $\sigma$ не удовлетворяет $SP$ тогда самое плохое поскольку это свойство безопасности возникает в какой-то момент $\sigma$ . Обратите внимание: если после такого плохого поступка дальнейшее выполнение приведет к выполнению $\sigma ^{\prime }$ , затем $\sigma ^{\prime }$ тоже не удовлетворяет $SP$ , так как все плохо в $\sigma$ также встречается в $\sigma ^{\prime }$ . Мы считаем этот вывод о непоправимости плохих вещей определяющей характеристикой $SP$ быть объектом безопасности. Формализация этого в логике предикатов дает формальное определение для $SP$ являющийся защитным свойством. ^{[ 5 ]}

\forall \sigma \in S^{\omega }:\sigma \notin SP\implies (\exists \beta \leq \sigma :(\forall \tau \in S^{\omega }:\beta \tau \notin SP))

Это формальное определение свойств безопасности подразумевает, что если выполнение $\sigma$ удовлетворяет свойству безопасности $SP$ тогда каждый префикс $\sigma$ (с повторением последнего состояния) также удовлетворяет $SP$ .

живость

Свойство жизнеспособности предписывает хорошие действия для каждого выполнения или, что то же самое, описывает то, что должно произойти во время выполнения. ^{[ 1 ]} Хорошая вещь не обязательно должна быть дискретной — она может включать в себя бесконечное количество шагов. Примеры хороших вещей, используемых для определения свойства живучести, включают: ^{[ 5 ]}

Прекращение выполнения, начатого в подходящем состоянии;
Незавершение выполнения, начатого в подходящем состоянии;
Гарантированный возможный вход в критический раздел при каждой попытке входа;
Справедливый доступ к ресурсу при наличии разногласий.

Хорошая вещь в первом примере дискретна, но не в остальных.

Получение ответа в пределах заданной границы реального времени является свойством безопасности, а не свойством жизнеспособности. дискретная плохая вещь Это происходит потому, что запрещается : частичное выполнение, которое достигает состояния, в котором ответ еще не получен, а значение часов (переменная состояния) нарушает границу. Свобода тупиков — это свойство безопасности: «плохая вещь» — это тупик (который дискретен).

В большинстве случаев знание того, что программа в конечном итоге делает что-то «хорошее», неудовлетворительно; мы хотим знать, что программа выполняет «хорошую вещь» за определенное количество шагов или до определенного срока. Свойство, которое дает конкретную границу «хорошей вещи», является свойством безопасности (как отмечалось выше), тогда как более слабое свойство, которое просто утверждает, что граница существует, является свойством жизнеспособности. Доказательство такого свойства жизнеспособности, вероятно, будет проще, чем доказательство более строгого свойства безопасности, поскольку доказательство свойства живучести не требует такого подробного учета, который требуется для доказательства свойства безопасности.

В отличие от свойства безопасности свойство живучести $LP$ не может править из любого конечного префикса $\alpha \in S^{*}$ ^{[ 8 ]} казни (поскольку такое а $\alpha$ было бы «плохо» и, таким образом, определяло бы свойство безопасности). Это приводит к определению свойства живучести. $LP$ быть свойством, которое не исключает какой-либо конечный префикс. ^{[ 5 ]}

\forall \alpha \in S^{*}:(\exists \tau \in S^{\omega }:\alpha \tau \in LP)

Это определение не ограничивает хорошую вещь дискретностью — хорошая вещь может включать в себя все $\tau$ , что является выполнением бесконечной длины.

История

Лэмпорт использовал термины «свойство безопасности» и «свойство жизнеспособности». в своей статье 1977 года ^{[ 1 ]} по доказательству корректности многопроцессных (параллельных) программ . Он заимствовал термины из теории сетей Петри , в которой использовались термины живость и ограниченность для описания того, как присваиваются «токены» сети Петри. чтобы его «места» могли эволюционировать; сетей Петри Безопасность представляла собой специфическую форму ограниченности . Впоследствии Лэмпорт разработал формальное определение безопасности для Краткий курс НАТО по распределенным системам в Мюнхене. ^{[ 9 ]} Предполагалось, что свойства инвариантны при заикании . Формальное определение безопасности, данное выше, содержится в статье Альперна и Шнайдер; ^{[ 5 ]} связь между двумя формализациями свойств безопасности появляется в статье Альперна, Демерса и Шнайдера. ^{[ 10 ]}

Альперн и Шнайдер ^{[ 5 ]} дает формальное определение жизнеспособности, сопровождаемое доказательством того, что все свойства могут быть построены с использованием свойств безопасности и свойств живучести. Это доказательство было вдохновлено открытием Гордона Плоткина о том, что свойства безопасности соответствуют замкнутым множествам , а свойства живучести соответствуют плотным множествам в естественной топологии на множестве. $S^{\omega }$ бесконечных последовательностей состояний программы. ^{[ 11 ]} Впоследствии Альперн и Шнайдер ^{[ 12 ]} не только дал характеристику автомата Бюхи для формальных определений свойств безопасности и свойств живучести, но и использовал эти формулировки автоматов, чтобы показать, что проверка свойств безопасности потребует инварианта , а проверка свойств живучести потребует обоснованного аргумента . Соответствие между типом свойства (безопасность/жизнеспособность) и видом доказательства (инвариантность/обоснованность) было сильным аргументом в пользу того, что разложение свойств на безопасность и живучесть (в отличие от какого-либо другого разделения) было Полезный — знание типа собственности, которую необходимо доказать, определяет тип требуемого доказательства.

Ссылки

^ Перейти обратно: ^а ^б ^с ^д Лэмпорт, Лесли (март 1977 г.). «Доказательство корректности многопроцессных программ». Транзакции IEEE по разработке программного обеспечения . СЭ-3 (2): 125–143. CiteSeerX 10.1.1.137.9454 . дои : 10.1109/TSE.1977.229904 . S2CID 9985552 .
^ Манна, Зоар; Пнуэли, Амир (сентябрь 1974 г.). «Аксиоматический подход к тотальной корректности программ». Акта Информатика . 3 (3): 243–263. дои : 10.1007/BF00288637 . S2CID 2988073 .
^ т.е. он имеет конечную продолжительность
^ Алфорд, Мак В.; Лэмпорт, Лесли ; Маллери, Джефф П. (3 апреля 1984 г.). «Основные понятия». Распределенные системы: методы и инструменты спецификации, продвинутый курс . Конспекты лекций по информатике. Том. 190. Мюнхен, Германия: Springer Verlag . стр. 7–43. ISBN 3-540-15216-4 .
^ Перейти обратно: ^а ^б ^с ^д ^и ^ж ^г ^час ^я ^дж ^к Альперн, Боуэн; Шнайдер, Фред Б. (1985). «Определение живости». Письма об обработке информации . 21 (4): 181–185. дои : 10.1016/0020-0190(85)90056-0 .
^ Альперн, Боуэн; Шнайдер, Фред Б. (1987). «Признание безопасности и живучести». Распределенные вычисления . 2 (3): 117–126. дои : 10.1007/BF01782772 . hdl : 1813/6567 . S2CID 9717112 .
^ Газета ^{[ 5 ]} получил премию Дейкстры в 2018 году («за выдающиеся статьи по принципам распределенных вычислений, значение и влияние которых на теорию и/или практику распределенных вычислений были очевидны в течение как минимум десяти лет»), за формальное разложение на свойства безопасности и живучести. имел решающее значение для будущих исследований по доказательству свойств программ.
^ $S^{*}$ обозначает множество конечных последовательностей состояний программы и $S^{\omega }$ множество бесконечных последовательностей состояний программы.
^ Алфорд, Мак В.; Лэмпорт, Лесли ; Маллери, Джефф П. (3 апреля 1984 г.). «Основные понятия». Распределенные системы: методы и инструменты спецификации, продвинутый курс . Конспекты лекций по информатике. Том. 190. Мюнхен, Германия: Springer Verlag . стр. 7–43. ISBN 3-540-15216-4 .
^ Альперн, Боуэн; Демерс, Алан Дж.; Шнайдер, Фред Б. (ноябрь 1986 г.). «Безопасность без заиканий». Письма об обработке информации . 23 (4): 177–180. дои : 10.1016/0020-0190(86)90132-8 . hdl : 1813/6548 .
↑ Частное сообщение Плоткина Шнайдеру.
^ Альперн, Боуэн; Шнайдер, Фред Б. (1987). «Признание безопасности и живучести». Распределенные вычисления . 2 (3): 117–126. дои : 10.1007/BF01782772 . hdl : 1813/6567 . S2CID 9717112 .

[Lamport1977-1] Перейти обратно: ^а ^б ^с ^д Лэмпорт, Лесли (март 1977 г.). «Доказательство корректности многопроцессных программ». Транзакции IEEE по разработке программного обеспечения . СЭ-3 (2): 125–143. CiteSeerX 10.1.1.137.9454 . дои : 10.1109/TSE.1977.229904 . S2CID 9985552 .

[totalcorrectness-2] Манна, Зоар; Пнуэли, Амир (сентябрь 1974 г.). «Аксиоматический подход к тотальной корректности программ». Акта Информатика . 3 (3): 243–263. дои : 10.1007/BF00288637 . S2CID 2988073 .

[3] т.е. он имеет конечную продолжительность

[4] Алфорд, Мак В.; Лэмпорт, Лесли ; Маллери, Джефф П. (3 апреля 1984 г.). «Основные понятия». Распределенные системы: методы и инструменты спецификации, продвинутый курс . Конспекты лекций по информатике. Том. 190. Мюнхен, Германия: Springer Verlag . стр. 7–43. ISBN 3-540-15216-4 .

[DefiningLiveness-5] Перейти обратно: ^а ^б ^с ^д ^и ^ж ^г ^час ^я ^дж ^к Альперн, Боуэн; Шнайдер, Фред Б. (1985). «Определение живости». Письма об обработке информации . 21 (4): 181–185. дои : 10.1016/0020-0190(85)90056-0 .

[6] Альперн, Боуэн; Шнайдер, Фред Б. (1987). «Признание безопасности и живучести». Распределенные вычисления . 2 (3): 117–126. дои : 10.1007/BF01782772 . hdl : 1813/6567 . S2CID 9717112 .

[7] Газета ^{[ 5 ]} получил премию Дейкстры в 2018 году («за выдающиеся статьи по принципам распределенных вычислений, значение и влияние которых на теорию и/или практику распределенных вычислений были очевидны в течение как минимум десяти лет»), за формальное разложение на свойства безопасности и живучести. имел решающее значение для будущих исследований по доказательству свойств программ.

[8] $S^{*}$ обозначает множество конечных последовательностей состояний программы и $S^{\omega }$ множество бесконечных последовательностей состояний программы.

[9] Алфорд, Мак В.; Лэмпорт, Лесли ; Маллери, Джефф П. (3 апреля 1984 г.). «Основные понятия». Распределенные системы: методы и инструменты спецификации, продвинутый курс . Конспекты лекций по информатике. Том. 190. Мюнхен, Германия: Springer Verlag . стр. 7–43. ISBN 3-540-15216-4 .

[10] Альперн, Боуэн; Демерс, Алан Дж.; Шнайдер, Фред Б. (ноябрь 1986 г.). «Безопасность без заиканий». Письма об обработке информации . 23 (4): 177–180. дои : 10.1016/0020-0190(86)90132-8 . hdl : 1813/6548 .

[11] Частное сообщение Плоткина Шнайдеру.

[12] Альперн, Боуэн; Шнайдер, Фред Б. (1987). «Признание безопасности и живучести». Распределенные вычисления . 2 (3): 117–126. дои : 10.1007/BF01782772 . hdl : 1813/6567 . S2CID 9717112 .

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]