mCUTE: A Model-level Concolic Unit Testing Engine for UML State Machines
Thu 14 Nov 2019 15:10 - 15:20 at Hillcrest - Models and Logs Chair(s): Timo Kehrer
Model Driven Engineering (MDE) techniques raise the level of abstraction at which developers construct software. However, modern cyber-physical systems are becoming more prevalent and complex and hence software models that represent the structure and behavior of such systems still tend to be large and complex. These models may have numerous if not infinite possible behaviors, with complex communications between their components. Appropriate software testing techniques to generate test cases with high coverage rate to put these systems to test at the model-level (without the need to understand the underlying code generator or refer to the generated code) are therefore important. Concolic testing, a hybrid testing technique that benefits from both concrete and symbolic execution, gains a high execution coverage and is used extensively in the industry for program testing but not for software models. In this paper, we present a novel technique and its tool mCUTE1 , an open source 2 model-level concolic testing engine. We describe the implementation of our tool in the context of Papyrus-RT, an open source Model Driven Engineering (MDE) tool based on UML-RT, and report the results of validating our tool using a set of benchmark models.
Wed 13 Nov
10:00 - 10:40 Demonstration | TsmartGP: A Tool for Finding Memory Defects with Pointer Analysis Yuexing WangTsinghua University, Guang ChenTsinghua University, Min ZhouTsinghua University, Ming GuTsinghua University, Jiaguang SunTsinghua University | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | BuRRiTo: A Framework to Extract, Specify, Verify and Analyze Business Rules Pavan ChittimalliTCS Research, Kritika AnandTCS Research, Shrishti PradhanTCS Research, Sayandeep MitraTCS Research, Chandan PrakashTCS Research, Rohit ShereTCS Research, Ravindra NaikTCS Research, TRDDC, India | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | Lancer: Your Code Tell Me What You Need Shufan ZhouSchool of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University, Beijun ShenSchool of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University, Hao ZhongShanghai Jiao Tong University | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | TestCov: Robust Test-Suite Execution and Coverage Measurement Pre-print Media Attached File Attached | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | Prema: A Tool for Precise Requirements Editing, Modeling and Analysis Yihao HuangEast China Normal University, Jincao FengEast China Normal University, Hanyue ZhengEast China Normal University, Jiayi ZhuEast China Normal University, Shang WangEast China Normal University, Siyuan JiangEastern Michigan University, Weikai MiaoShanghai Key Lab for Trustworthy Computing, School of Computer Science and Software Engineering, East China Normal University, Geguang PuEast China Normal University&Shanghai Trusted Industrial Control Platform Co., Ltd | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | XRaSE: Towards Virtually Tangible Software using Augmented Reality Rohit MehraAccenture Labs, India, Vibhu Saujanya SharmaAccenture Labs, Vikrant KaulgudAccenture Labs, India, Sanjay PodderAccenture | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | MuSC: A Tool for Mutation Testing of Ethereum Smart Contract Zixin LiNanjing University, Haoran WuState Key Laboratory for Novel Software Technology, Nanjing University, Jiehui XuNanjing University, Xingya WangState Key Laboratory for Novel Software Technology, Nanjing University, Lingming ZhangThe University of Texas at Dallas, Zhenyu ChenNanjing University | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | VeriSmart 2.0: Swarm-Based Bug-Finding for Multi-Threaded Programs with Lazy-CSeq Bernd FischerStellenbosch University, Salvatore La TorreUniversità degli Studi di Salerno, Gennaro ParlatoUniversity of Molise | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | DeepMutation++: a Mutation Testing Framework for Deep Learning Systems Qiang HuKyushu University, Japan, Lei MaKyushu University, Xiaofei XieNanyang Technological University, Bing YuKyushu University, Japan, Yang LiuNanyang Technological University, Singapore, Jianjun ZhaoKyushu University | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts Mark MossbergTrail of Bits, Felipe ManzanoTrail of Bits, Eric HennenfentTrail of Bits, Alex GroceTrail of Bits, Gustavo GriecoTrail of Bits, Josselin FeistTrail of Bits, Trent BrunsonTrail of Bits, Artem DinaburgTrail of Bits Media Attached | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | ConVul: An Effective Tool for Detecting Concurrency Vulnerabilities Ruijie MengUniversity of Chinese Academy of Sciences, Biyun ZhuUniversity of Chinese Academy of Sciences, Hao YunUniversity of Chinese Academy of Sciences, Haicheng LiUniversity of Chinese Academy of Sciences, Yan CaiInstitute of Software, Chinese Academy of Sciences, Zijiang YangWestern Michigan University | |||||||||||||||||||||||||||||||||||||||||
10:00 - 10:40 Demonstration | mCUTE: A Model-level Concolic Unit Testing Engine for UML State Machines Reza AhmadiQueen's University, Karim JahedQueen's University, Juergen DingelQueen's University, Kingston, Ontario |
Thu 14 Nov
13:40 - 15:20: Papers - Models and Logs at Hillcrest Chair(s): Timo KehrerHumboldt-Universtität zu Berlin | ||||||||||||||||||||||||||||||||||||||||||
13:40 - 14:00 Talk | Statistical Log Differencing Lingfeng BaoInstitute of Information Engineering, Chinese Academy of Sciences, Nimrod BusanyTel Aviv University, David LoSingapore Management University, Shahar MaozTel Aviv University Pre-print | |||||||||||||||||||||||||||||||||||||||||
14:00 - 14:20 Talk | Logzip: Extracting Hidden Structures via Iterative Clustering for Log Compression Jinyang LiuSun Yat-Sen University, Jieming ZhuHuawei Noah's Ark Lab, Shilin HeChinese University of Hong Kong, Pinjia HeETH Zurich, Zibin ZhengSun Yat-Sen University, Michael LyuThe Chinese University of Hong Kong | |||||||||||||||||||||||||||||||||||||||||
14:20 - 14:40 Talk | Code-First Model-Driven Engineering: On the Agile Adoption of MDE Tooling Artur BoronatUniversity of Leicester | |||||||||||||||||||||||||||||||||||||||||
14:40 - 15:00 Talk | Size and Accuracy in Model Inference Nimrod BusanyTel Aviv University, Shahar MaozTel Aviv University, Yehonatan YulazariTel Aviv University Pre-print | |||||||||||||||||||||||||||||||||||||||||
15:00 - 15:10 Demonstration | PMExec: An Execution Engine of Partial UML-RT Models Mojtaba BagherzadehQueen's University, Karim JahedQueen's University, Nafiseh KahaniQueen's University, Juergen DingelQueen's University, Kingston, Ontario Pre-print | |||||||||||||||||||||||||||||||||||||||||
15:10 - 15:20 Demonstration | mCUTE: A Model-level Concolic Unit Testing Engine for UML State Machines Reza AhmadiQueen's University, Karim JahedQueen's University, Juergen DingelQueen's University, Kingston, Ontario |