سیده زهرا سجادی - کارشناس ارشد، دانشکده علوم و مهندسی کامپیوتر، دانشگاه شهید بهشتی، تهران
حسن حقیقی - استادیار، دانشکده علوم و مهندسی کامپیوتر، دانشگاه شهید بهشتی، تهران

روش های صوری با ایده ی استفاده از ریاضیات در تولید نرم افزار، به عنوان گزینه ای برای تأمین قابلیت اطمینان نرم افزار مطرح شده اند؛ مهم ترین مزیت این روش ها فراهم نمودن امکان استدلال، اثبات و کاهش هزینه ی کلی تولید نرم افزار، به ویژه هزینه ی درستی یابی و نگهداری آن است. امروزه با افزایش پیچیدگی طراحی پایگاه داده ها و افزایش احتمال بروز خطا در آنها، به کارگیری روش های صوری در توصیف، طراحی و درستی یابی اینگونه سیستم ها، با هدف جلوگیری از خطاها و حفظ محدودیت های جامعیتی پیشنهاد می شود. در اغلب کارهای انجام شده در این زمینه، مدل سازی داده ها توسط روش های متداول که فاقد معنای تعریف شده دقیق و صوری هستند، انجام شده است. از آنجایی که کنترل سازگاری، بدون ابهام بودن و کامل بودن طراحی از طریق این روش ها مشکل است، لازم است که در یک مرحله دیگر، طراحی انجام شده توسط یک زبان صوری توصیف شود؛ این موضوع موجب تأخیر در درستی یابی و اعتبارسنجی مدل داده ای می شود؛ همچنین خطاهای کشف شده باید با مراجعه مجدد به مدلسازی اولیه رفع شوند. برای جلوگیری از اتلاف زمان، هزینه و همچنین به منظور انجام هر چه سریع تر درستی یابی صوری پایگاه داده ها، این مقاله به ارائه روش جدیدی برای مدلسازی داده و توصیف تراکنش ها توسط زبان توصیف صوری Object-Z می پردازد. همچنین راهکاری جهت کنترل سازگاری و درستی یابی مدلسازی انجام شده توسط ابزارگان Z پیشنهاد می شود.

مدلسازی داده، پایگاه داده، درستی یابی، توصیف صوری، زبان صوری Object-Z، تراکنش