конечные автоматы для верификации

[juan_gandhi]

Тут в разговоре про очередного, имхо, шарлатана, профессора Шалыто, выяснилось, что есть такая идея, будто для верификации программ достаточно FSM, конечного автомата.

Вот скажите мне, возьмём такой пример: даден алфавит, {a, b}, и две программы, одна генерирует все палиндромы в этом алфавите, вторая проверяет, что данная строка является палиндромом.

Скажите, какой конечный автомат может верифицировать эти программы?

Comments

[vit-r.livejournal.com]

и выдаст правильное значение

Ну я ж русским языком пишу "практически"

В большинстве случаев она выдаёт правильное значение. В остальных - падает кверху лапками и производит перезапуск. Если может.

[vit-r.livejournal.com]

В принципе, у оператора есть кнопка горячего перезапуска. Ну, или детонатор для автономной системы.

[vit-r.livejournal.com]

Уважаемый, писать что-то для такого софта можно не на языке С, С++ или Паскале, а только на строго ограниченном подмножестве.
Тут в каждой строчке нарушены базовые требования любого стандарта на кодирование.

[vit-r.livejournal.com]

Первым делом, в приличных системах не одна программа, а минимум две, работающих параллельно.

Вторым, обычно идёт бесконечный цикл чтения входных значений и выдача выходных. Если программа в том же самолёте остановится, то пилотам придётся очень туго. А Арианы, те просто взрываются.

Весёлым же местом в таких системах являются не зацикливания, а дидлоки. Беда в том, что о существовании асинхронных не все специалисты подозревают. А оттестировать такое дело очень и очень сложно.

[ivan-gandhi.livejournal.com]

У меня такое ощущение, что собеседник немножко поплыл.

[vit-r.livejournal.com]

Я не поплыл. Тут просто четыре часа ночи и мне очень влом.

[ivan-gandhi.livejournal.com]

Ну можно же и не спешить вступать в бой в 4-то часа ночи, а? :)

[vit-r.livejournal.com]

Естественно, я параллельно что-то другое делаю. А завтра будет просто не интересно.

Тезис был про то, что "Практически, задача у верификации - доказать, что система не выдаст ошибочного значения." То есть то, чем некто Ш. может заниматься.

Но спор как-то перекинулся на "теория против практики". Ш. упирал именно на практику. Если у Ш. есть какие-то теории, я априори не очень верю, но искать блох мне влом.

[vit-r.livejournal.com]

Мы говорим о верифицированном компиляторе или о верифицированной системе управления?

1) если заменять на полностью систему, то туда придётся включать железо. Так что кнопка "рестарт" входит.

2) в общем случае верификация является утверждением, а не доказательством.
Теоретическое доказательство я видел только в очень редких случаях. Точнее, не видел, а читал отчёты об успешном проведении. Судя по тому, что делал в одном проекте математик, у меня в успешности большие сомнения.

3) работает фактор ответственности. То есть, выдача неправильного ответа - это провал. Невыдача ответа - срабатывание защиты.

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

Про лайвлоки - да. Но, подозреваю, условия в реальности для них возникают очень редко.

[vit-r.livejournal.com]

а о верификации исходного кода в системе тира spin.

Как сравнивается объём кода известных систем этого тира с теми системами, которые делает Ш.? Решают ли эти системы те же задачи?

является доказательством
...но во многих практических случаях она решается с применением разных эвристических методов.

Не понял. Также не понял, как мы будем это рассматривать в реалтайме для взаимодействия двух систем.

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

В принципе, системы дублируются. Так что ошибочную просто убивают. То, что ошибки происходят редко, идёт за счёт массированного тестирования. Софт без железа при вычислении общей надёжности не рассматривают. Потому как сбои памяти тоже учитываются.

Ладно. Это был мой последний выпад.

[vit-r.livejournal.com]

На всякий случай:
Любой тезис можно доказать, приведя левый, не относящийся к делу аргумент.

[ivan-gandhi.livejournal.com]

О! Вы переводите разговор на совершенно несущественные рельсы. Этот пример, выше - прекрасный пример, очень содержательный. И разговаривать о нём надо по существу.

[vit-r.livejournal.com]

совершенно несущественные рельсы

По существу, верифицировать можно только вполне определённый класс задач на вполне определённом множестве. Кстати, палиндромов это тоже касается.

Короче говоря, если мы говорим о поезде, то он ездит по рельсам. Если не по рельсам, то это уже не поезд.

А так, да. Разговор идёт мимо.