Automatic verification of uml state chart by bogor model checking tool Automatic formal verification of network and distributed systems

سال انتشار: 1394
محل انتشار: دومین کنفرانس بین المللی مهندسی دانش بنیان و نوآوری
کد COI اختصاصی: KBEI02_113
زبان مقاله: انگلیسی
تعداد مشاهده: 492

نویسندگان

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

چکیده

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.

کلیدواژه ها

Automation Model Checking; UML State Machine; BOGOR; PAT; Dead Lock

مقالات مرتبط جدید

اطلاعات بیشتر در مورد COI

COI مخفف عبارت CIVILICA Object Identifier به معنی شناسه سیویلیکا برای اسناد است. COI کدی است که مطابق محل انتشار، به مقالات کنفرانسها و ژورنالهای داخل کشور به هنگام نمایه سازی بر روی پایگاه استنادی سیویلیکا اختصاص می یابد.

کد COI به مفهوم کد ملی اسناد نمایه شده در سیویلیکا است و کدی یکتا و ثابت است و به همین دلیل همواره قابلیت استناد و پیگیری دارد.