Якщо комп’ютер раптом дав збій у процесі запису інформації чи зникла електрика, файлова система дискового накопичувача також може пошкодитися. Це означає, що робочі та персональні файли можуть уже не відкритися, а програми можуть перестати коректно працювати. Вирішити цю проблему змогли дослідники з Массачусетського технологічного інституту (MІТ).
У ході жовтневої конференції ACM Symposium on Operating Systems Principles вони покажуть першу файлову систему FSCQ, яка математично гарантує, що дані не загубляться навіть у процесі непередбачених збоїв ОС. Хоча запропонована файлова система є повільнішою порівняно із сучасними аналогами, фахівці планують поліпшити її продуктивність у майбутньому.
Надійність нової системи заснована на так званій техніці формальній перевірці. Ця техніка передбачає математичний опис допустимих меж операції для комп’ютерної програми і гарантує, що програма ніколи не вийде за ці межі. Це складний процес, тому він найчастіше застосовується тільки до найбільш високорівневих схем, що описують функціональність програми. Перетворення такої високорівневої моделі на робочий код призводить до цілого комплексу проблем.
Відмінністю розробки MІТ є те, що за допомогою спеціальної утиліти з ім’ям Coq комп’ютер може описати системні об’єкти і поведінкові зв’язки між ними в умовах форс-мажору. Це гарантує, що при збої комп’ютер не запише файл у непотрібне місце або забуде обнулити видалений. Проведені тести доводять, що файлова система FSCQ здатна коректно відновити дані в разі непередбачуваних ситуацій.
