Formal Methods and Object Technology

منظور مهندسی نرم افزار توسعه نرم افزار با استفاده از رویکردهایی است که امکان توسعه مجموعه برنامه های بزرگ و پیچیده را به روشی سیستماتیک فراهم می کند. با این حال، به خوبی شناخته شده است که به دست آوردن سطح اطمینان از صحت مورد نیاز برای نرم افزارهای حیاتی ایمنی با استفاده از تکنیک های قدیمی برنامه ming دشوار است. سطح ایمنی مورد نیاز به ویژه در نرم افزارهایی که قرار است برای مدت طولانی بدون وقفه کار کنند، بالا می رود، زیرا نرم افزار قابل راه اندازی مجدد نیست و ممکن است خطاها جمع شوند. در نتیجه برنامه‌نویسی برای سیستم‌های حیاتی مأموریت، برای مثال، نیاز به رسیدگی به الزامات صحت با دقت خاصی دارد. در جستجوی تکنیک‌هایی برای ارزان‌تر کردن و مطمئن‌تر کردن نرم‌افزار، دو تأثیر مهم اما تا حد زیادی مستقل در سال‌های اخیر قابل مشاهده است. اینها عبارتند از: • فناوری شیء • روشهای رسمی اولاً، آشکار شده است که اشیا یک مفهوم مهم در نرم افزار هستند و باقی خواهند ماند. زبان‌های تجربی دهه 1970 مفاهیم مختلفی از بسته، خوشه، ماژول و غیره را معرفی کردند که به اهمیت مدولار بودن و کپسوله‌سازی، ساخت مؤلفه‌های نرم‌افزاری که نمایش‌های حالت و مکانیسم‌های الگوریتمی خود را از کاربران پنهان می‌کردند، و فقط آن ویژگی‌ها را صادر می‌کردند، بیان دقیقی ارائه کردند. مکانیسم های فراخوانی رویه) که برای استفاده از اشیاء مورد نیاز بود. این به اجزای نرم‌افزار سطحی از انتزاع می‌دهد و نمای کاری که یک ماژول برای سیستم انجام می‌دهد از جزئیات نحوه انجام آن‌ها جدا می‌کند.

Rationale Software engineering aims to develop software by using approaches which en­ able large and complex program suites to be developed in a systematic way. However, it is well known that it is difficult to obtain the level of assurance of correctness required for safety critical software using old fashioned program­ ming techniques. The level of safety required becomes particularly high in software which is to function without a break for long periods of time, since the software cannot be restarted and errors can accumulate. Consequently programming for mission critical systems, for example, needs to address the requirements of correctness with particular care. In the search for techniques for making software cheaper and more reliable, two important but largely independent influences have been visible in recent years. These are: • Object Technology • Formal Methods First, it has become evident that objects are, and will remain an important concept in software. Experimental languages of the 1970's introduced various concepts of package, cluster, module, etc. giving concrete expression to the importance of modularity and encapsulation, the construction of software com­ ponents hiding their state representations and algorithmic mechanisms from users, exporting only those features (mainly the procedure calling mechanisms) which were needed in order to use the objects. This gives the software com­ ponents a level of abstraction, separating the view of what a module does for the system from the details of how it does them.