—تستمر هذه المقالة في سلسلة من المنشورات حول تطوير والتحقق من برامج التحكم المعتمدة على نوع خاص من المواصفات المنطقية الزمنية الخطية (LTL). في السابق، تم اقتراح مواصفة LTL إعلانية لوصف سلوك البرنامج المحدد بشكل صارم، وتم تطوير طرق للتحقق منها وترجمتها: يتم استخدام مدقق النموذج nuXmv للتحقق، وتتم الترجمة إلى لغة البرمجة الأمرية ST لوحدات التحكم المنطقية القابلة للبرمجة (PLCs). عند التحقق من مواصفة LTL الإعلانية لسلوك البرنامج، قد يصبح من الضروري نمذجة سلوك بيئته. بشكل عام، من المهم ضمان إمكانية بناء أنظمة مغلقة تضم كل من برنامج التحكم وبيئته. في هذه الورقة، تم اقتراح مواصفة LTL لسلوك غير محدد محدود لمتغير بولياني لوصف سلوك البيئة في البرامج التحكم المنطقية. تسمح هذه المواصفة بتحديد سلوك إشارات التغذية الراجعة البوليانية وظروف العدالة لاستبعاد سيناريوهات السلوك غير الواقعية. تقدم المقالة نهجًا لتطوير والتحقق من البرامج التحكم المنطقية حيث يتم نمذجة سلوك بيئة البرنامج كقيود على سلوك إشارات دخوله، مما يتجنب الحاجة إلى نمذجة العمليات الداخلية للبيئة بشكل صريح. نتيجة لذلك، يوفر النموذج المغلق
Neyzov et al. (Mon,) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: