Формальная модель
Дополнение к рабочей формальной модели
Протокол — правила записей, состояний, подтверждений и переходов. Подтверждение содержит тип действия, участника, полномочия, объект, область действия, время и версию условий. Кандидаты инвариантов: ознакомление не создаёт обязательства; предложение ИИ не заменяет решение; существенная новая версия требует надлежащего согласования; исполнение не равно приёмке; история и основания изменения сохраняются. Эти требования ещё предстоит формализовать и проверить.
Кто → перед кем → какой результат → срок → условия → ресурсы → зависимости → кто и по каким критериям принимает результат. Дополнительно фиксируются основание, полномочия, версия, подтверждения, свидетельства и порядок пересмотра или спора. Указание одного ресурса в нескольких обещаниях требует проверки совместной выполнимости.
Ответственность исполнителя рассматривается вместе с обязательствами предоставить ресурсы, решения и доступ. Руководители, обеспечивающие службы и оператор системы также имеют проверяемые обязательства. Обязательство группы опирается на полномочия её представителя и внутренние обеспечивающие обязательства; раскрываются только необходимые другим сторонам сведения.
Как работает протоколПроект языка описания обязательств, полномочий и переходов.
Объекты и связи
Участник, цель, полномочие, ресурс, действие, обязательство, условие, зависимость, свидетельство и приёмка. Запись обязательства связывает стороны, ожидаемый результат, срок и основания подтверждения. Известная участникам сеть не отождествляется со всеми фактическими зависимостями деятельности.
Переходы и кандидаты инвариантов
Необходимо определить предложение, подтверждение, исполнение, приёмку, пересмотр и спор. Кандидаты инвариантов: действие требует надлежащего полномочия; изменение среды само не переписывает соглашение; история условий сохраняется; исполнение и приёмка различаются. Это проект требований, а не уже проверенные теоремы.
Граница доказательства
Формальная совместимость обязательств не гарантирует достижения общих целей. Даже выполненная сеть может опираться на ошибочные сведения, пропускать важные зависимости или обеспечивать лишь промежуточные результаты. Приёмка отдельной работы и успех организации оцениваются раздельно.
Артефакты и статус
Статус: проект спецификации. Определения на этой странице — доступный артефакт. Чтобы назначить статус «Формально проверено», нужны версия исполняемой спецификации, точные свойства и допущения, инструмент, границы проверки и воспроизводимый результат. Такой пакет здесь пока не представлен.