Proof in VDM: Case Studies

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

Not so many years ago, it would have been difficult to find more than a handful of examples of the use of formal methods in industry. Today however, the industrial application of formal methods is becoming increasingly common in a variety of application areas, particularly those with a safety, security or financially critical aspects. Furthermore, in situations where a particularly high level of assurance is required, formal proof is broadly accepted as being of value. Perhaps the major benefit of formalisation is that it enables formal symbolic manip­ ulation of elements of a design and hence can provide developers with a variety of analyses which facilitate the detection of faults. Proof is just one of these possible formal activities, others, such as test case generation and animation, have also been shown to be effective bug finders. Proof can be used for both validation and verifi­ cation. Validation of a specification can be achieved by proving formal statements conjectured about the required behaviours of the system. Verification of the cor­ rectness of successive designs can be achieved by proof of a prescribed set of proof obligations generated from the specifications.