Mining Assumptions for Software Components using Machine Learning
Software verification approaches aim to check a software component under analysis for all possible environments. In reality, however, components are expected to operate within a larger system and are required to satisfy their requirements only when their inputs are constrained by environment assumptions. In this paper, we propose EPIcuRus, an approach to automatically synthesize environment assumptions for a component under analysis (i.e., conditions on the component inputs under which the component is guaranteed to satisfy its requirements). EPIcuRus combines search-based testing, machine learning and model checking. The core of EPIcuRus is a decision tree algorithm that infers environment assumptions from a set of test results including test cases and their verdicts. The test cases are generated using search-based testing, and the assumptions inferred by decision trees are validated through model checking. In order to improve the efficiency and effectiveness of the assumption generation process, we propose a novel test case generation technique, namely Important Features Boundary Test (IFBT), that guides the test generation based on the feedback produced by machine learning. We evaluated EPIcuRus by assessing its effectiveness in computing assumptions on a set of study subjects that include 18 requirements of four industrial models. We show that, for each of the 18 requirements, EPIcuRus was able to compute an assumption to ensure the satisfaction of that requirement, and further, ≈78% of these assumptions were computed in one hour.
Thu 12 NovDisplayed time zone: (UTC) Coordinated Universal Time change
08:00 - 08:30 | |||
08:00 2mTalk | Flexeme: Untangling Commits Using Lexical Flows Research Papers Profir-Petru Pârțachi University College London, UK, Santanu Dash University of Surrey, UK, Miltiadis Allamanis Microsoft Research, UK, Earl T. Barr University College London, UK DOI Pre-print Media Attached File Attached | ||
08:03 1mTalk | FREPA: An Automated and Formal Approach to Requirement Modeling and Analysis in Aircraft Control Domain Industry Papers Jincao Feng East China Normal University, Weikai Miao East China Normal University, China, Hanyue Zheng East China Normal University, Yihao Huang East China Normal University, Jianwen Li East China Normal University, China, Zheng Wang Beijing Sunwise Information Technology, China, Ting Su East China Normal University, China, Bin Gu Beijing Institute of Control Engineering, China, Geguang Pu Shanghai Trusted Industrial Control Platform, China, Mengfei Yang China Academy of Space Technology, China, Jifeng He Shanghai Key Lab of Trustworthy Computing, China DOI | ||
08:05 1mTalk | Mining Assumptions for Software Components using Machine Learning Research Papers Khouloud Gaaloul University of Luxembourg, Luxembourg, Claudio Menghi University of Luxembourg, Luxembourg, Shiva Nejati University of Ottawa, Canada / University of Luxembourg, Luxembourg, Lionel Briand University of Ottawa, Canada / University of Luxembourg, Luxembourg, David Wolfe QRA, Canada DOI | ||
08:07 1mTalk | Mining Input Grammars from Dynamic Control Flow Research Papers DOI | ||
08:09 1mTalk | TypeWriter: Neural Type Prediction with Search-Based Validation Research Papers Michael Pradel University of Stuttgart, Germany, Georgios Gousios Facebook & Delft University of Technology, Jason Liu Facebook, USA, Satish Chandra Facebook, USA DOI Pre-print Media Attached | ||
08:11 19mTalk | Conversations on Analysis 3 Paper Presentations Khouloud Gaaloul University of Luxembourg, Luxembourg, Michael Pradel University of Stuttgart, Germany, Profir-Petru Pârțachi University College London, UK, Rahul Gopinath CISPA, Germany, M: Dan Hao Peking University, China | ||