مقدمه مفهومی در علوم کامپیوتر، اصطلاح ’’رسمی’’ (Formal) به سیستم ها، روش ها و زبان هایی اشاره دارد که بر پایه اصول دقیق ریاضی و منطقی بنا شده اند. این مفهوم در مقابل روش های غیررسمی و شهودی قرار می گیرد. روش های رسمی امکان استدلال دقیق، اثبات درستی و تحلیل سیستم های پیچیده را فراهم می کنند. از کاربردهای مهم این مفهوم می توان به زبان های رسمی، روش های رسمی در مهندسی نرم افزار و سیستم های مبتنی بر منطق اشاره کرد. تاریخچه و تکامل ریشه های مفهوم رسمیت به کارهای منطق دانانی مانند جورج بول و گوتلوب فرگه در قرن نوزدهم بازمی گردد. در دهه 1930، آلن تورینگ و آلونزو چرچ مفاهیم محاسبه پذیری رسمی را توسعه دادند. از دهه 1960، روش های رسمی در طراحی زبان های برنامه نویسی و سیستم های نرم افزاری به کار گرفته شدند. امروزه این روش ها در توسعه سیستم های حیاتی و امنیتی نقش کلیدی ایفا می کنند. زمینه های کاربرد 1. زبان های رسمی و نظریه اتوماتا 2. روش های رسمی در مهندسی نرم افزار 3. سیستم های مبتنی بر منطق 4. اثبات قضایا و بررسی مدل 5. معناشناسی رسمی زبان های برنامه نویسی 6. تحلیل و طراحی الگوریتم ها 7. سیستم های امنیتی و رمزنگاری مزایای روش های رسمی - امکان استدلال دقیق درباره سیستم ها - کاهش خطاهای طراحی و پیاده سازی - افزایش قابلیت اطمینان سیستم ها - تسهیل فرآیند تأیید و اعتبارسنجی - پشتیبانی از تحلیل سیستم های پیچیده - ایجاد مستندات دقیق و بدون ابهام چالش ها و محدودیت ها - هزینه بالای یادگیری و پیاده سازی - نیاز به تخصص پیشرفته ریاضی - زمان بر بودن فرآیندهای رسمی - مقیاس پذیری در پروژه های بزرگ - مقاومت فرهنگی در برابر تغییر روش ها - محدودیت های ابزارهای موجود ابزارها و زبان های رسمی - زبان های مشخصه نویسی مانند Z و VDM - ابزارهای اثبات قضیه مانند Coq و Isabelle - چک کننده های مدل مانند SPIN و NuSMV - زبان های برنامه نویسی رسمی مانند Ada - فریم ورک های تحلیل استاتیک - سیستم های پردازش زبان های رسمی روندهای آینده - ادغام با روش های یادگیری ماشین - توسعه ابزارهای کاربرپسندتر - اتوماسیون فرآیندهای رسمی - کاربرد در سیستم های خودمختار - توسعه روش های ترکیبی رسمی-غیررسمی - بهبود مقیاس پذیری برای پروژه های بزرگ
