TY - JOUR
T1 - Combining Genetic Programming and Model Checking to Generate Environment Assumptions
AU - Gaaloul, Khouloud
AU - Menghi, Claudio
AU - Nejati, Shiva
AU - Briand, Lionel C.
AU - Parache, Yago Isasi
N1 - Publisher Copyright:
© 1976-2012 IEEE.
PY - 2022/9/1
Y1 - 2022/9/1
N2 - 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.
AB - 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.
KW - decision trees
KW - Environment assumptions
KW - genetic programming
KW - machine learning
KW - model checking
KW - search-based software testing
UR - http://www.scopus.com/inward/record.url?scp=85112623797&partnerID=8YFLogxK
U2 - 10.1109/TSE.2021.3101818
DO - 10.1109/TSE.2021.3101818
M3 - Article
AN - SCOPUS:85112623797
SN - 0098-5589
VL - 48
SP - 3664
EP - 3685
JO - IEEE Transactions on Software Engineering
JF - IEEE Transactions on Software Engineering
IS - 9
ER -