Reference : Evaluating Model Testing and Model Checking for Finding Requirements Violations in Si...

	Document type :	Scientific congresses, symposiums and conference proceedings : Paper published in a book
	Discipline(s) :	Engineering, computing & technology : Computer science
	Focus Areas :	Computational Sciences
	To cite this reference:	http://hdl.handle.net/10993/39794

Title :	Evaluating Model Testing and Model Checking for Finding Requirements Violations in Simulink Models
Language :	English
Author, co-author :	Nejati, Shiva [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
	Gaaloul, Khouloud [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > >]
	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]
Publication date :	2019
Main document title :	Proceedings of the 27th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE)
Peer reviewed :	Yes
Event name :	The 27th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE)
Event date :	from 26-08-2019 to 30-08-2019
Keywords :	[en] Model Checking ; Simulink Models ; SMT Solver ; Searchbased Software Testing
Abstract :	[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.
Research centres :	University of Luxembourg: High Performance Computing - ULHPC
Name of the research project :	Tune
Target :	Researchers
Permalink :	http://hdl.handle.net/10993/39794
DOI :	10.1145/3338906.3340444
Framework Programme / European Project :	H2020 ; 694277 - TUNE - Testing the Untestable: Model Testing of Complex Software-Intensive Systems
FnR project :	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): File Commentary Version Size Access Open access paper.pdf Author postprint 1.09 MB View/Open

All documents in ORBi^lu are protected by a user license.

 

University of Luxembourg Library |  Feedback |  Legal notices Site Map