SpecChecker-ISA: A Data Sharing Analyzer for Interrupt-driven Embedded Software
Concurrency bugs are common in interrupt-driven programs, which are widely used in safety-critical areas. These bugs are often caused by incorrect data sharing among tasks and interrupts. Therefore, data sharing analysis is crucial to reasoning about the concurrency behaviour of interrupt-driven programs. Due to the variety of data access forms, existing tools suffer from both extensive false positives and false negatives while applying to interrupt-driven programs. This paper presents \textit{SpecChecker-ISA}, a tool that provides sound and precise data sharing analysis for interrupt-driven embedded software. The tool uses a memory access model parameterized by numerical invariants, which are computed by abstract interpretation based value analysis, to describe data accesses of various kinds, and then uses numerical meet operations to obtain the final result of data sharing. Our experiments on 4 real-world aerospace embedded software show that \textit{SpecChecker-ISA} can find all shared data accesses with few false positives, significantly outperforming other existing tools. \textit{SpecChecker-ISA} can effectively aid embedded software testers during code inspection and can also be utilized as a solid front-end of concurrency bug detection tools. The demo can be accessed at https://github.com/wangilson/SpecChecker-ISA.
Thu 21 JulDisplayed time zone: Seoul change
10:00 - 11:00 | |||
10:00 5mTalk | ATUA: an Update-driven App Testing Tool Tool Demonstrations Chanh-Duc Ngo University of Luxembourg, Fabrizio Pastore University of Luxembourg, Lionel Briand University of Luxembourg; University of Ottawa DOI | ||
10:05 5mTalk | Automatic Generation of Smoke Test Suites for Kubernetes Tool Demonstrations DOI | ||
10:10 5mTalk | ESBMC-CHERI: Towards Verification of C Programs for CHERI Platforms with ESBMC Tool Demonstrations Franz Brausse The University of Manchester, Fedor Shmarov The University of Manchester, Rafael Menezes University of Manchester, Mikhail R. Gadelha Igalia, Konstantin Korovin University of Manchester, Giles Reger University of Manchester, Lucas C. Cordeiro University of Manchester DOI | ||
10:16 5mTalk | ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation Tool Demonstrations Rafael Menezes University of Manchester, Rosiane de Freitas Federal University of Amazonas, Daniel Moura Federal University of Amazonas, Helena Cavalcante Federal University of Amazonas, Lucas C. Cordeiro University of Manchester DOI | ||
10:21 5mTalk | Faster Mutation Analysis with MeMu Tool Demonstrations DOI | ||
10:27 5mTalk | iFixDataloss: A Tool for Detecting and Fixing Data Loss Issues in Android Apps Tool Demonstrations Wunan Guo Fudan University, Zhen Dong Fudan University, China, Liwei Shen Fudan University, Wei Tian Fudan University, Ting Su East China Normal University, Xin Peng Fudan University DOI | ||
10:32 5mTalk | Maestro: A Platform for Benchmarking Automatic Program Repair Tools on Software Vulnerabilities Tool Demonstrations Eduard Costel Pinconschi Instituto Superior Técnico, University of Lisboa & INESC-ID, Quang-Cuong Bui Hamburg University of Technology, Rui Abreu Faculty of Engineering, University of Porto, Portugal, Pedro Adão IST-ULisboa and Instituto de Telecomunicações, Riccardo Scandariato Hamburg University of Technology DOI | ||
10:38 5mTalk | Pytest-Smell: A smell detection tool for Python unit tests Tool Demonstrations Alexandru Bodea Student at Babes Bolay University - Faculty of Mathematics and Computer Science DOI | ||
10:43 5mTalk | QMutPy: A Mutation Testing Tool for Quantum Algorithms & Applications in Qiskit Tool Demonstrations Daniel Fortunato INESC-ID, University of Porto, José Campos Faculty of Engineering of University of Porto & LASIGE, Portugal, Rui Abreu Faculty of Engineering, University of Porto, Portugal DOI | ||
10:49 5mTalk | SpecChecker-ISA: A Data Sharing Analyzer for Interrupt-driven Embedded Software Tool Demonstrations Boxiang Wang Xidian University and Beijing Sunwise Information Technology Ltd, Rui Chen Beijing Institute of Control Engineering, Chao Li Beijing Institute of Control Engineering and Beijing Sunwise Information Technology Ltd, Tingting Yu Beijing Institute of Control Engineering and Beijing Sunwise Information Technology Ltd, Dongdong Gao Beijing Institute of Control Engineering and Beijing Sunwise Information Technology Ltd, Mengfei Yang China Academy of Space Technology, China DOI | ||
10:54 5mTalk | UniRLTest: Universal Platform-Independent Testing with Reinforcement Learning via Image Understanding Tool Demonstrations Ziqian Zhang Nanjing University, Yulei Liu Nanjing University, Shengcheng Yu Nanjing University, Xin Li Nanjing University, Yexiao Yun Nanjing University, Chunrong Fang Nanjing University, Zhenyu Chen Nanjing University DOI | ||