Обсуждение

"Система=Объекты+связи"?

Черной завистью завидую французам, которые работают над такими прогами. :(

Нет, "объекты и связи" явно не отсюда (ближе всего было бы подсистемы и интерфейсы -- но и так не про то).

Еще мне интересна сама постановка задачи доказательства правильности систем по аналогии доказательства правильности программ. Можно построить по аналогии с программированием. Спецификацией системы будет формальное описание требований. А реализацией - какой-то проект/план/модель будущей системы. Соответственно, нужно доказать, что реализация соответствует формальным требованиям. В (псевдо)математической нотации: Допустим, A - сигнатура модели (грубо говоря, формальное описание входов/выходов, типа A : In -> Out), Req(a) - предикат, заданный на множестве этих сигнатур. В другой форме, Req(in, out). Предикат задает требования, т.е. те сигнатуры, на которых предикат выполним, являются корректными реализациями. Соответственно, задача проверки корректности требований, состоит в том, чтобы доказать, что Exists a : A, Req(a). В другой форме Exists f : In->Out, Forall x, Req(x, f(x)). Если доказательство, конструктивное, то по нему можно извлечь и саму модель, отвечающую требованиям. Но на практике, модель нужно разрабатывать отдельно, потому как в целях удобство доказывания, модель должна иметь структуру, отличную от той, которую нужно применять в реальности (грубо говоря, экономить нужно другие ресурсы). И потом доказывать, что сия модель соответствует спецификации. Соответственно, возникают три подзадачи: 1. формальное задание сигнатуры целевой системы (тип преобразования входов в выходы) 2. построение предиката задающего требования (например, бинарный предикат на парах вход/выход) 3. построение модели целевой системы, имеющей нужную сигнатуру, и доказательство, того, что модель соответствует требованиям Все это довольно сложно и трудоемко, но на практике, даже простенькие частичные формализации часто весьма полезны для понимания требований.

Для систем, связанных с безопасностью на такую сложность и трудоёмкость вполне идут -- овчинка стоит выделки. А вот для других систем нужно понять, что легче делать "в псевдокоде", а что не легче. Люди, изучающие использование UML в проектах, рапортуют сейчас, что использование UML для промежуточного моделирования только ухудшает проектные характеристики...

Проектные характеристики отражают затягивание и удорожание проектов, но не отражают тех проблем, которых удалось избежать путем применения формальных методов. Так что тут надо осторожно изучать эти оценки. В целом же конечно, на данный момент так дело и обстоит. Ибо всякие формализации весьма затратны на данный момент. В частности, UML предполагает прямую генерацию кода как правило, а код сей не удобен в реальном использовании. Т.е. нужно делать непрямую трансляцию, а гибко настраиваемую. А таких тулзов на данный момент нет, либо они слишком сложны в изучении. Поэтому, мне в реальных проектах формальные методы пока не удалось применить. Исключая разве что тестирование, где в ограниченном виде кое что удается. Но на этапе анализа требований - без последующей генерации программного кода - формальные методы думаю почти всегда полезны. Ибо на этом этапе, ошибки наиболее дешевы. Поэтому имеет смысл потратить усилия сейчас, чтобы не мучаться на этапе реализации и тестирования. Возможно это ухудшит проектные характеристики, затягивая фазу дизайна. Ну а что делать, кому сейчас легко? :)

Ибо на этом этапе, ошибки наиболее дешевы. Неправильно выразился - ошибки наоборот наиболее дороги. А наиболее дешевы инструменты предотвращения этих ошибок.

А если задачей системы является не сформировать определенный вывод данных, а например, поддерживать состояние внутренних элементов (например, при системной инженерии дома престарелых)? Тут с бинарным предикатом может не получиться.

Здесь выходом будут состояния внутренних элементов. А поддерживать состояния - значит есть какие-то ограничения, а ограничения уже можно задавать предикатами.

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

Вот для того чтобы обеспечить адаптивность, формализация и является крайне полезным мероприятием. Для дома престарелых, это может и избыточно, а вот для какого-нить кардиостимулятора, или иного медицинского оборудования очень даже актуально. А то престарелый или просто больной может запросто откинуть копыта раньше срока из-за сбоя в программе.

