Для Linux ΠΏΡ€Π΅Π΄Π»ΠΎΠΆΠ΅Π½ ΠΌΠ΅Ρ…Π°Π½ΠΈΠ·ΠΌ Π²Π΅Ρ€ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΠΈ коррСктности Ρ€Π°Π±ΠΎΡ‚Ρ‹ ядра

Для Π²ΠΊΠ»ΡŽΡ‡Π΅Π½ΠΈΡ Π² состав ядра Linux 5.20 (Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎ, Π²Π΅Ρ‚ΠΊΠ° ΠΏΠΎΠ»ΡƒΡ‡ΠΈΡ‚ Π½ΠΎΠΌΠ΅Ρ€ 6.0) ΠΏΡ€Π΅Π΄Π»ΠΎΠΆΠ΅Π½ Π½Π°Π±ΠΎΡ€ ΠΏΠ°Ρ‚Ρ‡Π΅ΠΉ с Ρ€Π΅Π°Π»ΠΈΠ·Π°Ρ†ΠΈΠ΅ΠΉ ΠΌΠ΅Ρ…Π°Π½ΠΈΠ·ΠΌΠ° RV (Runtime Verification), ΠΏΡ€Π΅Π΄ΡΡ‚Π°Π²Π»ΡΡŽΡ‰Π΅Π³ΠΎ срСдства для ΠΏΡ€ΠΎΠ²Π΅Ρ€ΠΊΠΈ коррСктности Ρ€Π°Π±ΠΎΡ‚Ρ‹ Π½Π° высоконадСТных систСмах, Π³Π°Ρ€Π°Π½Ρ‚ΠΈΡ€ΡƒΡŽΡ‰ΠΈΡ… отсутствиС сбоСв. ΠŸΡ€ΠΎΠ²Π΅Ρ€ΠΊΠ° производится Π²ΠΎ врСмя выполнСния Ρ‡Π΅Ρ€Π΅Π· ΠΏΡ€ΠΈΠΊΡ€Π΅ΠΏΠ»Π΅Π½ΠΈΠ΅ ΠΎΠ±Ρ€Π°Π±ΠΎΡ‚Ρ‡ΠΈΠΊΠΎΠ² ΠΊ Ρ‚ΠΎΡ‡ΠΊΠ°ΠΌ трассировки, ΡΠ²Π΅Ρ€ΡΡŽΡ‰ΠΈΡ… фактичСский Ρ…ΠΎΠ΄ выполнСния с Π·Π°Ρ€Π°Π½Π΅Π΅ ΠΎΠΏΡ€Π΅Π΄Π΅Π»Ρ‘Π½Π½ΠΎΠΉ эталонной Π΄Π΅Ρ‚Π΅Ρ€ΠΌΠΈΠ½ΠΈΡ€ΠΎΠ²Π°Π½Π½ΠΎΠΉ модСлью Π°Π²Ρ‚ΠΎΠΌΠ°Ρ‚Π°, ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΡΡŽΡ‰Π΅Π³ΠΎ ΠΎΠΆΠΈΠ΄Π°Π΅ΠΌΠΎΠ΅ ΠΏΠΎΠ²Π΅Π΄Π΅Π½ΠΈΠ΅ систСмы.

Π˜Π½Ρ„ΠΎΡ€ΠΌΠ°Ρ†ΠΈΡ ΠΎΡ‚ Ρ‚ΠΎΡ‡Π΅ΠΊ трассировки ΠΏΠ΅Ρ€Π΅Π²ΠΎΠ΄ΠΈΡ‚ модСль ΠΈΠ· ΠΎΠ΄Π½ΠΎΠ³ΠΎ состояния Π² Π΄Ρ€ΡƒΠ³ΠΎΠ΅, ΠΈ Ссли Π½ΠΎΠ²ΠΎΠ΅ состояниС Π½Π΅ соотвСтствуСт ΠΏΠ°Ρ€Π°ΠΌΠ΅Ρ‚Ρ€Π°ΠΌ ΠΌΠΎΠ΄Π΅Π»ΠΈ, гСнСрируСтся ΠΏΡ€Π΅Π΄ΡƒΠΏΡ€Π΅ΠΆΠ΄Π΅Π½ΠΈΠ΅ ΠΈΠ»ΠΈ ядро пСрСводится Π² состояниС «panic» (подразумСваСтся, Ρ‡Ρ‚ΠΎ высоконадёТныС систСмы Π±ΡƒΠ΄ΡƒΡ‚ ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΡΡ‚ΡŒ ΠΏΠΎΠ΄ΠΎΠ±Π½Ρ‹Π΅ ситуации ΠΈ Ρ€Π΅Π°Π³ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ Π½Π° Π½ΠΈΡ…). МодСль Π°Π²Ρ‚ΠΎΠΌΠ°Ρ‚Π°, ΠΎΠΏΡ€Π΅Π΄Π΅Π»ΡΡŽΡ‰Π°Ρ ΠΏΠ΅Ρ€Π΅Ρ…ΠΎΠ΄Ρ‹ ΠΈΠ· ΠΎΠ΄Π½ΠΎΠ³ΠΎ состояния Π² Π΄Ρ€ΡƒΠ³ΠΎΠ΅, экспортируСтся Π² Ρ„ΠΎΡ€ΠΌΠ°Ρ‚ «dot» (graphviz), послС Ρ‡Π΅Π³ΠΎ транслируСтся ΠΏΡ€ΠΈ ΠΏΠΎΠΌΠΎΡ‰ΠΈ ΡƒΡ‚ΠΈΠ»ΠΈΡ‚Ρ‹ dot2c Π² прСдставлСниС Π½Π° языкС Π‘ΠΈ, ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠ΅ загруТаСтся Π² Ρ„ΠΎΡ€ΠΌΠ΅ модуля ядра, ΠΎΡ‚ΡΠ»Π΅ΠΆΠΈΠ²Π°ΡŽΡ‰Π΅Π³ΠΎ отклонСния Ρ…ΠΎΠ΄Π° выполнСния ΠΎΡ‚ ΠΏΡ€Π΅Π΄ΠΎΠΏΡ€Π΅Π΄Π΅Π»Ρ‘Π½Π½ΠΎΠΉ ΠΌΠΎΠ΄Π΅Π»ΠΈ.

