Надежность файловой системы базируется на принципе формальной проверки.
Команда исследователей из Массачусетского технологического института представила первую файловую систему, способную восстановить все данные в случае аварийного завершения работы компьютера, сообщается на официальном портале учебного заведения. Свою разработку специалисты намерены продемонстрировать на Симпозиуме по Принципам Операционных систем (ACM Symposium on Operating Systems Principles), который пройдет в октябре этого года.
Основной задачей файловой системы является запись данных на накопитель, а также последующее отслеживание местонахождения этих данных. Если в процессе записи информации компьютер даст непредвиденный сбой, файловая система также может повредиться. В результате могут быть потеряны данные, для которых еще не создана резервная копия. Кроме того, некоторые программы могут перестать корректно работать.
По словам специалистов, несмотря на то, что разработанная ими файловая система является более медленной, чем современные аналоги, она «математически гарантирует», что данные не исчезнут даже в случае непредвиденных сбоев в работе ОС.
Надежность файловой системы базируется на так называемом принципе формальной проверки, предполагающей математическое описание допустимых границ операции для компьютерной программы и гарантирующей, что программа никогда не выйдет за эти границы. Это довольно сложный процесс, применяющийся только к высокоуровневым схематическим представлениям функциональности программы. Отличием разработки инженеров MIT является проверка свойств конечного кода файловой системы, а не высокоуровневой схемы. Для этой цели используется инструмент типа proof assistant под названием Coq (CoC, calculus of constructions), применяющийся для верификации программ.
По словам экспертов, техника, используемая ими, может применяться для создания более эффективных и надежных файловых систем.
Команда исследователей из Массачусетского технологического института представила первую файловую систему, способную восстановить все данные в случае аварийного завершения работы компьютера, сообщается на официальном портале учебного заведения. Свою разработку специалисты намерены продемонстрировать на Симпозиуме по Принципам Операционных систем (ACM Symposium on Operating Systems Principles), который пройдет в октябре этого года.
Основной задачей файловой системы является запись данных на накопитель, а также последующее отслеживание местонахождения этих данных. Если в процессе записи информации компьютер даст непредвиденный сбой, файловая система также может повредиться. В результате могут быть потеряны данные, для которых еще не создана резервная копия. Кроме того, некоторые программы могут перестать корректно работать.
По словам специалистов, несмотря на то, что разработанная ими файловая система является более медленной, чем современные аналоги, она «математически гарантирует», что данные не исчезнут даже в случае непредвиденных сбоев в работе ОС.
Надежность файловой системы базируется на так называемом принципе формальной проверки, предполагающей математическое описание допустимых границ операции для компьютерной программы и гарантирующей, что программа никогда не выйдет за эти границы. Это довольно сложный процесс, применяющийся только к высокоуровневым схематическим представлениям функциональности программы. Отличием разработки инженеров MIT является проверка свойств конечного кода файловой системы, а не высокоуровневой схемы. Для этой цели используется инструмент типа proof assistant под названием Coq (CoC, calculus of constructions), применяющийся для верификации программ.
По словам экспертов, техника, используемая ими, может применяться для создания более эффективных и надежных файловых систем.
