Precisely modeling complex systems like cyber-physical systems is challenging, which often render model-based system verification techniques like model checking infeasible. To overcome this challenge, we propose a method called LAR to automatically ‘verify’ such complex systems through a combination of learning, abstraction and refinement from a set of system log traces. We assume that log traces and sampling frequency are adequate to capture ‘enough’ behaviour of the system. Given a safety property and the concrete system log traces as input, LAR automatically learns and refines system models, and produces two kinds of outputs. One is a counterexample with a bounded probability of being spurious. The other is a probabilistic model based on which the given property is ‘verified’. The model can be viewed as a proof obligation, i.e., the property is verified if the model is correct. It can also be used for subsequent system analysis activities like runtime monitoring or model-based testing. Our method has been implemented as a self-contained software toolkit. The evaluation on multiple benchmark systems as well as a real-world water treatment system shows promising results.

Link to Publication: https://ieeexplore.ieee.org/abstract/document/8576657

Jingyi Wang

National University of Singapore, Singapore

Singapore

Jun Sun

Singapore Management University, Singapore

Singapore

Shengchao Qin

University of Teesside

United Kingdom

Cyrille Jegourel

ISTD, Singapore University of Technology and Design

Context Specification mining techniques are typically used to extract the specification of a software in the absence of (up-to-date) specification documents. This is useful for program comprehension, testing, and anomaly detection. However, specification mining can also potentially be used for debugging, where a faulty behavior is abstracted to give developers a context about the bug and help them locating it.

Objective In this project, we investigate this idea in an industrial setting. We propose a very basic semi-automated specification mining approach for debugging and apply that on real reported issues from an AutoPilot software system from our industry partner, MicroPilot Inc. The objective is to assess the feasibility and usefulness of the approach in a real-world setting.

Method The approach is developed as a prototype tool, working on C code, which accept a set of relevant state fields and functions, per issue, and generates an extended finite state machine that represents the faulty behavior, abstracted with respect to the relevant context (the selected fields and functions).

Results We qualitatively evaluate the approach by a set of interviews (including observational studies) with the company’s developers on their real-world reported bugs. The results show that (a) our approach is feasible, (b) it can be automated to some extent, and (c) brings advantages over only using their code-level debugging tools. We also compared this approach with traditional fully automated state-merging algorithms and reported several issues when applying those techniques on a real-world debugging context.

Conclusion The main conclusion of this study is that the idea of an “interactive” specification mining rather than a fully automated mining tool is NOT impractical and indeed is useful for the debugging use case.

Link to Publication: https://www.sciencedirect.com/science/article/pii/S0950584919301004

Mohammad Jafar Mashhadi

University of Calgary

Canada

Taha R. Siddiqui

InfoMagnetics Technologies Corp

Canada

Hadi Hemmati

University of Calgary

Canada

Howard W. Loewen

Department of Electrical & Computer Engineering, University of Calgary

Canada

Modern software systems are increasingly dependent on third-party libraries. It is widely recognized that reusing functionality provided by mature and well-tested third-party libraries can improve developers’ productivity, reduce time-to-market, and produce more reliable software. Today’s open-source repositories provide a wide range of libraries that can be freely downloaded and used. However, as software libraries are documented separately but intended to be used together, developers are unlikely to fully take advantage of these reuse opportunities. In this paper, we present a novel approach to automatically identify third-party library usage patterns, i.e., collections of libraries that are commonly used together by developers. Our approach employs a hierarchical clustering technique to group together software libraries based on external client usage. Our approach is based on the analysis of the joint versus separate use of the libraries. The pattern’s libraries are distributed on different usage cohesion levels/layers. Each layer reflects the co-usage frequency between a set of libraries, while the distribution on the different levels demonstrates the graduation in the degree of co-usage frequency. To evaluate our approach, we mined a large set of over 6000 popular libraries from Maven Central Repository and investigated their usage by over 38,000 client systems from the GitHub repository. Our experiments show that our technique is able to detect the majority (77%) of highly consistent and cohesive library usage patterns across a considerable number of client systems.

Link to Publication: https://www.sciencedirect.com/science/article/pii/S0164121218301699

