توليد خودكار داده آزمون از ضابطه هاي رسمي جبري

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