конечные автоматы для верификации
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:07 am (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:29 am (UTC)Ну я ж русским языком пишу "практически"
В большинстве случаев она выдаёт правильное значение. В остальных - падает кверху лапками и производит перезапуск. Если может.
no subject
Date: 2010-05-09 12:32 am (UTC)no subject
Date: 2010-05-09 12:39 am (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:43 am (UTC)no subject
Date: 2010-05-09 12:53 am (UTC)no subject
Date: 2010-05-09 01:00 am (UTC)Тут в каждой строчке нарушены базовые требования любого стандарта на кодирование.
no subject
Date: 2010-05-09 01:05 am (UTC)ispal x = x == reverse x
Можно ли верифицировать ее правильность конечным автоматом? Это же практически определение палиндрома, доказывать нечего. Может ли конечный автомат проверить, правильно ли записано определение? Хрен его знает, почему бы и нет? Во всяком случае, к какому классу относится язык, принимаемый программой, здесь вроде бы не играет роли. Нам больше интересен язык, на котором она написана.
no subject
Date: 2010-05-09 01:12 am (UTC)Вторым, обычно идёт бесконечный цикл чтения входных значений и выдача выходных. Если программа в том же самолёте остановится, то пилотам придётся очень туго. А Арианы, те просто взрываются.
Весёлым же местом в таких системах являются не зацикливания, а дидлоки. Беда в том, что о существовании асинхронных не все специалисты подозревают. А оттестировать такое дело очень и очень сложно.
no subject
Date: 2010-05-09 01:13 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 01:42 am (UTC)no subject
Date: 2010-05-09 01:43 am (UTC)no subject
Date: 2010-05-09 01:44 am (UTC)no subject
Date: 2010-05-09 01:44 am (UTC)no subject
Date: 2010-05-09 02:04 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:27 am (UTC)1) если заменять на полностью систему, то туда придётся включать железо. Так что кнопка "рестарт" входит.
2) в общем случае верификация является утверждением, а не доказательством.
Теоретическое доказательство я видел только в очень редких случаях. Точнее, не видел, а читал отчёты об успешном проведении. Судя по тому, что делал в одном проекте математик, у меня в успешности большие сомнения.
3) работает фактор ответственности. То есть, выдача неправильного ответа - это провал. Невыдача ответа - срабатывание защиты.
Насколько понимаю там, где время ответа важно, стоит просто по рабоче-крестьянски следящая система, которая элементарно убивает застрявший процесс и запускает всё по новой. Не думаю, что даже в университетах пытаются найти доказательства для неэлементарных систем, получающих случайные асинхронные внешние воздействия.
Про лайвлоки - да. Но, подозреваю, условия в реальности для них возникают очень редко.
no subject
Date: 2010-05-09 02:28 am (UTC)