کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
434942 1441655 2015 20 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Safety assessment of AltaRica models via symbolic model checking
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Safety assessment of AltaRica models via symbolic model checking
چکیده انگلیسی

AltaRica is a language used to describe safety critical systems that has become a de-facto European industrial standard for Model-Based Safety Assessment (MBSA). However, even the most mature tool for the support for MBSA of AltaRica models, i.e. Dassault's OCAS, has several limitations. The most important ones are its inability to perform many analyses exhaustively, severe scalability issues, and the lack of model checking techniques for temporal properties.In this paper we present a novel approach for the analysis of AltaRica models, based on a translation into an extended version of the model checker NuSMV. The translation relies on a novel formal characterization of the Dataflow dialect of AltaRica used in OCAS. The translation is formally defined, and its correctness is proved. Based on this formal characterization, a toolset has been developed and integrated within OCAS, thus enabling functional verification and safety assessment with the state of the art techniques of NuSMV. The whole approach is validated by an experimental evaluation on a set of industrial case studies, which demonstrates the advantages of the proposed technique over the currently available tools.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 98, Part 4, 1 February 2015, Pages 464–483
نویسندگان
, , , , , , ,