سبک معماری نرمافزار یک اَبَرمدل جهت تعیین مجموعهای از اجزاء و ارتباطات بین آنها برای مشخص کردن معماری نرمافزاری بر مبنای آن سبک است. معماری نرمافزار نقش حیاتی در حوزه مهندسی نرمافزار دارد و توصیف و تحلیل رسمی میتواند کیفیت مدلهای طراحی شده را تضمین نماید. یکی از زبانهای رسمی که قابلیت توصیف سبکهای معماری را دارد زبان تبدیل گراف است. همچنین، وارسی مدل یک روش رسمی برای تحلیل خودکار مدلهای طراحی شده )برای مثال، با زبان تبدیل گراف( میباشد. جهت جلوگیری از وقوع مشکل انفجار فضای حالت در حین وارسی مدل، فضای حالت مدل باید بطور هوشمندانه پیمایش شود. برای این منظور، در این مقاله با توجه به مشابه بودن زیرساختها و قوانین قابل اجرا روی مدلها با اندازههای مختلف از یک سبک معماری )توصیف شده با زبان تبدیل گراف(، ابتدا مدل کوچکی از سیستم داده شده را با تولید کامل فضای حالت وارسی کرده و سپس با یک شبکه بیزی، وابستگی بین قوانین به کار رفته در فضای حالت پیمایش شده را یاد میگیریم. بعد از یادگیری، این شبکه بیزی را برای وارسی هوشمندانه مدل بزرگتر به کار میگیریم. برای ارزیابی کارایی روش ارائه شده، آن را در ابزار GROOVE پیاده سازی خواهیم کرد.