Ценю Ваш юмор. Но на мои доводы Вы не ответили. Я говорил, что формализация в виде предиката, который соотносит ввод и вывод системы (и дальше оперирует только этим) может оказаться неудобной в ряде случаев, касающися, прежде всего, сервисоориентированных систем со слабо формализуемым (по принципиальным соображениям) заказчиком. Это не значит, что надо отказываться от формализации, это всего лишь значит, что данный путь формализации - не оптимален. В качестве альтернатив более приемлема процессно-ориентированная формализация, отталкивающаяся от, например, методологии ITIL. Там конструкция несколько сложнее, чем просто базовые предикаты с вводом и выводом, вернее даже так - отдельные процессы там вполне укладываются в предикатную логику, но кроме нее в системе есть еще архитектура, которая описывает взаимодействие этих черных ящиков. Из чего делаю вывод - что предикатов, вообще говоря, не достаточно для выделения всех требований (например, требований, которые будут связаны с требуемой логикой взаимодействия с пользователем по доформализации самих требований), и более правильно рассматривать систему по слоям, где предикатам есть законное (но не главенствующее) место.

Мы видимо на несколько разных уровнях оперируем. В практической деятельности, безусловно оперировать бинарными предикатами не всегда удобно, мягко говоря. Но я писал про другое. Есть определенная методология формализации. Любая система динамична - она реагирует на какие-то события и порождает какие-то ответные реакции (ибо если система не шевелится, то она на хрен никому не нужна). Таким образом можно описать и классифицировать входные события и выходные реакции. И построить модель системы связав вход и выход какой-то функцией. Т.е. такую функция всегда можно построить до нужной степени приближения - это вопрос затрачиваемых усилий и квалификации моделера. Это касается и домов престарелых и процесно-ориентированных архитектур. Также на основе классификации входов и выходов, можно определить, какие сценарии развития событий нежелательны. Таким образом, возникает ограничения на множестве пар входов/выходов, т.е. предикат. Он бинарный в том, смысле, что у него два параметра. Но это обобщенная ситуация. На практике, конечно его можно описывать какими-то комбинацими предикатов, или функций и прочих символов. Но все они все равно приводимы к общему виду, когда есть обобщенное множество входов, множество выходов (любые предикаты сводимы к бинарным, функцию тоже можно моделировать предикатами). Есть множество функций, преобразующих входы в выходы. Есть предикат, который говорит, какие пары входов/выходов правильные, а какие нет. На уровне подсистем это тоже верно. Т.е. можно задавать контракты для черных ящиков, что они должны вести себя определенным образом. Тогда можно дать какие-то гарантии для протоколов взаимодействия таких черных ящиков, при условии, что они соблюдают контракты. Ну и т.д. При этом конечно, возможности формализации ограниченны - прежде всего затратами на проведение этой формализации. Поэтому в слабоформализуемых областях применять формализмы и прочие предикаты, может особого смысла и нет (а с другой стороны, всегда можно напороться на неожиданно простую и продуктивную формализацию).

Ну почему же, по-моему мы с Вами вполне на одном уровне. С теоретической возможностью все свести к бинарным предикатам я не спорил. Я только говорил, что конкретный вид этого предиката (который был бы адекватен функциональному преобразованию всех возможных входов и выходов, особенно в системах с глубокой памятью, где неудачное воздействие может аукнуться через несколько лет) может быть чрезвычайно сложен, потому принципиально (в силу формальных ограничений) не выводим аналитически. Т.е. все упирается не в квалификацию моделера, а в разрешимость определенных формальных задач. Проблема серьезнее, чем может показаться на первый взгляд. Я ее разумеется глубоко не исследовал, но по ощущениям, попытка формального предикатного описания всей системы даже в довольно простых случаях (процессная модель help desk) окажется неразрешимой. Как следствие, с практической точки зрения неизбежно введение архитектурного (или точнее - семантического) уровня описания, который будет работать с отдельными весьма небольшими подсистемами, которые можно уже будет описать предикативно. Я даже более того скажу, имея предикативное описание подпроцессов, можно вполне соорудить так Вами любимый МЕГАПРЕДИКАТ, который описывал бы всю систему с учетом всего многообразия (мерности и динамики) входа и выхода. Только вот боюсь, аналитически доказать "правильность" этого предиката (я так понимаю, что таковым доказательством Вы видите его разложение по ряду предикатов - функциональных требований) вероятнее всего не получится. Итого, придется семантику (архитектуру) анализировать с целью доказательства ее корректности отдельно (не предикативными методами), а отдельные суб-системы - отдельно, возможно, даже и предикативными методами.

