Linux માટે, કર્નલની સાચી કામગીરીને ચકાસવા માટે એક પદ્ધતિની દરખાસ્ત કરવામાં આવી છે

Linux કર્નલ 5.20 (કદાચ શાખાને 6.0 ક્રમાંકિત કરવામાં આવશે) માં સમાવેશ કરવા માટે, RV (રનટાઇમ વેરિફિકેશન) મિકેનિઝમના અમલીકરણ સાથે પેચોનો સમૂહ પ્રસ્તાવિત કરવામાં આવ્યો છે, જે ઉચ્ચ વિશ્વસનીય સિસ્ટમો પર યોગ્ય કામગીરીને ચકાસવા માટે સાધનો પૂરા પાડે છે જે ખાતરી આપે છે. નિષ્ફળતાઓની ગેરહાજરી. વેરિફિકેશન રનટાઈમ પર હેન્ડલર્સને ટ્રેસ પોઈન્ટ સાથે જોડીને કરવામાં આવે છે જે ઓટોમેટનના પૂર્વનિર્ધારિત સંદર્ભ નિર્ધારિત મોડેલ સામે અમલની વાસ્તવિક પ્રગતિ તપાસે છે જે સિસ્ટમની અપેક્ષિત વર્તણૂકને વ્યાખ્યાયિત કરે છે.

ટ્રેસ પોઈન્ટ્સની માહિતી મોડેલને એક રાજ્યમાંથી બીજા રાજ્યમાં લઈ જાય છે, અને જો નવી સ્થિતિ મોડેલના પરિમાણો સાથે મેળ ખાતી નથી, તો ચેતવણી જનરેટ કરવામાં આવે છે અથવા કર્નલને "ગભરાટ" સ્થિતિમાં મૂકવામાં આવે છે (ઉચ્ચ વિશ્વસનીયતા સિસ્ટમો શોધવાની અપેક્ષા રાખે છે. અને આવી પરિસ્થિતિઓનો જવાબ આપો). ઓટોમેટન મોડલ, જે એક રાજ્યથી બીજા રાજ્યમાં સંક્રમણોને વ્યાખ્યાયિત કરે છે, તેને "ડોટ" ફોર્મેટ (ગ્રાફવિઝ) માં નિકાસ કરવામાં આવે છે, જે પછી તેને ડોટ2સી ઉપયોગિતાનો ઉપયોગ કરીને C રજૂઆતમાં અનુવાદિત કરવામાં આવે છે, જે કર્નલ મોડ્યુલના સ્વરૂપમાં લોડ થાય છે. પૂર્વવ્યાખ્યાયિત મોડેલમાંથી અમલની પ્રગતિના વિચલનોને ટ્રેક કરે છે.

રન-ટાઇમ મૉડલ ચેકિંગ મિશન-ક્રિટિકલ સિસ્ટમ્સ પર યોગ્ય અમલને ચકાસવા માટે હળવા-વજન અને સરળ-થી-અમલીકરણ પદ્ધતિ તરીકે સ્થિત છે, શાસ્ત્રીય વિશ્વસનીયતા ચકાસણી પદ્ધતિઓ જેમ કે મોડલ ચકાસણી અને ઔપચારિકમાં આપેલ વિશિષ્ટતાઓ સાથે કોડના પાલનના ગાણિતિક પુરાવાને પૂરક બનાવે છે. ભાષા RV ના ફાયદાઓમાં એક મોડેલિંગ ભાષામાં સમગ્ર સિસ્ટમના અલગ અમલીકરણ વિના કડક ચકાસણી પ્રદાન કરવાની ક્ષમતા છે, તેમજ અણધાર્યા ઘટનાઓ માટે લવચીક પ્રતિભાવ, ઉદાહરણ તરીકે, જટિલ સિસ્ટમ્સમાં નિષ્ફળતાના વધુ પ્રસારને અવરોધિત કરવા માટે.

સોર્સ: opennet.ru