文章基本信息

标题：Model-Checking-based vs. SMT-based Consistency Analysis of Industrial Embedded Systems Requirements: Application and Experience
本地全文：下载
作者：Predrag Filipovikj ; Guillermo Rodriguez-Navas ; Cristina Seceleanu 等
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2018
卷号：75
DOI：10.14279/tuj.eceasst.75.1054
语种：English
出版社：European Association of Software Science and Technology (EASST)
摘要：Industry relies predominantly on manual peer-review techniques for assessing the correctness of system specifications. However, with the ever increasing size, complexity and intricacy of the specifications, it becomes difficult to assure their correctness with respect to certain criteria such as consistency. To cope with this challenge, a set of techniques based on formal methods, called extit{sanity checks} have been proposed to automatically assess the quality of system specifications in a systematic and rigorous manner. The predominant way of assessing the sanity of system specifications is by model checking, which in literature is reported to be expensive for analysis as it takes a long time for the procedure to terminate. Recently, another approach for checking the consistency of a system's specification using Satisfiability Modulo Theories has been proposed in order to reduce the analysis time. In this paper, we compare the two approaches for consistency analysis, by applying them on a relevant industrial use case, using the same definition for consistency and the same set of requirements. The comparison is carried out with respect to: i) time for generating the model and the latter's complexity, and ii) consistency analysis time. Contrary to the currently available data, our preliminary results show no significant difference in analysis time when applied on the same system specification under the same definition of consistency, but show significant difference in the time of creating the model for analysis.