Mohamed Aymen Saied

Concordia University

Ali Ouni

ETS Montreal, University of Quebec

Canada

Houari Sahraoui

Université de Montréal

Canada

Raula Gaikovina Kula

NAIST

Japan

Katsuro Inoue

Osaka University

Japan

David Lo

Singapore Management University

Singapore

Software systems are often released without formal specifications. To deal with the problem of lack of and outdated specifications, rule-based specification mining approaches have been proposed. These approaches analyze execution traces of a system to infer the rules that characterize the protocols, typically of a library, that its clients must obey. Rule-based specification mining approaches work by exploring the search space of all possible rules and use interestingness measures to differentiate specifications from false positives. Previous rule-based specification mining approaches often rely on one or two interestingness measures, while the potential benefit of combining multiple available interestingness measures is not yet investigated. In this work, we propose a learning to rank based approach that automatically learns a good combination of 38 interestingness measures. Our experiments show that the learning to rank based approach outperforms the best performing approach leveraging single interestingness measure by up to 66%.

Link to Publication: https://ink.library.smu.edu.sg/cgi/viewcontent.cgi?article=4990&context=sis_research

Zherui Cao

Zhejiang University

China

Yuan Tian

Queens University, Kingston, Canada

Canada

Tien-Duy B. Le

School of Information Systems, Singapore Management University

David Lo

Singapore Management University

Singapore

Precise pointer analysis is desired since it is a core technique to find memory defects. There are several dimensions of pointer analysis precision, flow sensitivity, context sensitivity, field sensitivity and path sensitivity. For static analysis tools utilizing pointer analysis, considering all dimensions is difficult because the trade-off between precision and efficiency should be balanced. This paper presents TsmartGP, a static analysis tool for finding memory defects in C programs with a precise and efficient pointer analysis. The pointer analysis algorithm is flow, context, field, and quasi path sensitive. Control flow automatons are the key structures for our analysis to be flow sensitive. Function summaries are applied to get context information and elements of aggregate structures are handled to improve precision. Path conditions are used to filter unreachable paths. For efficiency, a multi-entry mechanism is proposed. Utilizing the pointer analysis algorithm, we implement a checker in TsmartGP to find uninitialized pointer errors in 13 real-world applications. Cppcheck and Clang Static Analyzer are chosen for comparison. The experimental results show that TsmartGP can find more errors while its accuracy rate is 100%, much higher than 3.1% for Cppcheck and 16.7% for Clang Static Analyzer. The demo video is available at https://youtu.be/IQlshemk6OA and TsmartGP can be downloaded from https://github.com/laoyaolandq/TsmartGP.

Yuexing Wang

Tsinghua University

Guang Chen

Tsinghua University

Min Zhou

Tsinghua University

Ming Gu

Tsinghua University

Jiaguang Sun

Tsinghua University

Misuse of APIs happens frequently due to misunderstanding of API semantics and lack of documentation. An important category of API-related defects is the error handling defects, which may result in security and reliability flaws. These defects can be detected with the help of static program analysis, provided that error specifications are known. The error specification of an API function indicates how the function can fail. Writing error specifications manually is time-consuming and tedious. Therefore, automatic inferring the error specification from API usage code is preferred. In this paper, we present Ares, a tool for automatically inferring error specifications for C code through static analysis. we employ multiple heuristics to identify error handling blocks and infer error specifications by analyzing the corresponding condition logic. Ares is evaluated on 19 real world projects, and the results reveal that Ares outperforms the state-of-the-art tool APEx by 37% in precision. Ares can also identify more error specifications than APEx. Moreover, the specifications inferred from Ares help find dozens of API-related bugs in well-known projects such as OpenSSL, among them 10 bugs are confirmed by developers. Video: https://youtu.be/nf1QnFAmu8Q. Repository: https://github.com/lc3412/Ares.

Li Chi

Tsinghua University

Zuxing Gu

School of Software, Tsinghua University

China

Min Zhou

Tsinghua University

Ming Gu

Tsinghua University

Hongyu Zhang

The University of Newcastle

Australia