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

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