Reference : Combining Genetic Programming and Model Checking to Generate Environment Assumptions
Scientific journals : Article
Engineering, computing & technology : Computer science
Security, Reliability and Trust
http://hdl.handle.net/10993/47740
Combining Genetic Programming and Model Checking to Generate Environment Assumptions
English
Gaaloul, Khouloud [University of Luxembourg > Faculty of Science, Technology and Medecine (FSTM) > >]
Menghi, Claudio [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV >]
Nejati, Shiva [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV >]
Briand, Lionel [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV >]
Isasi Parache, Yago [LuxSpace]
Sep-2022
IEEE Transactions on Software Engineering
Institute of Electrical and Electronics Engineers
Yes
0098-5589
1939-3520
New-York
NY
[en] Environment assumptions ; Model checking ; Machine learning ; Decision trees ; Genetic programming ; Search-based software testing
[en] Software verification may yield spurious failures when environment assumptions are not accounted for. Environment assumptions are the expectations that a system or a component makes about its operational environment and are often specified in terms of conditions over the inputs of that system or component. In this article, we propose an approach to automatically infer environment assumptions for Cyber-Physical Systems (CPS). Our approach improves the state-of-the-art in three different ways: First, we learn assumptions for complex CPS models involving signal and numeric variables; second, the learned assumptions include arithmetic expressions defined over multiple variables; third, we identify the trade-off between soundness and coverage of environment assumptions and demonstrate the flexibility of our approach in prioritizing either of these criteria.

We evaluate our approach using a public domain benchmark of CPS models from Lockheed Martin and a component of a satellite control system from LuxSpace, a satellite system provider. The results show that our approach outperforms state-of-the-art techniques on learning assumptions for CPS models, and further, when applied to our industrial CPS model, our approach is able to learn assumptions that are sufficiently close to the assumptions manually developed by engineers to be of practical value.
NSERC of Canada under the Discovery and CRC programs
http://hdl.handle.net/10993/47740
10.1109/TSE.2021.3101818
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
TSEEpicurus.pdfAuthor preprint774.74 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.