Application of formal verification and falsification to large-scale chemical plant automation systems

در این مقاله، ما برای بررسی سیستم های اتوماسیون اتوماتیک شیمیایی، از تأیید رسمی و جعلی بودن مشخصات منطقی زمانی استفاده می کنیم. ما نتایج جدیدی را به دست می آوریم که با استفاده از یک رویکرد به تازگی توسعه یافته برای رسیدگی به نیازهای غیرانسانی و دستیابی به ترکیبات به دست آمده است. علاوه بر این، ما مجموعه ای از آزمون هایی را ایجاد می کنیم که می توانند برای یک سیستم کنترل داده شده به صورت خودکار تولید شوند، که برخی از آنها همان شکل را در ادبیات موجود دارند و برخی از آنها ترکیبی از تغییر پذیری و قابل دستیابی است که ما از رویکرد جدید استفاده می کنیم. قبلا ذکر شده. در هر دو مورد، ما با انتزاعی از سیستم های اتوماسیون کار می کنیم تا درخواست مدل نمادین را برای مشکلات در مقیاس صنعتی مورد استفاده قرار دهیم. ما نتایج را با استفاده از مجموعه ای از مثال های کوچک نشان می دهیم و نتایج حاصل از یک مطالعه موردی صنعتی را نیز گزارش می کنیم. روش هایی که ما اعمال می کنیم در یک جفت ابزار نرم افزار منبع باز اجرا می شود، که ما به طور خلاصه آن را توصیف می کنیم.