ສໍາລັບ Linux, ກົນໄກໄດ້ຖືກສະເຫນີເພື່ອກວດສອບການເຮັດວຽກທີ່ຖືກຕ້ອງຂອງ kernel

ສໍາລັບການລວມຢູ່ໃນ Linux 5.20 kernel (ບາງທີສາຂາຈະເປັນເລກ 6.0), ຊຸດຂອງ patches ໄດ້ຖືກສະເຫນີດ້ວຍການຈັດຕັ້ງປະຕິບັດກົນໄກການ RV (Runtime Verification), ເຊິ່ງສະຫນອງເຄື່ອງມືສໍາລັບການກວດສອບການດໍາເນີນການທີ່ຖືກຕ້ອງໃນລະບົບທີ່ເຊື່ອຖືໄດ້ສູງທີ່ຮັບປະກັນ. ຂາດຄວາມລົ້ມເຫລວ. ການກວດສອບແມ່ນດໍາເນີນການໃນເວລາແລ່ນໂດຍການຕິດຕົວຈັດການກັບຈຸດຕິດຕາມທີ່ກວດເບິ່ງຄວາມຄືບຫນ້າຕົວຈິງຂອງການປະຕິບັດຕໍ່ກັບຮູບແບບການອ້າງອີງທີ່ກໍານົດໄວ້ລ່ວງຫນ້າຂອງ automaton ທີ່ກໍານົດພຶດຕິກໍາທີ່ຄາດໄວ້ຂອງລະບົບ.

ຂໍ້ມູນຈາກຈຸດຕິດຕາມຈະຍ້າຍຕົວແບບຈາກລັດໜຶ່ງໄປຫາອີກລັດໜຶ່ງ, ແລະຖ້າສະຖານະໃໝ່ບໍ່ກົງກັບພາລາມິເຕີຂອງຕົວແບບ, ມີການເຕືອນໄພ ຫຼື ແກ່ນສານຖືກວາງໄວ້ໃນສະຖານະ "ຄວາມຢ້ານ" (ລະບົບຄວາມໜ້າເຊື່ອຖືສູງຄາດວ່າຈະກວດພົບ. ແລະຕອບສະຫນອງຕໍ່ສະຖານະການດັ່ງກ່າວ). ຮູບແບບ automaton, ເຊິ່ງກໍານົດການຫັນປ່ຽນຈາກລັດຫນຶ່ງໄປຫາອີກລັດຫນຶ່ງ, ຖືກສົ່ງອອກໄປສູ່ຮູບແບບ "dot" (graphviz), ຫຼັງຈາກນັ້ນມັນຖືກແປໂດຍໃຊ້ dot2c utility ເຂົ້າໄປໃນການສະແດງ C, ເຊິ່ງຖືກໂຫລດໃນຮູບແບບຂອງໂມດູນເມັດທີ່. ຕິດຕາມຄວາມບ່ຽງເບນໃນຄວາມຄືບໜ້າຂອງການປະຕິບັດຈາກຮູບແບບທີ່ກຳນົດໄວ້ລ່ວງໜ້າ.

ການກວດສອບແບບຈໍາລອງເວລາແລ່ນແມ່ນຈັດເປັນວິທີການທີ່ມີນ້ໍາຫນັກເບົາ ແລະງ່າຍຕໍ່ການປະຕິບັດໃນການກວດສອບການປະຕິບັດທີ່ຖືກຕ້ອງໃນລະບົບພາລະກິດທີ່ສໍາຄັນ, ປະກອບວິທີການກວດສອບຄວາມຫນ້າເຊື່ອຖືແບບຄລາສສິກ ເຊັ່ນ: ການກວດສອບແບບຈໍາລອງ ແລະຫຼັກຖານທາງຄະນິດສາດຂອງການປະຕິບັດຕາມລະຫັດທີ່ລະບຸໄວ້ຢ່າງເປັນທາງການ. ພາສາ. ໃນບັນດາຂໍ້ດີຂອງ RV ແມ່ນຄວາມສາມາດໃນການສະຫນອງການກວດສອບຢ່າງເຂັ້ມງວດໂດຍບໍ່ມີການປະຕິບັດແຍກຕ່າງຫາກຂອງລະບົບທັງຫມົດໃນພາສາແບບຈໍາລອງ, ເຊັ່ນດຽວກັນກັບການຕອບສະຫນອງທີ່ມີຄວາມຍືດຫຍຸ່ນຕໍ່ເຫດການທີ່ບໍ່ໄດ້ຄາດໄວ້, ສໍາລັບຕົວຢ່າງ, ສະກັດກັ້ນການຂະຫຍາຍພັນຂອງຄວາມລົ້ມເຫຼວໃນລະບົບທີ່ສໍາຄັນ.

ແຫຼ່ງຂໍ້ມູນ: opennet.ru