تولید خودکار داده‌آزمون از ضابطه¬های رسمی جبری

چکیده مقاله

روش‌های رسمی از روش‌هایی است که دارای استحکام و مبنای ریاضی متقن است و برای توصیف دقیق و کامل نرم‌افزار استفاده می‌شود. با استفاده از یک روش رسمی، می‌توان یک سیستم را به صورت انتزاعی تولید کرد و به اهداف رویکرد آزمون جعبه سیاه کمک کرد تا بتوان مجموعه‌ نمونه‌های آزمون را از یک توصیف انتزاعی تولید کرد. تا کنون زبان‌های توصیفی جبری در توصیفات رسمی نوع داده انتزاعی و مولفه‌های نرم‌افزار موفق بوده‌اند و چندین روش وجود دارد که نمونه‌های آزمون را به صورت خودکار ایجاد می‌کند و توصیفات جبری مولفه‌های نرم‌افزار را با پیاده‌سازی آن مطابقت می‌دهد، ولی روش‌های موجود پوشش اصول شرطی و شرایط تو در تو در اصول پیچیده را تضمین نمی‌کند. در این مقاله ما یک روش به همراه نرم‌افزاری شرح می‌دهیم که نمونه‌های آزمون از توصیفات کران‌دار جبری نوع داده‌های انتزاعی را به صورت خودکار تولید می‌کند و پوشش اصول را تضمین می‌کند. ابتدا توصیفات جبری به زبان مدل‌سازی Alloy ترجمه می‌شود سپس آنالیزکننده Alloy نمونه‌های مدل را از داده آزمون‌هایی که Junit تولید کرده‌ است، پیدا می‌کند.