Никаких формальных ограничений, чтобы строить сложные предикаты нет. Ведь пишут очень сложный софт и ничего. А по любой функции (а софт это тоже такая сложная функция по преобразованию входов в выходы), можно построить предикат. Тут никаких принципиальных проблем, кроме как инженерно-экономических (вопрос ресурсов) и философо-онтологических нет. Более того, ограничения обладают аддитивным свойством: т.е. если к набору ограничений добавить еще одно, то это точно так же будет набор ограничений. Поэтому в реальности, предикаты еще и проще задавать, нежели написать функцию, которая бы "вычисляла" сей предикат. Тут естественно, есть риск переограничить, так что предикат будет пустым множеством, но это решаемая проблема. Модели тоже нужно отлаживать как и программы. Вот с доказательство действительно будут проблемы, но это опять же инженерный вопрос. Грубо говоря, нефиг формулировать такие формализмы, которые трудно верифицировать :). Это вобщем-то тоже вопрос квалификации. Более того, преодоление всех этих сложностей с формулированием и верификацией и дает прекрасное и глубокое понимание требований предметной области. Даже если по этому пути продвинутся лишь частично. Например, описать входы входы и выходы, рассмотреть какие-то подмодели. Преодоление трудностей с формализацией и верификацией дает знание, которого ни у кого больше нет.

Собственно в этом и различаются наши позиции. Относительно софта автор уже выразился в том смысле, что доказательство корректности работы программы (любой) можно провести, т.к. любая программа есть в пределе конечный автомат, для которого по определению можно построить как точный (бинарный) предикат, так и всевозможные его модельные приближения (в т.ч. с выделением существенных требований). По отношению к системам такого сказать к сожалению нельзя, т.к. например человеко-машинные системы уже конечным автоматом не являются (в силу наличия в них неопределенности, связанной с человеческим фактором). Опять же - ситуация с ограничениями. Практически гарантировано, если Вы начнете задавать ограничения методом отсечений (т.е. описывать слабоформализованные области, куда системе можно ходить, а куда нельзя) то Вы нарветесь на невыполнимый предикат гораздо раньше, чем сможете описать поведение системы с многочисленными обратными связями, внутренними состояниями и сложными переходами между ними, по крайней мере, если не захотите работать в пространстве, мерность которого равна суммарному количеству степеней свободы системы (которое при слабой формализации области может быть катастрофически велико для реальных систем). С этой сложностью неизбежно придется бороться структурными методами. Поэтому чисто предикативная методика, ИМХО, обречена именно потому, что с доказательством будут неразрешимые проблемы. Эти проблемы огребли по полной японцы, когда начали на Прологе пытаться сделать компьютер пятого поколения. Проект, насколько мне известно, загнулся, проглотив полмиллиарда баксов. Хотя ребят сложно обвинить в некомпетентности и в том, что они сознательно формулировали сложно верифицируемые формализмы. Кстати, и наши работы по ИИ (например, см. ВИНИТИ, работы В.К.Финна) говорят, что если начать работать все-таки со структурной информацией (графами) и использовать более гибкие системы рассуждений (т.н. правдоподобный вывод), то можно добиться куда большего, чем тупо пытаться соорудить предикат, описывающий систему. И к слову, чем Вас так не устраивает знание, которое получается в процессе правдоподобного вывода или рассуждений на графах, чем оно хуже предикативных утверждений? ИМХО, именно там и надо копаться в поисках приемлемого формализма, а не в предикатах, как таковых.

Только вот боюсь, аналитически доказать "правильность" этого предиката (я так понимаю, что таковым доказательством Вы видите его разложение по ряду предикатов - функциональных требований) вероятнее всего не получится. Задача верификации состоит не в доказательстве "правильности" предиката. Предикат как раз задает требования, которым должна удовлетворять реализация - последнее и нужно доказать. Конечно "правильность" предиката тоже нужно проверять, куда без этого. В частности, это можно делать методом доказательства - например доказывая, что у системы удовлетворяющей предикату, есть те или иные свойства. Хотя, в идеале, эти свойства лучше сразу задать как требования, т.е. включить в предикат. Но вообще, типа принимается, что требования изначально правильны :). Ну и предикат тоже :). Потому как, а с чем их еще сравнивать? Где взять эталон? А если есть где взять, тот как проверить правильность эталона? На практике, конечно, есть несколько разных документов, как формальных так и неформальных, ну и нужно их синхронизировать. Часть этого процесса можно формализовать и даже строго верифицировать. Но всегда будет и неформальная часть. Фактически, доказательство есть сведение к каким-то предположениям, аксиомам, которые принимаются изначально верными (в контексте доказательства). Если в процессе выясняется, что с аксиомами что-то не так - а это обычно выясняется - то это весьма и весьма ценная информация. Ибо неявные допущения присутствуют всегда. Задача формализации - вытащить их на свет божий.

Хорошо. Предлагаю завершить дискуссию на следующем тезисе. Дескрипционная логика http://ru.wikipedia.org/wiki/Дескрипционная_логика, которая предоставляет богатый аппарат для накопления и верификации знаний (частный случай - знания о соответствии системы требованиям), а также дает инструментарий для вывода, конечно сводима к предикатам. Однако структурная информация (об архитектуре и процессах в системе) в ней может быть отделена от информации предметной (как конкретно действует тот или иной элемент). В силу того, что многие системы (особено антропоцентрические) предполагают по умолчанию возможность изменения требований, то доказать правильность системы можно только в каком-то одном view point. Например, с точки зрения текущего реестра требований. Или с точки зрения эффективности процедур адаптации системы к новым требвоаниям. Для первого предикативная форма возможна, но вероятно, не очень удобна, особенно в контексте вычислимости (всякое ли требование или суперпозицию требований можно представить в виде вычислимого предиката, а также даже зная конкретный вид предиката - для каждого ли можно алгоритмически найти процедуру, которая обернет этот предикат в единицу). Для второго - переходить от структурного описания в дескрипционной логике к ее предикативному отоборажению бессмысленно, т.к. именно структурная (процессная) информация является определяющей, и соответственно, доказательство правильнее всего строить в дескрипционной логике. Если не согласны - любопытно, в чем.

т.к. например человеко-машинные системы уже конечным автоматом не являются (в силу наличия в них неопределенности, связанной с человеческим фактором У меня такое впечатление, что Вы хотите меня убедить в том, что есть области, которые принципиально неформализуемы :). В реальности, ситуация гораздо хуже: даже там, где формализация возможна, затраты на нее весьма велики. Так что по экономическим соображениям, формализация возможна весьма редко. А уж лезть туда, где она еще и неприменима, смысла никакого нет (кроме чисто исследовательского). Опять же - ситуация с ограничениями. Практически гарантировано, если Вы начнете задавать ограничения методом отсечений (т.е. описывать слабоформализованные области, куда системе можно ходить, а куда нельзя) то Вы нарветесь на невыполнимый предикат гораздо раньше, чем сможете описать поведение системы с многочисленными обратными связями, внутренними состояниями и сложными переходами между ними, по крайней мере, если не захотите работать в пространстве, мерность которого равна суммарному количеству степеней свободы системы (которое при слабой формализации области может быть катастрофически велико для реальных систем). Невыполнимые предикаты технически отсеиваются тем же инструментарием, что и в процессе верификации. Грубо говоря, нужно доказывать теоремы существования. Либо задавать предикат конструктивно. Вопрос квалификации опять же. Более того, реальные неформальные требования задаются ровано так же. И поэтому они всегда на практике противоречивы, т.е. невыполнимы. А формализация как раз и дает инструментарий, чтобы это положение дел исправить. С этой сложностью неизбежно придется бороться структурными методами. Поэтому чисто предикативная методика, ИМХО, обречена именно потому, что с доказательством будут неразрешимые проблемы. Эти проблемы огребли по полной японцы, когда начали на Прологе пытаться сделать компьютер пятого поколения. Проект, насколько мне известно, загнулся, проглотив полмиллиарда баксов. Ну а что Ваши структурные методы невыразимы в предикатах что ли? Одно другому не мешает. Предикаты - лишь другой способ взгляда на мир, формализованный, не более того. Смотреть им конечно сложно, зато возможна строгая проверка. Хотя ребят сложно обвинить в некомпетентности и в том, что они сознательно формулировали сложно верифицируемые формализмы. На тот момент они были компетенты, но с тех пор много времени прошло. Сейчас технологии верификации вполне развиты. Кстати, и наши работы по ИИ (например, см. ВИНИТИ, работы В.К.Финна) говорят, что если начать работать все-таки со структурной информацией (графами) и использовать более гибкие системы рассуждений (т.н. правдоподобный вывод), то можно добиться куда большего, чем тупо пытаться соорудить предикат, описывающий систему. И к слову, чем Вас так не устраивает знание, которое получается в процессе правдоподобного вывода или рассуждений на графах, чем оно хуже предикативных утверждений? ИМХО, именно там и надо копаться в поисках приемлемого формализма, а не в предикатах, как таковых. Я не утверждал, что меня чего-то там не устраивает. Я изначально отвечал на вопрос, цитирую дословно ""Еще мне интересна сама постановка задачи доказательства правильности систем по аналогии доказательства правильности программ."". В контексте сего вопроса, любой ответ будет включать предикатные логики явно или неявно, ибо все системы доказательства правильности программ в конечном итоге основаны на предикатных логиках. Даже если и найдутся не основанные, они к ним сводимы.

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