Для Linux ΠΏΡ€Π΅Π΄Π»ΠΎΠΆΠ΅Π½ ΠΌΠ΅Ρ…Π°Π½ΠΈΠ·ΠΌ Π²Π΅Ρ€ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΠΈ коррСктности Ρ€Π°Π±ΠΎΡ‚Ρ‹ ядра

Π‘Π²Π΅Ρ€ΠΊΠ° с модСлью Π²ΠΎ врСмя выполнСния позиционируСтся ΠΊΠ°ΠΊ Π±ΠΎΠ»Π΅Π΅ лСгковСсный ΠΈ простой для Ρ€Π΅Π°Π»ΠΈΠ·Π°Ρ†ΠΈΠΈ Π½Π° ΠΏΡ€Π°ΠΊΡ‚ΠΈΠΊΠ΅ способ подтвСрТдСния коррСктности выполнСния Π½Π° критичСски Π²Π°ΠΆΠ½Ρ‹Ρ… систСмах, Π΄ΠΎΠΏΠΎΠ»Π½ΡΡŽΡ‰ΠΈΠΉ классичСскиС ΠΌΠ΅Ρ‚ΠΎΠ΄Ρ‹ подтвСрТдСния надёТности, Ρ‚Π°ΠΊΠΈΠ΅ ΠΊΠ°ΠΊ ΠΏΡ€ΠΎΠ²Π΅Ρ€ΠΊΠ° ΠΌΠΎΠ΄Π΅Π»ΠΈ ΠΈ матСматичСскиС Π΄ΠΎΠΊΠ°Π·Π°Ρ‚Π΅Π»ΡŒΡΡ‚Π²Π° соотвСтствия ΠΊΠΎΠ΄Π° спСцификациям, Π·Π°Π΄Π°Π½Π½Ρ‹ΠΌ Π½Π° Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΠΎΠΌ языкС. Из достоинств RV называСтся Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎΡΡ‚ΡŒ ΠΎΠ±Π΅ΡΠΏΠ΅Ρ‡ΠΈΡ‚ΡŒ ΡΡ‚Ρ€ΠΎΠ³ΡƒΡŽ Π²Π΅Ρ€ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΡŽ Π±Π΅Π· ΠΎΡ‚Π΄Π΅Π»ΡŒΠ½ΠΎΠΉ Ρ€Π΅Π°Π»ΠΈΠ·Π°Ρ†ΠΈΠΈ всСй систСмы Π½Π° языкС модСлирования, Π° Ρ‚Π°ΠΊΠΆΠ΅ Π³ΠΈΠ±ΠΊΠΎΠ΅ Ρ€Π΅Π°Π³ΠΈΡ€ΠΎΠ²Π°Π½ΠΈΠ΅ Π½Π° Π½Π΅ΠΏΡ€Π΅Π΄Π²ΠΈΠ΄Π΅Π½Π½Ρ‹Π΅ события, Π½Π°ΠΏΡ€ΠΈΠΌΠ΅Ρ€, для блокирования дальнСйшСго распространСния сбоя Π² критичСски Π²Π°ΠΆΠ½Ρ‹Ρ… систСмах.

Π˜ΡΡ‚ΠΎΡ‡Π½ΠΈΠΊ: opennet.ru

Π”ΠΎΠ±Π°Π²ΠΈΡ‚ΡŒ ΠΊΠΎΠΌΠΌΠ΅Π½Ρ‚Π°Ρ€ΠΈΠΉ