Reference : Evaluating Model Testing and Model Checking for Finding Requirements Violations in Si...
Scientific congresses, symposiums and conference proceedings : Paper published in a book
Engineering, computing & technology : Computer science
Computational Sciences
http://hdl.handle.net/10993/39794
Evaluating Model Testing and Model Checking for Finding Requirements Violations in Simulink Models
English
Nejati, Shiva [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
gaaloul, Khouloud [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)]
Menghi, Claudio [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Briand, Lionel [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Foster, Stephen [QRA Corp Canada]
Wolfe, David [QRA Corp Canada]
2019
Proceedings of the 27th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE)
Yes
The 27th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE)
from 26-08-2019 to 30-08-2019
[en] Model Checking ; Simulink Models ; SMT Solver ; Searchbased Software Testing
[en] Matlab/Simulink is a development and simulation language that is
widely used by the Cyber-Physical System (CPS) industry to model
dynamical systems. There are two mainstream approaches to verify
CPS Simulink models: model testing that attempts to identify
failures in models by executing them for a number of sampled test
inputs, and model checking that attempts to exhaustively check the
correctness of models against some given formal properties. In this
paper, we present an industrial Simulink model benchmark, provide
a categorization of different model types in the benchmark, describe
the recurring logical patterns in the model requirements, and discuss
the results of applying model checking and model testing
approaches to identify requirements violations in the benchmarked
models. Based on the results, we discuss the strengths and weaknesses
of model testing and model checking. Our results further
suggest that model checking and model testing are complementary
and by combining them, we can significantly enhance the capabilities
of each of these approaches individually. We conclude by
providing guidelines as to how the two approaches can be best
applied together.
University of Luxembourg: High Performance Computing - ULHPC
Tune
Researchers
http://hdl.handle.net/10993/39794
10.1145/3338906.3340444
H2020 ; 694277 - TUNE - Testing the Untestable: Model Testing of Complex Software-Intensive Systems
FnR ; FNR12632261 > Mehrdad Sabetzadeh > EQUACS > Early QUality Assurance of Critical Systems > 01/01/2019 > 31/12/2021 > 2018

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
paper.pdfAuthor postprint1.09 MBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.