اسلاید اول

طراحی فرآیند دستیابی به درک جزیی تر از خصوصیات داده شده است. 

پیاده سازی را می توان چزیی ترین درک از خصوصیات داده شده در نظر گرفت. 

• اعتبارسنجی فرآیند اطمینان از این است که درک (realization) خصوصیات داده شده را ارضا می کند. 
• اعتبارسنجی بیشتر در طراحی و پیاده سازی سیستم ها  مورد استفاده قرار می گیرد. 
• طراحی یک سیستم پیچیده در چندین سطح رخ می دهد. 
• پیاده سازی را می توان پایین سطح طراحی در نظر گرفت. 
• اعتبارسنجی سه روش اساسی دارد: درستی یابی(Verification)، ارزیابی (Evaluation)و تست(Testing)
• درستی یابی یک روش فرمال ریاضی برای اثبات این است که درک به دست آمده خصوصیات سیستم را ارضا می کند. 
• ارزیابی روشی برای پیدا کردن این است که یک سیستم چقدر خوب رفتار می کند. 
• تست روشی برای اثبات این است که درک سیستم خصوصیات داده شده را ارضا نمی کند. 
• تست، درستی یابی و ارزیابی معمولاً روش های مکمل یکدیگر هستند. 

تست فقط می تواند حضور باگ ها را نشان دهد. نه عدم حضور آن ها را.

روش های فرمال چیست؟

• تکنیک هایی برای تحلیل سیستم ها بر اساس ریاضیات است. 
• این بدین معنا نیست که کاربر باید ریاضیدان باشد!!!...
• بعضی از کارها به دلیل پیچیدگی های روش های فرمال به  روش غیرفرمال انجام می شوند. 

روش های فرمال:

تکنیک های بر پایه ریاضی برای تشریح مشخصات سیستم ها

• تأمین یک فریم ورک برای 
• تببین مشخصات سیستم ها
• توسعه سیستم ها
• درستی یابی صحت 
• پیاده سازی W.r.t. مشخصات
• معادل بودن پیاده سازی های مختلف
• استدلال بر مبنای منطق است
• متمایل به تحلیل و دستکاری ماشین
• در اصل، می تواند هر چیز درستی در سیستم را درستی یابی کند!
• با زمان، مهارت و صبر کافی

درستی یابی فرمال

درستی یابی فرمال به دنبال اثبات درست کارکردن سیستم با اثبات ریاضی است. 

یک رهیافت فرمال موارد زیر را تأمین می کند:

• یک مدل سیستم (زبان) برای توصیف سیستم
• یک مدل مشخصات (زبان) برای توصیف درستی نیازمندیها
• یک تکنیک تجزیه و تحلیل برای اثبات درستی اینکه سیستم مشخصات را ملاقات می کند. (دارا می باشد)

چرا فرمال متد به طور گسترده تر مورد استفاده قرار نمیگیرد؟

این روش ها سخت و گران هستند و استفاده گسترده آن ها مفید نیست. بنابراین تنها برای سیستم هایی که از لحاظ ایمنی حساس هستند مورد استفاده قرار می گیرند. 

و یک مشکل دیگر...

این روش ها نیاز دارند که خصوصیات چیزی را که قرار است ساخته شود پیش از شروع به ساخت بدانند. 

این زیاد واقع گرایانه نیست:

• ممکن است به صورت تکراری مشخص شود که چه چیز قرار است ساخته شود.
• نرم افزارها به صورت مداوم تغییر می کنند. 

روش های فرمال "سبک"

• کاربرد جزیی روش های فرمال
• تنها بخش هایی از سیستم مشخص شوند. 
• تأکید روی تحلیل بعضی از خصوصیات
• امنیت، عدالت، اختتام بن بست، به جای درستی یابی کامل سیستم
• اشکال زدایی به جای تضمین
• اتوماسیون

موفق ترین تکنیک سبک وزن : بررسی مدل

روش های درستی یابی:

• دو روش کلی برای درستی یابی وجود دارد: "روش استقرایی" و "بررسی مدل"
• در روش استقرایی، مسئله داده شده به عنوان اثبات یک تئوری در دستگاه اثبات ریاضیات فرموله می شوند. 
• در روش بررسی مدل، رفتار سیستم به صورت الگوریتمی برای جست و جوی جامع تمام حالت های دسترس پذیر بررسی می شود. 

سیستم های واکنشی

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

سیستم های واکنشی معمولاً ویژگی های زیر را دارند:

• همگامی
• موعد زمانی (Timeliness)
• نیازمندیهای با قابلیت اعتماد بالا

درستی یابی فرمال

• درستی یابی فرمال در جست و جوی یک اثبات ریاضی برای کارکرد صحیح سیستم است. یک رهیافت فرمال موارد زیر را تأمین می کند:
• یک مدل سیستم (زبان) برای تشریح سیستم
• یک مدل مشخصات (زیان) برای تشریح صحت نیازمندی ها
• یک تکنیک تحلیل برای درستی یابی اینکه سیستم مشخصات تعریف شده اش را ملاقات می کند. 

مدل های سیستم

• سیستم های گذار (اتوماتا)
• جبر فرآیندها  (Process Algebra) و توسعه های آن
• Communicating Sequential Processes (CSP)
• Calculus of Communicating Systems (CCS)
• Actors
• Petri Nets و توسعه های آن
• مدل های دیگری نیز اخیراً توسعه یافته اند.

مدل مشخصات

• Temporal Logics and their extensions
• Linear Temporal Logics (LTLs)
• Computational Tree Logics (CTLs)
• CTL*
• مدل های دیگری نیز اخیراً توسعه یافته اند.