کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
550562 872646 2014 18 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Formal verification of static software models in MDE: A systematic review
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر تعامل انسان و کامپیوتر
پیش نمایش صفحه اول مقاله
Formal verification of static software models in MDE: A systematic review
چکیده انگلیسی

ContextModel-driven Engineering (MDE) promotes the utilization of models as primary artifacts in all software engineering activities. Therefore, mechanisms to ensure model correctness become crucial, specially when applying MDE to the development of software, where software is the result of a chain of (semi)automatic model transformations that refine initial abstract models to lower level ones from which the final code is eventually generated. Clearly, in this context, an error in the model/s is propagated to the code endangering the soundness of the resulting software. Formal verification of software models is a promising approach that advocates the employment of formal methods to achieve model correctness, and it has received a considerable amount of attention in the last few years.ObjectiveThe objective of this paper is to analyze the state of the art in the field of formal verification of models, restricting the analysis to those approaches applied over static software models complemented or not with constraints expressed in textual languages, typically the Object Constraint Language (OCL).MethodWe have conducted a Systematic Literature Review (SLR) of the published works in this field, describing their main characteristics.ResultsThe study is based on a set of 48 resources that have been grouped in 18 different approaches according to their affinity. For each of them we have analyzed, among other issues, the formalism used, the support given to OCL, the correctness properties addressed or the feedback yielded by the verification process.ConclusionsOne of the most important conclusions obtained is that current model verification approaches are strongly influenced by the support given to OCL. Another important finding is that in general, current verification tools present important flaws like the lack of integration into the model designer tool chain or the lack of efficiency when verifying large, real-life models.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Software Technology - Volume 56, Issue 8, August 2014, Pages 821–838
نویسندگان
, ,