Доказательство правильности систем
В 80-е годы было модно говорить о "языках спецификаций" (тогда не говорили о "моделировании", а именно что о "спецификации"), из которых целевая система появлялась путем последовательного их уточнения и последующей генерации кода (на языке высокого уровня, или даже сразу в машинный язык). В 90-е годы к этому добавили то, что таким образом "специфицированные" системы могли бы быть с "доказанным соответствием спецификациям". В те поры было множество разработок на эту тему ("доказательство правильности программ"), на которые я особо не смотрел: мне всегда казалось, что программа сама по себе может быть сколько угодно правильна, но достигать неверной цели.
Одной из самых успешных работ в этом направлении был подход B, основанный на теории множеств. 1998 году была запрограммирована линия 14 метро METEOR (Париж). 86тыс. строк кода, до сих пор в версии 1.0, и до сих пор не замечено ошибок.
Но уже следующие линии метро (а применения этого подхода пошли главным образом по железнодорожной части, хотя хватало и других применений) показали, что ошибки таки бывают -- а успех первой реализации был связан с тем, что повышенное внимание уделялось системной инженерии (работе на уровне системы), а не ограничивались вознёй с целевой программой. После того, как это отследили, на рубеже столетия подход B был сознательно эскалирован на уровень системы: назван Event-B, в котором не только прямо говорилось не о софте, а о системе, но и "операции и методы" были заменены на "события". Обзор Event-B -- http://www.bmethod.com/pdf/grace-2010/event-b-overview.pdf
Сейчас Европа закачивает в данный подход деньги налогоплательщиков, получая разнообразный софт для B-моделирования и валидации получающихся моделей. Тут нужно заметить, что получатели этих денег главным образом во Франции.
Меня это все заинтересовало, поскольку появились работы, прямо адресующие разрыв между непонятностью формальных спецификаций и понятностью представления результатов неспециалистам:
-- ProB validation tool поддерживает множество языков спецификаций (B, Z, CSP, Event-B, Promela, dSL, ...) и позволяет делать анимации для того, чтобы эксперты, ничего не понимающие в спецификационных математических нотациях, могли понять то, что за этими нотациями скрывается (http://www.bmethod.com/pdf/grace-2010/pro-b-tokyo-2010.pdf).
-- controlled English для написания требований, из которых потом генерируются спецификации на B, а уж эти спецификации затем контролируются на целостность (http://doi.acm.org/10.1145/1734103.1734114)
Подробности можно копать отсюда:
-- свежайшие (март 2010) презентации в изобилии http://www.bmethod.com/php/conference-grace-2010-en.php
-- гнездо Event-B тут: http://www.event-b.org/ (и там изобилие ссылок)
-- ресурс по B методу компании ClearSy System Engineering: http://www.bmethod.com/ (и там еще ссылки на инструменты)
Еще мне интересна сама постановка задачи доказательства правильности систем по аналогии доказательства правильности программ. Похоже, что скоро нужно любой тезис из software engineering или computer science про программы как first class object переносить на системы. С другой стороны, B-моделирование забирается уже внутрь программы/системы. Поэтому можно ожидать, что скоро для системы будет переформулировано и знаменитое "программа = алгоритмы + данные". "Система = ???". И непонятно, что будет быстрее: самому придумать, как это будет в случае систем, или просто подождать годик-другой, пока другие придумают.
Одной из самых успешных работ в этом направлении был подход B, основанный на теории множеств. 1998 году была запрограммирована линия 14 метро METEOR (Париж). 86тыс. строк кода, до сих пор в версии 1.0, и до сих пор не замечено ошибок.
Но уже следующие линии метро (а применения этого подхода пошли главным образом по железнодорожной части, хотя хватало и других применений) показали, что ошибки таки бывают -- а успех первой реализации был связан с тем, что повышенное внимание уделялось системной инженерии (работе на уровне системы), а не ограничивались вознёй с целевой программой. После того, как это отследили, на рубеже столетия подход B был сознательно эскалирован на уровень системы: назван Event-B, в котором не только прямо говорилось не о софте, а о системе, но и "операции и методы" были заменены на "события". Обзор Event-B -- http://www.bmethod.com/pdf/grace-2010/event-b-overview.pdf
Сейчас Европа закачивает в данный подход деньги налогоплательщиков, получая разнообразный софт для B-моделирования и валидации получающихся моделей. Тут нужно заметить, что получатели этих денег главным образом во Франции.
Меня это все заинтересовало, поскольку появились работы, прямо адресующие разрыв между непонятностью формальных спецификаций и понятностью представления результатов неспециалистам:
-- ProB validation tool поддерживает множество языков спецификаций (B, Z, CSP, Event-B, Promela, dSL, ...) и позволяет делать анимации для того, чтобы эксперты, ничего не понимающие в спецификационных математических нотациях, могли понять то, что за этими нотациями скрывается (http://www.bmethod.com/pdf/grace-2010/pro-b-tokyo-2010.pdf).
-- controlled English для написания требований, из которых потом генерируются спецификации на B, а уж эти спецификации затем контролируются на целостность (http://doi.acm.org/10.1145/1734103.1734114)
Подробности можно копать отсюда:
-- свежайшие (март 2010) презентации в изобилии http://www.bmethod.com/php/conference-grace-2010-en.php
-- гнездо Event-B тут: http://www.event-b.org/ (и там изобилие ссылок)
-- ресурс по B методу компании ClearSy System Engineering: http://www.bmethod.com/ (и там еще ссылки на инструменты)
Еще мне интересна сама постановка задачи доказательства правильности систем по аналогии доказательства правильности программ. Похоже, что скоро нужно любой тезис из software engineering или computer science про программы как first class object переносить на системы. С другой стороны, B-моделирование забирается уже внутрь программы/системы. Поэтому можно ожидать, что скоро для системы будет переформулировано и знаменитое "программа = алгоритмы + данные". "Система = ???". И непонятно, что будет быстрее: самому придумать, как это будет в случае систем, или просто подождать годик-другой, пока другие придумают.