کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
6862674 677013 2014 16 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
A property-based abstraction framework for SysML activity diagrams
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر هوش مصنوعی
پیش نمایش صفحه اول مقاله
A property-based abstraction framework for SysML activity diagrams
چکیده انگلیسی
SysML activity diagrams are OMG/INCOSE standards used for modeling, analyzing and specifying probabilistic systems. Since they are considered as a de facto systems' modeling language, it is of a major importance to verify these diagrams. Moreover, it is even more important to reduce the cost of their verification process. In this paper, we propose a probabilistic abstraction framework to efficiently verify SysML activity diagrams. It is based on reducing the diagram complexity with respect to a system requirement. For verification, we use our verification approach that relies on PRISM model checker. To ensure the correctness of our proposed approach, we prove its soundness. This is achieved by finding the adequate pre-order relation between the semantics of the abstract and the concrete diagrams. This relation is shown to preserve the satisfaction of systems requirements. To this end, a calculus to capture the underlying semantics of SysML activity diagrams is proposed. Finally, the effectiveness of our approach is demonstrated on two real systems.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Knowledge-Based Systems - Volume 56, January 2014, Pages 328-343
نویسندگان
, , ,