تبدیل خودکار نمودارهای حالت UML به سیستم‌های گذار برچسب‌دار

چکیده مقاله

چکیده: نمودارهای حالت در UML یک روش متداول و رایج برای بیان و توصیف رفتار سیستم¬ها است. اما این توصیف فاقد برخی از توانایی¬ها و قابلیت ها مانند وارسی خودکار ویژگی¬ها و درستی رفتار سیستم است. به این منظور لازم است است که این توصیف رفتار ها به یک توصیف رسمی تبدیل شود تا بتوان برخی از این ویژگی ها را به نمایش گذاشته و در برخی از موارد بتوان بعضی از آنها را حتی کنترل کرد. در مقاله پیش رو روشی را برای تبدیل توصیف نمودارهای حالت UML به سیستم¬های گذار حالت ارائه می دهیم که قابلیت و توانایی وارسی خودکار ویژگی¬ها و درستی توصیف را دارا می¬باشد. این تبدیل به عنوان روشی مؤثر برای تحلیل رفتار سیستم‌های پیچیده و چندوجهی مورد استفاده قرار می‌گیرد. توصیف هدف قابلیت وارسی خودکار را در محیط LTSA دارد.