Работите по важен документ, който трябва да предадете спешно след часове. Забравяте да натиснете "Запази", защото "ей сега ще приключите". Следва непредизвикана грешка, спиране на тока, сривове или син екран (BSOD) и целия ви неделен следобед е отишъл на кино, и се налага да започнете отначало. Случвало ви се е подобно нещо? Най-вероятно, както на мнозина от нас и вие сте си скубали косите след срив в системата и загубата на ценна информация и време. Това може да е само епизод от миналото, ако учени от Масачузетския технологичен институт (MIT) успеят да реализират свой проект за система, която даже и при срив успява да запази последното си състояние без изменение.Въпросните специалисти от MIT използват математически методи, за да верифицират данните, облягайки се на популярна техника, известна като формална верификация, като надеждността на системата се  базира именно на този метод. Формалната верификация представлява метод за потвърждаване или отричане на правотата на даден факт посредством математически методи.Един от авторите на иновативната файлова система - Николай Зелдович - обяснява, че успехът една система да бъде изградена така че да запазва данните, с които работи към момента на срива е много труден, тъй като проблемите могат да възникнат на толкова много места, че е почти невъзможно да се предвиди откъде може да се получи срива. Инженерът, който е решил да изгражда подобна система е нужно да вземе предвид всяка една инструкция, изпълняваща се във всеки даден момент върху твърдия диск на компютъра. "Ами, ако взема да се срина сега? Ами сега? Или сега?", обяснява една примерна ситуация, пред която би се изправил един специалист, заел се с една почти непосилна задача.Посредством формалната верификация, границите на операцията на дадена компютърна програма, които може да достига биват дефинирани ясно и бива подсигурено това, че тези граници няма никога да бъдат преминавани от програмата.

MIT ,

Тяхната система вече е била и изпробвана на практика, като засега тя се представя значително по-бавно от днешните файлове системи, но специалистите работят по нейния дизайн, така че да се представя значително по-добре за в бъдеще.Разработки, подобни на специалистите от MIT има и преди, но техният проект може да се окаже първият работещ такъв. Вместо да се обръщат към помощта на високо схематични репрезентации на функционалността на програмата, те са се заели с практическо изследване на приложението на формалната верификация, пренаписвайки няколко пъти файловата система, по която работят от началото. Освен това те са решили да използват и доказателствен асистент (proof assistant), който да осигури официален език, който да опише различните аспекти на системата и връзката между всеки от тях."Ние реализираме файловата система на същия език, на който пишем доказателствата, като тези доказателства биват проверявани в средата на реална файлова система, а не посредством някаква идеализация, представена бяла дъска, която няма официална връзка с кода", обясняват учените.Авторите на изследването ще представят своя проект през октомври по време на конференцията  ACM Symposium on Operating Systems Principles.