В октябре на симпозиуме по операционным системам, проводимом aссоциацией вычислительной техники Association for Computing Machinery, специалисты Массачусетского технологического института собираются представить файловую систему, гарантирующую отсутствие потерь данных при сбоях, которые могут быть вызваны отказами питания, программными и аппаратными ошибками и т. п. Как отмечают исследователи, добиться того, чтобы файловая система могла восстановиться после любых сбоев, трудно, поскольку приходится учитывать слишком много вероятных событий. Поэтому они решили обеспечить надежность с помощью методов формальной верификации — математического описания допустимых рабочих режимов программы и доказательства того, что она никогда не нарушит этих границ. Авторам, по их словам, пришлось на языке Coq описывать, что такое бит, накопитель и т. п., а затем задавать связи между различными компонентами файловой системы в условиях сбоя. После этого было проведено доказательство того, что система будет работать согласно спецификациям, а затем написан сам код.

Купить номер с этой статьей в PDF