Automatic verification of uml state chart by bogor model checking tool Automatic formal verification of network and distributed systems
سال انتشار: 1394
نوع سند: مقاله کنفرانسی
زبان: انگلیسی
مشاهده: 576
فایل این مقاله در 6 صفحه با فرمت PDF قابل دریافت می باشد
- صدور گواهی نمایه سازی
- من نویسنده این مقاله هستم
استخراج به نرم افزارهای پژوهشی:
شناسه ملی سند علمی:
KBEI02_113
تاریخ نمایه سازی: 5 بهمن 1395
چکیده مقاله:
Validation and verification of software or system specifications are crucial in reducing costs and proper software development. Software specifications are usually represented bysemi-formal languages like UML. For verification of non-formal and semi-formal models, they should be first transformed into aformal language. The state chart is one of the well-known UML charts that describe the behavior of a system and used formodeling many systems such as resource managements andcommunications in networks or distributed systems. In this paper, we propose a method to automatically map a UML statechart to BIR language, which is designed for BOGOR model checking. The goal of the verification in this paper is to evaluatethe deadlock property of this chart. The proposed method is evaluated by four case studies of ATM and Fax machine statecharts and the model is verified regarding the existence of adeadlock. Results indicate that while the PAT verification tool cannot properly recognize deadlocks in a state chart, theproposed approach is capable of detecting such cases of a deadlock.
کلیدواژه ها:
نویسندگان
Behzad Soleimani Neysian
Department of Software Engineering Faculty of Computer & Electrical Engineering University of Kashan Kashan, Esfahan, Iran
Seyed Morteza Babamir
Department of Software Engineering Faculty of Computer & Electrical Engineering University of Kashan Kashan, Esfahan, Iran