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

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

Программа полностью корректна относительно предусловия и постусловия, если любое выполнение, начатое в состоянии, удовлетворяющем , завершается в состоянии, удовлетворяющем . Полная корректность является конъюнкцией свойства безопасности и свойства жизнеспособности: [2] П {\displaystyle P} В {\displaystyle Q} П {\displaystyle P} В {\displaystyle Q}

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

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

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

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

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

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

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

Выполнение программы можно описать формально, указав бесконечную последовательность состояний программы, которая возникает в ходе выполнения, где последнее состояние завершающейся программы повторяется бесконечно. Для интересующей программы пусть обозначает множество возможных состояний программы, обозначает множество конечных последовательностей состояний программы и обозначает множество бесконечных последовательностей состояний программы. Соотношение справедливо для последовательностей и тогда и только тогда , когда является префиксом или равно . [5] С {\displaystyle S} С ∗ {\displaystyle S^{*}} С ω {\displaystyle S^{\omega }} σ ≤ τ {\displaystyle \сигма \leq \тау } σ {\displaystyle \сигма} τ {\displaystyle \тау} σ {\displaystyle \сигма} τ {\displaystyle \тау} σ {\displaystyle \сигма} τ {\displaystyle \тау}

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

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

∀ σ ∈ С ω : σ ∉ С П ⟹ ( ∃ β ≤ σ : ( ∀ τ ∈ С ω : β τ ∉ С П ) ) {\displaystyle \forall \sigma \in S^{\omega }:\sigma \notin SP\implies (\exists \beta \leq \sigma :(\forall \tau \in S^{\omega }:\beta \tau \notin SP))}

Это формальное определение свойств безопасности подразумевает, что если выполнение удовлетворяет свойству безопасности , то каждый префикс (с повторением последнего состояния) также удовлетворяет . σ {\displaystyle \сигма} С П {\displaystyle СП} σ {\displaystyle \сигма} С П {\displaystyle СП}

Живость

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

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

В первом примере хорошо то , что он дискретен, а в остальных — нет.

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

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

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

∀ α ∈ С ∗ : ( ∃ τ ∈ С ω : α τ ∈ Л П ) {\displaystyle \forall \alpha \in S^{*}:(\exists \tau \in S^{\omega }:\alpha \tau \in LP)}

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

История

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

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

Ссылки

  1. ^ abcd Лампорт, Лесли (март 1977 г.). «Доказательство корректности многопроцессных программ». Труды IEEE по программной инженерии . SE-3 (2): 125– 143. CiteSeerX  10.1.1.137.9454 . doi :10.1109/TSE.1977.229904. S2CID  9985552.
  2. ^ Манна, Зохар; Пнуэли, Амир (сентябрь 1974 г.). «Аксиоматический подход к полной корректности программ». Acta Informatica . 3 (3): 243– 263. doi :10.1007/BF00288637. S2CID  2988073.
  3. ^ т.е. имеет конечную продолжительность
  4. ^ Alford, Mack W.; Lamport, Leslie ; Mullery, Geoff P. (3 апреля 1984 г.). "Основные концепции". Распределенные системы: методы и инструменты для спецификации, продвинутый курс . Конспект лекций по информатике. Том 190. Мюнхен, Германия: Springer Verlag . С.  7–43 . ISBN 3-540-15216-4.
  5. ^ abcdefghijk Альперн, Боуэн; Шнайдер, Фред Б. (1985). «Определение жизнеспособности». Information Processing Letters . 21 (4): 181– 185. doi :10.1016/0020-0190(85)90056-0.
  6. ^ Альперн, Боуэн; Шнайдер, Фред Б. (1987). «Распознавание безопасности и жизнеспособности». Распределенные вычисления . 2 (3): 117– 126. doi :10.1007/BF01782772. hdl : 1813/6567 . S2CID  9717112.
  7. ^ Статья [5] получила премию Дейкстры 2018 года («за выдающиеся статьи о принципах распределенных вычислений, значимость и влияние которых на теорию и/или практику распределенных вычислений были очевидны в течение как минимум десятилетия»), поскольку формальное разложение на свойства безопасности и жизнеспособности имело решающее значение для будущих исследований в области доказательства свойств программ.
  8. ^ обозначает множество конечных последовательностей состояний программы и множество бесконечных последовательностей состояний программы. С ∗ {\displaystyle S^{*}} С ω {\displaystyle S^{\omega }}
  9. ^ Alford, Mack W.; Lamport, Leslie ; Mullery, Geoff P. (3 апреля 1984 г.). "Основные концепции". Распределенные системы: методы и инструменты для спецификации, продвинутый курс . Конспект лекций по информатике. Том 190. Мюнхен, Германия: Springer Verlag . С.  7–43 . ISBN 3-540-15216-4.
  10. ^ Альперн, Боуэн; Демерс, Алан Дж.; Шнайдер, Фред Б. (ноябрь 1986 г.). «Безопасность без заикания». Information Processing Letters . 23 (4): 177– 180. doi :10.1016/0020-0190(86)90132-8. hdl : 1813/6548 .
  11. ↑ Частное сообщение Плоткина Шнайдеру.
  12. ^ Альперн, Боуэн; Шнайдер, Фред Б. (1987). «Распознавание безопасности и жизнеспособности». Распределенные вычисления . 2 (3): 117– 126. doi :10.1007/BF01782772. hdl : 1813/6567 . S2CID  9717112.
Взято с "https://en.wikipedia.org/w/index.php?title=Свойства_безопасности_и_жизнеспособности&oldid=1241388060"