Write a Blog >>
Thu 12 Nov 2020 08:05 - 08:06 at Virtual room 1 - Analysis 3

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 Nov
Times are displayed in time zone: (UTC) Coordinated Universal Time change

08:00 - 08:02
Talk
Flexeme: Untangling Commits Using Lexical Flows
Research Papers
Profir-Petru PârțachiUniversity College London, UK, Santanu Kumar DashUniversity of Surrey, UK, Miltiadis AllamanisMicrosoft Research, UK, Earl T. BarrUniversity College London, UK
DOI Pre-print Media Attached File Attached
08:03 - 08:04
Talk
FREPA: An Automated and Formal Approach to Requirement Modeling and Analysis in Aircraft Control Domain
Industry Papers
Jincao FengEast China Normal University, Weikai MiaoEast China Normal University, China, Hanyue ZhengEast China Normal University, Yihao HuangEast China Normal University, Jianwen LiEast China Normal University, China, Zheng WangBeijing Sunwise Information Technology, China, Ting SuEast China Normal University, China, Bin GuBeijing Institute of Control Engineering, China, Geguang PuShanghai Trusted Industrial Control Platform, China, Mengfei YangChina Academy of Space Technology, China, Jifeng HeShanghai Key Lab of Trustworthy Computing, China
DOI
08:05 - 08:06
Talk
Mining Assumptions for Software Components using Machine Learning
Research Papers
Khouloud GaaloulUniversity of Luxembourg, Luxembourg, Claudio MenghiUniversity of Luxembourg, Luxembourg, Shiva NejatiUniversity of Ottawa, Canada / University of Luxembourg, Luxembourg, Lionel BriandUniversity of Ottawa, Canada / University of Luxembourg, Luxembourg, David WolfeQRA, Canada
DOI
08:07 - 08:08
Talk
Mining Input Grammars from Dynamic Control Flow
Research Papers
Rahul GopinathCISPA, Germany, Björn MathisCISPA, Germany, Andreas ZellerCISPA, Germany
DOI
08:09 - 08:10
Talk
TypeWriter: Neural Type Prediction with Search-Based Validation
Research Papers
Michael PradelUniversity of Stuttgart, Germany, Georgios GousiosFacebook & Delft University of Technology, Jason LiuFacebook, USA, Satish ChandraFacebook, USA
DOI Pre-print Media Attached
08:11 - 08:30
Talk
Conversations on Analysis 3
Paper Presentations
Khouloud GaaloulUniversity of Luxembourg, Luxembourg, Michael PradelUniversity of Stuttgart, Germany, Profir-Petru PârțachiUniversity College London, UK, Rahul GopinathCISPA, Germany, M: Dan HaoPeking University, China