JК
Мифы о безопасном ПО - уроки знаменитых катастроф :: Аджиев Валерий
Страница: 34 из 44Вопрос, реалистично ли ожидать, что для систем масштаба Ariane 5 возможно выполнить полный цикл доказательства правильности всего ПО, остается открытым. ет сомнений, однако, что для отдельных подсистем такая задача может и должна ставиться уже приводились аргументы о полезности использования формальных методов при разработке механизмов синхронизации в Therac-25.
Формальные методы разработки это тема специального большого разговора. Здесь же в качестве примера формального подхода, имеющего промышленные перспективы, упомянем только "B-Method" [9], получивший недавно широкое паблисити в связи с созданием ПО для автоматического управления движением на одной из линий парижского метро. Разработчик метода Жан-Раймон Абриал (J.-R.
Abrial), до того известный как создатель формального метода Z (вошедшего в учебные программы всех уважающих себя университетов), использовал идеи таких классиков, как Эдсгар Дийкстра (E.W.Dijkstra) и Тони Хоар (C.A.R.Hoare).
Важно, что основанная на формализмах методология поддержана практической инструментальной средой разработки Atelie B (которая, кстати, не единственная).
Формальные методы разработки это тема специального большого разговора. Здесь же в качестве примера формального подхода, имеющего промышленные перспективы, упомянем только "B-Method" [9], получивший недавно широкое паблисити в связи с созданием ПО для автоматического управления движением на одной из линий парижского метро. Разработчик метода Жан-Раймон Абриал (J.-R.
Abrial), до того известный как создатель формального метода Z (вошедшего в учебные программы всех уважающих себя университетов), использовал идеи таких классиков, как Эдсгар Дийкстра (E.W.Dijkstra) и Тони Хоар (C.A.R.Hoare).
Важно, что основанная на формализмах методология поддержана практической инструментальной средой разработки Atelie B (которая, кстати, не единственная).