بکارگیری بررسی مدل برای برنامه های PLC در اندازه و سطوح صنعتی
برای دریافت اصل مقاله شماره 4 را به 09903207833 تلگرام نمایید.
Abstract—Programmable Logic Controllers (PLCs) are embedded
computers widely used in industrial control systems.
Ensuring that a PLC software complies with its specification is a
challenging task. Formal verification has become a recommended
practice to ensure the correctness of safety-critical software but
is still underused in industry due to the complexity of building
and managing formal models of real applications. In this paper,
we propose a general methodology to perform automated model
checking of complex properties expressed in temporal logics (e.g.,
CTL, LTL) on PLC programs. This methodology is based on
an Intermediate Model (IM), meant to transform PLC programs
written in various standard languages (ST, SFC, etc.) to different
modeling languages of verification tools. We present the syntax
and semantics of the IM and the transformation rules of the ST
and SFC languages to the nuXmv model checker passing through
the intermediate model. Finally, two real cases studies of CERN
PLC programs, written mainly in the ST language, are presented
to illustrate and validate the proposed approach.
چکیده
کنترلر های منطقی برنامه پذیر PLC ،ها کامپیوترهای نهفته و طراحی شده ای اند که در سیستم های کنترل صنعتی کاربرد های فراوانی دارند.اطمینان از اینکه یک نرم افزار PLC با ویژگی هایش تطابق داشته باشد ،امری چالش بر انگیز است.درستی یابی رسمی یکی از اقدامات توصیه شده برای اطمینان از صحت و درستی نرم افزار است اما هنوز به دلیل دشواری و پیچیدگی ساختار و مدل های رسمی مدیریت در موارد کاربردی واقعی در همه ی صنایع مورد استفاده قرار نمیگیرد.در این مقاله ما یک روش کلی برای اجرای بررسی مدل خودکار از ویژگی های پیچیده ی مطرح شده در CTL و LTL بر برنامه های PLC را مطرح میکنیم.این روش مبتنی است بر مدل واسطه ای و میانجی IM ،برای تبدیل برنامه های PLC نوشته شده به زبان های استاندارد مختلف ST و SFC و به زبان های مدل سازی مختلف از ابزار های درستی یابی و وارسی.در این تحقیق ما ترکیب لغوی و معنایی IM و قوانین تبدیل زبان های ST و SFC را به بازبینی کننده ی مدل nuXmv از طریق مدل واسطه ای و میانجی را بیان نموده ایم.نهایتا دو مطالعه ی موردی حقیقی از برنامه های CERN PLC نوشته شده به زبان ST ،برای بیان و تایید رویکرد مطرح شده انجام و ارائه شده است.
