конечные автоматы для верификации
May. 8th, 2010 03:29 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
juan_gandhiТут в разговоре про очередного, имхо, шарлатана, профессора Шалыто, выяснилось, что есть такая идея, будто для верификации программ достаточно FSM, конечного автомата.
Вот скажите мне, возьмём такой пример: даден алфавит, {a, b}, и две программы, одна генерирует все палиндромы в этом алфавите, вторая проверяет, что данная строка является палиндромом.
Скажите, какой конечный автомат может верифицировать эти программы?
Вот скажите мне, возьмём такой пример: даден алфавит, {a, b}, и две программы, одна генерирует все палиндромы в этом алфавите, вторая проверяет, что данная строка является палиндромом.
Скажите, какой конечный автомат может верифицировать эти программы?
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2010-05-08 11:00 pm (UTC)no subject
Date: 2010-05-08 11:15 pm (UTC)no subject
Date: 2010-05-09 12:23 am (UTC)То, что верификация хардвера существует (как распостраненное занятие), а верификация софтвера - нет, объясняется не только "конечностью" хардвера, но и более высокими требованиями к качеству, чем у софтвера (после отправления дизайна на фабрику его не поменяешь (за исключением FPGA)). Верификация софтвера (I guess) наверное имеет практический смысл только для RTOS, которые маленькие, сильно параллельные, и имеют четко определенные абстракции (threads, mailbox, semaphore) и т.д.
no subject
Date: 2010-05-09 12:32 am (UTC)no subject
Date: 2010-05-10 07:09 pm (UTC)no subject
Date: 2010-05-10 07:43 pm (UTC)no subject
Date: 2010-05-10 08:01 pm (UTC)То что у программы потенциально бесконечное количество возможных исполнений тут совершенно ни при чем. Верификация исполнений называется "тестирование" и действительно является занятием интеллектуально малопродуктивным. Как известно от классика она подтверждает только наличие ошибок, но не их отсутствие.
Верификация программ (а не их исполненений) рассматривает программу как математический объект - формулу, конечной длины, и доказывает о нем некоторые теоремы. Никакой разницы с верификацией аппаратуры в принципе нет.
no subject
Date: 2010-05-09 12:41 am (UTC)А вот программные продукты для верификации софтвера я не знаю, поэтому и спрашиваю. Я предполагаю, что они должны существовать для RTOS, которые маленькие, сильно параллельные, и имеют четко определенные абстракции (threads, mailbox, semaphore) и т.д. Но тогда встает вопрос - что для таких программ верификации является входным языком, который они парсируют? С/C++/Java? Эти языки труднее верифицировать, чем RTL-подмножество верилога ИМХО, ибо в них главную роль играют всякие динамические структуры (деревья с поинтерами), семантика которые на уровне языка не особенно видна (в то время как из кода на верилоге можно извлечь state machine).
no subject
Date: 2010-05-09 12:53 am (UTC)no subject
Date: 2010-05-09 01:31 am (UTC)no subject
Date: 2010-05-09 01:32 am (UTC)no subject
Date: 2010-05-09 12:07 am (UTC)Практически, задача у верификации - доказать, что система не выдаст ошибочного значения. Правда, самая надёжная система - та, которая выключена. Но это тоже удовлетворяет условию задачи, хоть мало кто об этом любит говорить.
Приличные системные требования, что я видел, описывались в таблицах переходов. (Хотя, софтверные люди и утверждали, что это прошлый век и не модно.) Естественно, размеры таблиц очень невелики.
no subject
Date: 2010-05-09 12:29 am (UTC)Ну я ж русским языком пишу "практически"
В большинстве случаев она выдаёт правильное значение. В остальных - падает кверху лапками и производит перезапуск. Если может.
no subject
Date: 2010-05-09 12:43 am (UTC)no subject
Date: 2010-05-09 01:00 am (UTC)Тут в каждой строчке нарушены базовые требования любого стандарта на кодирование.
no subject
Date: 2010-05-09 01:12 am (UTC)Вторым, обычно идёт бесконечный цикл чтения входных значений и выдача выходных. Если программа в том же самолёте остановится, то пилотам придётся очень туго. А Арианы, те просто взрываются.
Весёлым же местом в таких системах являются не зацикливания, а дидлоки. Беда в том, что о существовании асинхронных не все специалисты подозревают. А оттестировать такое дело очень и очень сложно.
no subject
Date: 2010-05-09 01:43 am (UTC)no subject
Date: 2010-05-09 02:06 am (UTC)no subject
Date: 2010-05-09 02:13 am (UTC)no subject
Date: 2010-05-09 02:31 am (UTC)Тезис был про то, что "Практически, задача у верификации - доказать, что система не выдаст ошибочного значения." То есть то, чем некто Ш. может заниматься.
Но спор как-то перекинулся на "теория против практики". Ш. упирал именно на практику. Если у Ш. есть какие-то теории, я априори не очень верю, но искать блох мне влом.
no subject
Date: 2010-05-09 02:27 am (UTC)1) если заменять на полностью систему, то туда придётся включать железо. Так что кнопка "рестарт" входит.
2) в общем случае верификация является утверждением, а не доказательством.
Теоретическое доказательство я видел только в очень редких случаях. Точнее, не видел, а читал отчёты об успешном проведении. Судя по тому, что делал в одном проекте математик, у меня в успешности большие сомнения.
3) работает фактор ответственности. То есть, выдача неправильного ответа - это провал. Невыдача ответа - срабатывание защиты.
Насколько понимаю там, где время ответа важно, стоит просто по рабоче-крестьянски следящая система, которая элементарно убивает застрявший процесс и запускает всё по новой. Не думаю, что даже в университетах пытаются найти доказательства для неэлементарных систем, получающих случайные асинхронные внешние воздействия.
Про лайвлоки - да. Но, подозреваю, условия в реальности для них возникают очень редко.
no subject
Date: 2010-05-09 09:21 am (UTC)Как сравнивается объём кода известных систем этого тира с теми системами, которые делает Ш.? Решают ли эти системы те же задачи?
является доказательством
...но во многих практических случаях она решается с применением разных эвристических методов.
Не понял. Также не понял, как мы будем это рассматривать в реалтайме для взаимодействия двух систем.
невыдача ответа вовремя в системе реального времени - это по определению провал.
Я тоже так думал. В документах, что я видел, стоит иное. Система несколько раз перезапускается. Если неудачно, то просто вырубается.
В принципе, системы дублируются. Так что ошибочную просто убивают. То, что ошибки происходят редко, идёт за счёт массированного тестирования. Софт без железа при вычислении общей надёжности не рассматривают. Потому как сбои памяти тоже учитываются.
Ладно. Это был мой последний выпад.
no subject
Date: 2010-05-09 01:13 am (UTC)Любой тезис можно доказать, приведя левый, не относящийся к делу аргумент.
no subject
Date: 2010-05-09 01:42 am (UTC)no subject
Date: 2010-05-09 02:04 am (UTC)По существу, верифицировать можно только вполне определённый класс задач на вполне определённом множестве. Кстати, палиндромов это тоже касается.
Короче говоря, если мы говорим о поезде, то он ездит по рельсам. Если не по рельсам, то это уже не поезд.
А так, да. Разговор идёт мимо.
no subject
Date: 2010-05-09 12:39 am (UTC)no subject
Date: 2010-05-09 01:44 am (UTC)no subject
Date: 2010-05-09 08:37 am (UTC)Идея примерно такая. Сначала формулируем свойство, которое хочется проверить. Затем, ориентируясь на это свойство, строим модель программы, которая отражает все, что важно с точки зрения нашего свойства, а все остальное игнорирует. Модель может быть в разных формах, на практике чаще всего используют Spin, который тут уже упоминали, и описывают поведение программы на языке Promela. Потом по этому описанию строится структура Крипке: набор логических переменных, набор состояний, о каждом из которых известно, истинна или ложна в нем каждая переменная, и набор переходов между состояниями. Свойство, которое хочется проверять, записываем формально в какой-нибудь темпоральной логике (автоматный подход используется обычно для логики LTL). Берем отрицание полученной формулы. Дальше по структуре Крипке строим автомат Бюхи, он будет допускать возможные в системе (бесконечные) последовательности интерпретаций набора переменных. По LTL-формуле отрицания свойства тоже строим автомат Бюхи, он будет допускать такие последовательности интерпретаций переменных, которые нарушают интересующее нас свойство. Проверяем, что произведение этих автоматов допускает пустой язык. Это значит, что ни одна траектория в структуре Крипке не нарушает интересующего нас свойства. Если язык не пуст - это множество контрпримеров. Входными символами для автоматов являются интерпретации логических переменных структуры Крипке, которые обычно вычисляются на основе входов, выходов и иногда состояний анализируемой системы, так что можно потом по набору значений этих переменных определить, какие собственно входные воздействия имели место - каждый контрпример оказывается воспроизводимым багом.
Формально любой компьютер, выполняющий любую программу - это конечная система, но состояний там слишком много. Поэтому верифицируют (как и в случае с железом) не реальный код, а его модель. Хочется строить такие модели с как можно меньшими затратами человеческого труда, но здесь, мне кажется, еще работать и работать. До промышленного повседневного применения далеко, хотя есть интересные результаты (Java PathFinder (http://babelfish.arc.nasa.gov/trac/jpf), например).
no subject
Date: 2010-05-09 04:22 pm (UTC)no subject
Date: 2010-05-09 01:05 am (UTC)ispal x = x == reverse x
Можно ли верифицировать ее правильность конечным автоматом? Это же практически определение палиндрома, доказывать нечего. Может ли конечный автомат проверить, правильно ли записано определение? Хрен его знает, почему бы и нет? Во всяком случае, к какому классу относится язык, принимаемый программой, здесь вроде бы не играет роли. Нам больше интересен язык, на котором она написана.
no subject
Date: 2010-05-09 01:44 am (UTC)no subject
Date: 2010-05-09 02:28 am (UTC)no subject
Date: 2010-05-09 03:34 pm (UTC)no subject
Date: 2010-05-09 05:12 pm (UTC)no subject
Date: 2010-05-10 02:36 am (UTC)Всё опирается как раз на логику и типы,
это не
бином Ньютонаконечные автоматы.http://adam.chlipala.net/cpdt/
no subject
Date: 2010-05-10 01:04 pm (UTC)no subject
Date: 2010-05-10 02:05 pm (UTC)no subject
Date: 2010-05-10 02:34 pm (UTC)Верификация программного обсепечения, неизвестная
no subject
Date: 2010-05-10 05:36 pm (UTC)Так если я повторю вопрос, можно ли на си написать программу, которая проверяет паритет скобок в другой программе?
no subject
Date: 2010-05-10 06:36 pm (UTC)По поводу скобок. Если "другая программа" задается через char getnextsymbol() то в общем случае нельзя, т.к. вложенность скобок может превысить любое значение представимое в данной реализации Си.
no subject
Date: 2010-05-10 07:42 pm (UTC)no subject
Date: 2010-05-10 08:06 pm (UTC)no subject
Date: 2010-05-10 08:23 pm (UTC)Может быть, Вы тут излагаете что-нибудь вроде нестандартного анализа, кто Вас знает, а я лезу с чепухой вроде континуума.
Потому что есть много различных взглядов на как бы одну и ту же вещь.
no subject
Date: 2010-05-10 09:02 pm (UTC)Конечный автомат всегда либо останавливается за конечное число шагов либо повторяет уже бывшее состояние и тогда не остановится никогда. Отсюда легко понять, что для класса конечных автоматов с числом состояний менее данной константы можно сделать универсальный конечный автомат который их будет верифицировать. Верифицировать в том смысле что он будет говорить остановится ли данный конечный автомат и если да то в каком состоянии. Это был ответ на исходный вопрос можно ли программы верифицировать конечными автоматами: программы на C можно.
Далее возник обратный вопрос. Можно ли проверить программой на C т.е. конечным автоматом парность скобок. Ответ вроде бы очевиден - нет. "Вообразить" бесконечно большую виртуальную память нельзя в том смысле, что это будет не расширением языка "С", а противоречивой системой. В C все типы включая указатели имеют только конечное количество значений. На этом построен весь язык начиная от массивов.
no subject
Date: 2010-05-10 09:42 pm (UTC)no subject
Date: 2010-05-10 09:56 pm (UTC)no subject
Date: 2010-05-10 10:57 pm (UTC)no subject
Date: 2010-05-10 11:39 pm (UTC)no subject
Date: 2010-05-11 07:16 am (UTC)no subject
Date: 2010-05-11 02:25 pm (UTC)no subject
Date: 2010-05-11 02:49 pm (UTC)The ability to create and destroy files from the above finite set is of little interest: there still is a finite constant N such that no program can at any point of its execution store more than N bits of data in files. This, together with the finiteness of addressable storage, means that the program is a finite state machine.
no subject
Date: 2010-05-11 05:19 pm (UTC)no subject
Date: 2010-05-11 06:34 pm (UTC)