The recent advancement of the automatic speech recognition (ASR) contributes to the voice user interface (VUI), which is broadly embedded into mobile apps. The VUI implemented on modern mobile operating systems like Android naturally involves multiple threads, and brings new race issues and challenges in defining and identifying them. Specifically, when the GUI and VUI (GV) actions both access to the same resource simultanously, the data race named GV-race may occur. GV-race can lead to wrong behavior and even crashes. However, to the best of our knowledge, this problem has not been adequately studied. In this paper, we present the first study of GV-race on Android apps. However, the involvement of the VUI complicates the concurrency model, affects the temporal relationship and brings state space explosion in global analysis. To tackle these challenges, we firstly defineprimitivesand theirhappen-beforerules to abstract GV interaction patterns. Using these primitives, we are able to characterize and formally define GV-race. We then developRoma(GV-race detectoronmobileapps) to detect both app-level and system-level GV-race automatically. Through static program analysis, Roma extracts GV related call graphs for each pair of conflicting GV actions to reduce the state space, and generates a universal GV interaction graph using our pre-defined primitives. It encodes happen-before constraints to formally specify thefreeness of GV-race, so that the detection of GV-race can be reduced to constraint solving with SMT solvers. We apply Roma to analyze 266 apps. Roma finds 52 apps with app-level GV-race and 56 apps with system-level GV-race. We confirm that 101 apps are true positives.

Code refinement aims to enhance existing code by addressing issues, refactoring, and optimizing to improve quality and meet specific requirements. As software projects scale in size and complexity, the traditional iterative exchange between re-viewers and developers becomes increasingly burdensome. While recent deep learning techniques have been explored to accelerate this process, their performance remains limited, primarily due to challenges in accurately understanding reviewers' intents. This paper proposes an intention-based code refinement technique that enhances the conventional comment-to-code process by explicitly extracting reviewer intentions from the comments. Our approach consists of two key phases: Intention Extraction and Intention Guided Revision Generation. Intention Extraction categorizes comments using predefined templates, while Intention Guided Revision Generation employs large language models (LLMs) to generate revised code based on these defined intentions. Three categories with eight subcategories are designed for comment transformation, which is followed by a hybrid approach that combines rule-based and LLM-based classifiers for accurate classification. Extensive experiments with five LLMs (G PT 40, GPT3.5, DeepSeekV2, DeepSeek7B, CodeQwen7B) under different prompting settings demonstrate that our approach achieves 79 % accuracy in intention extraction and up to 66 % in code refinement generation. Our results highlight the potential of our approach in enhancing data quality and improving the efficiency of code refinement.

In the software development process, formal program specifications play a crucial role in various stages, including requirement analysis, software testing, and verification. However, manually crafting formal program specifications is rather difficult, making the job time-consuming and labor-intensive. Moreover, it is even more challenging to write specifications that correctly and comprehensively describe the semantics of complex programs. To reduce the burden on software developers, automated specification generation methods have emerged. However, existing methods usually rely on predefined templates or grammar, making them struggle to accurately describe the behavior and functionality of complex real-world programs. To tackle this challenge, we introduce SpecGen, a novel technique for formal program specification generation based on Large Language Models (LLMs). Our key insight is to overcome the limitations of existing methods by leveraging the code comprehension capability of LLMs. The process of SpecGen consists of two phases. The first phase employs a conversational approach that guides the LLM in generating appropriate specifications for a given program, aiming to utilize the ability of LLM to generate high-quality specifications. The second phase, designed for where the LLM fails to generate correct specifications, applies four mutation operators to the model-generated specifications and selects verifiable specifications from the mutated ones through a novel heuristic selection strategy by assigning different weights of variants in an efficient manner. We evaluate SpecGen on two datasets, including the SV-COMP Java category benchmark and a manually constructed dataset containing 120 programs. Experimental results demonstrate that SpecGen succeeds in generating verifiable specifications for 279 out of 385 programs, outperforming the existing LLM-based approaches and conventional specification generation tools like Houdini and Daikon. Further investigations on the quality of generated specifications indicate that SpecGen can comprehensively articulate the behaviors of the input program.

Incremental program analysis (IPA) has gained increasing attention as an effective approach for maintaining up-to-date analysis results by leveraging previously computed results in response to program changes. Consequently, a variety of IPA algorithms and tools have been proposed. However, their empirical performance in practical, real-world scenarios remains insufficiently investigated. To address this gap, this study presents a comprehensive examination of the current state-of-the-art in IPA evaluation. Specifically, we identify two key limitations: (1) the lack of standardized benchmarks reflecting real-world program changes, and (2) the inadequacy and imbalanced distribution of evaluation metrics.To overcome these challenges, we propose an automated pipeline for constructing real-world program change benchmarks and develop a unified incremental evaluation framework for systematically evaluating IPA tools. Using the proposed evaluation pipeline, we constructed large-scale benchmarks of real-world program changes—sourced from 4,084 commits across 20 Java projects—and systematically evaluated two IPA tools for Java. The results demonstrate that, although incremental analysis substantially improves efficiency compared to exhaustive analysis, existing IPA tools exhibit inconsistencies and markedly higher peak memory consumption. Finally, we distill practical insights from our findings to inform future research and development in the field of incremental program analysis.

Extended Berkeley Packet Filter (eBPF) allows developers to extend Linux kernel functionality without modifying its source code. To ensure system safety, an in-kernel safety checker, the verifier, enforces strict safety constraints (e.g., a limited program size) on eBPF programs loaded into the kernel. These constraints, combined with eBPF’s performance-critical use cases, make effective optimization essential. However, existing compilers (e.g., Clang) offer limited optimization support, and many semantics-preserving transformations are rejected by the verifier, which makes handcrafted optimization rule design both challenging and limited in effectiveness.Superoptimization overcomes the limitations of rule-based methods by automatically discovering optimal transformations, but its high computational cost limits scalability. To address this, we propose EPSO, a caching-based superoptimizer that discovers rewrite rules via offline superoptimization, and reuses them to achieve high-quality optimizations with minimal runtime overhead. We evaluate EPSO on benchmarks from the Linux kernel and several eBPF-based projects, including Cilium, Katran, hXDP, Sysdig, Tetragon, and Tracee. EPSO discovers 795 rewrite rules and achieves up to 68.87% (avg. 24.37%) reduction in program size compared to Clang’s output, outperforming the state-of-the-art BPF optimizer K2 on all benchmarks and Merlin on 92.68% of them. Additionally, EPSO reduces program runtime by an average of 6.60%, improving throughput and lowering latency in network applications.

For compositional linear hybrid automata (CLHA), whose dynamics can be characterized by linear constraints, bounded model checking (BMC) is challenging due to the complexity caused by interactions among member automata. Classical BMC approaches encode CLHA behavior using interleaving semantics, where compositions are handled with Cartesian product; as a result, the encoding is often large and complex, significantly limiting the scalability and efficiency of BMC. To address this problem, we propose three interaction relations to categorize and describe CLHA interactions through shared-label synchronization, discrete-variable read-write, and time-duration read-write. Based on the interaction relations, we devise interaction-oriented synchronization (IOS) semantics for CLHA behavior, which provides for a concise BMC encoding. In BMC, we employ a path-oriented method to check bounded reachability of CLHA, by enumerating candidate paths and checking each path’s feasibility. To prune the search space of candidate paths, we introduce a temporal relation graph (TRG) to quickly rule out infeasible paths via graph-based checking. Our method is implemented into a CLHA bounded reachability checker, BACH . Experiments indicate that it enables significant efficiency improvement over state-of-the-art tools, and performs scalable bounded reachability analysis on practical CLHA cases within seconds.

Abstract Cyber-physical systems (CPSs) are used in many safety-critical areas, making it crucial to ensure their safety. However, with CPSs increasingly dynamically deployed and reconfigured during runtime, their safety analysis becomes challenging. For one thing, reconfigurable CPSs usually consist of multiple agents dynamically connected during runtime. Their highly dynamic system topologies are too intricate for traditional modeling languages, which, in turn, hinders formal analysis. For another, due to the growing size and uncertainty of reconfigurable CPSs, their system models can be huge and even unavailable at design time. This calls for runtime analysis approaches with better scalability and efficiency. To address these challenges, we propose a scenario-based hierarchical modeling language for reconfigurable CPS. It provides template models for agent inherent features, together with an instantiation mechanism to activate single agent’s runtime behavior, communication configurations for multiple agents’ connected behaviors, and scenario task configurations for their dynamic topologies. We also present a path-oriented falsification approach to falsify system requirements. It employs classification-model-based optimization to explore search space effectively and cut unnecessary system simulations and robustness calculations for efficiency. Our modeling and falsification are implemented in a tool called . Experiments have shown that it can largely reduce modeling time and improve modeling accuracy, and perform scalable CPS falsification with high success rates in seconds.

Digital filters, a subclass of linear time-invariant systems, are widely used in signal processing and control systems. A digital filter performs mathematical operations on a sampled, discrete-time signal to reduce or enhance certain aspects of that signal. Such a system is implemented by a loop that iterates over an infinite time horizon. At each iteration, a random value is generated as input, and a linear expression is evaluated as output. In control theory, bounded-input, bounded-output (BIBO) stability is a fundamental criterion, which requires that any bounded input to a digital filter yields a bounded output. Correspondingly, at the implementation level, we aim to determine if a specified interval bounds the output of a given filter. However, due to the complexity of digital filters, it is hard for state-of-the-art approaches to make a sound over-approximation of all the possible output values of a filter. In this work, considering the strong connection between poles of digital filters and BIBO stability, we propose a poles-based invariant to over-approximate the output ranges of filters. Initially, we design a decomposition of the iteration of a subclass of filters, based on which we derive a set of inequalities to provide bounds on the output. Subsequently, we generalize this approach to over-approximate the output ranges of general digital filters. Moreover, we split the output value at each iteration into two parts. One is computed precisely by bounded analysis. The other is a new filter that can be analyzed using our invariant. This optimization improves the precision of our approach. Leveraging this approach, we develop a prototype tool for verifying programs related to digital filters and compare it with the state-of-the-art. The results demonstrate that our approach delivers more precise over-approximations in less time for verifying BIBO stability.

The rise of code pre-trained models has significantly enhanced various coding tasks, such as code completion, and tools like GitHub Copilot. However, the substantial size of these models, especially large models, poses a significant challenge when it comes to fine-tuning them for specific downstream tasks. As an alternative approach, retrieval-based methods have emerged as a promising solution, augmenting model predictions without the need for fine-tuning. Despite their potential, a significant challenge is that the designs of these methods often rely on heuristics, leaving critical questions about what information should be stored or retrieved and how to interpolate such information for augmenting predictions. To tackle this challenge, we first perform a theoretical analysis of the fine-tuning process, highlighting the importance of delta logits as a catalyst for improving model predictions. Building on this insight, we develop a novel retrieval-based method, FT2Ra, which aims to mimic genuine fine-tuning. While FT2Ra adopts a retrieval-based mechanism, it uniquely adopts a paradigm with a learning rate and multi-epoch retrievals, which is similar to fine-tuning. We conducted a comprehensive evaluation of FT2Ra in both token-level and line-level code completions. Our findings demonstrate the remarkable effectiveness of FT2Ra when compared to state-of-the-art methods and its potential to genuine fine-tuning. In token-level completion, which represents a relatively easier task, FT2Ra achieves a 4.29% improvement in accuracy compared to the best baseline method on UniXcoder. In the more challenging line-level completion task, we observe a substantial more than twice increase in Exact Match (EM) performance, indicating the significant advantages of our theoretical analysis. Notably, even when operating without actual fine-tuning, FT2Ra exhibits competitive performance compared to the models with real fine-tuning.

Abstract The Java virtual machine (JVM) is the cornerstone of the Java platforms. A JVM's exception handling implementation interrupts, when the objective application encounters an exception (or an error), the normal execution of the application and performs specific handling tasks. However, little research has been done in systematically validating JVMs' exception handling implementations—test programs or even applications need to be carefully designed for throwing/catching exceptions at runtime; a JVM's exception handling implementation is also complicated, making it challenging to design tests for testing all of its functionalities. Inspired by the recent success of fuzz testing of compilers and JVM implementations, we introduce EHCBuilder, the first technique for fuzzing JVMs' exception handling implementations. The key idea is to construct exception handling chains, each of which abstracts a program's execution into a sequence of exception throwings, catchings, and/or handlings. A classfile seed can then be mutated into test programs with diverse exception handling chains, enabling (1) exceptions to be continuously thrown and caught at runtime, and (2) JVMs' exception handling implementations to be much more thoroughly tested. We have implemented EHCBuilder and evaluated EHCBuilder on popular JVM implementations including OpenJDK's HotSpot, Eclipse's OpenJ9, Azul's Zulu, and Oracle's GraalVM. Our results show that EHCBuilder can generate programs with very intricate exception handling chains and reveal differences among JVMs' exception handling implementations: Up to thousands of lines of source code in HotSpot's exception handling implementation are covered more than the original benchmarks; during 39 K iterations, EHCBuilder generates exception handling chains of different lengths, revealing 258 runtime differences. We classify the differences into four categories, and reveal a fast throw issue confirmed by HotSpot developers and another initCause issue confirmed by the OpenJ9 community.

Cache side-channel attacks (CSCAs), capable of deducing secrets by analyzing timing differences in the shared cache behavior of modern processors, pose a serious security threat. While there are approaches for detecting CSCAs and mitigating information leaks, they either fail to detect and classify new variants or have to impractically update deployed systems (e.g., CPU). In this work, we propose a novel approach, named SCAGuard, to detect and classify CSCAs via attack behavior modeling and similarity comparison. Specifically, we introduce the notion of cache state transition enhanced basic block sequences (CST-BBSes) to model attack behaviors which is able to capture both attack-relevant syntactic code information and semantic cache information. We propose an approach to automatically construct CST-BBS models from binary programs. To detect and classify attacks, we adapt a dynamic time warping algorithm to compare the similarity of CST-BBSes between attack and target programs. We implement our approach in a tool SCAGuard and evaluate it using real-world attacks and diverse benign programs. The results confirm the effectiveness of our approach, compared over existing detection approaches. In particular, SCAGuard significantly outperforms the other detection approaches on new variants.

The IFDS framework supports interprocedural dataflow analysis with distributive flow functions over finite domains. A large class of interprocedural dataflow analysis problems can be formulated as IFDS problems and thus can be solved with the IFDS framework precisely. Unfortunately, scaling IFDS analysis to large-scale programs is challenging in terms of both massive memory consumption and low analysis efficiency. This paper presents DStream, a scalable system dedicated to precise and highly parallel IFDS analysis for large-scale programs. DStream leverages a streaming-based out-of-core computation model to reduce memory footprint significantly and adopts fine-grained data parallelism to achieve efficiency. We implemented a taint analysis as a DStream instance analysis and compared DStream with three state-of-the-art tools. Our exper-iments validate that DStream outperforms all other tools with average speedups from 4.37x to 14.46x on a commodity PC with limited available memory. Meanwhile, the experiments confirm that DStream successfully scales to large-scale programs which the state-of-the-art tools (e.g., FlowDroid and/or DiskDroid) fail to analyze.

Internet of Things (IoT) has become prevalent in various fields, especially in the context of home automation (HA). To better control HA-IoT devices, especially to integrate several devices for rich smart functionalities, trigger-action programming, such as the If This Then That (IFTTT), has become a popular paradigm. Leveraging it, novice users can easily specify their intent in applets regarding how to control a device/service through another once a specific condition is met. Nevertheless, the users may design IFTTT-style integrations inappropriately, due to lack of security experience or unawareness of the security impact of cyber-attacks against individual devices. This has caused financial loss, privacy leakage, unauthorized access and other security issues. To address these problems, this work proposes a systematic framework named MEDIC to model smart home integrations and check their security. It automatically generates models incorporating the service/device behaviors and action rules of the applets, while taking into consideration the external attacks and in-device vulnerabilities. Our approach takes around one second to complete the modeling and checking of one integration. We carried out experiments based on 200 integrations created from a user study and a dataset crawled from ifttt.com. To our great surprise, nearly 83% of these integrations have security issues.

TVM is a popular deep learning (DL) compiler. It is designed for compiling DL models, which are naturally computation graphs, and as well promoting the efficiency of DL computation. State-of-the-art methods, such as Muffin and NNSmith, allow developers to generate computation graphs for testing DL compilers. However, these techniques are inefficient — their generated computation graphs are either type-invalid or inexpressive, and hence not able to test the core functionalities of a DL compiler.

Control-CPSs are usually safety or mission critical, hence they demand thorough debugging. As nowadays control-CPSs reaching millions of lines of source code, traditional human-flesh debugging is no longer sufficient. We need automated software fault localization (SFL) to assist the debugging. In automated SFL, automatically generated test cases are fed to the control-CPS (or the simulator of the control-CPS), to generate thousands of cyber-subsystem code traces and physical-subsystem trajectories. Next, another automated program, aka oracle, is needed to label the correctness of these physical-subsystem trajectories (and hence cyber-subsystem code traces), even without knowing if there is a bug in the cyber-subsystem. Control-CPS oracle design is a known hard problem. To our best knowledge, AR-SI oracle (denoted as AO in the following) is the most widely adopted control-CPS oracle so far. On the other hand, recently, transformer emerges as a major game changer in the domain of time series prediction. As AO is also time series prediction based, people naturally wonder if transformers can also be used as control-CPS oracles; and if so, can it outperform AO. In this paper, we answer this question by comparing AO with an intuitive design of transformer control-CPS oracle (simplified as TO in the following). Our comparison results show that in terms of SFL accuracy and latency, the TO does not significantly outperform the AO; in terms of false positive rate, the AO performs significantly better; and in terms of false negative rate, the TO performs significantly better.

Virtual personal assistant (VPA) services, e.g. Amazon Alexa and Google Assistant, are becoming increasingly popular recently. Users interact with them through voice-based apps, e.g. Amazon Alexa skills and Google Assistant actions. Unlike the desktop and mobile apps which have visible and intuitive graphical user interface (GUI) to facilitate interaction, VPA apps convey information purely verbally through the voice user interface (VUI), which is known to be limited in its invisibility, single mode and high demand of user attention. This may lead to various problems on the usability and correctness of VPA apps.

A large number of functionality-rich and easily accessible applications have become popular among various virtual personal assistant (VPA) services such as Amazon Alexa. VPA applications (or VPA apps for short) are accompanied by a privacy policy document that informs users of their data handling practices. These documents are usually lengthy and complex for users to comprehend, and developers may intentionally or unintentionally fail to comply with them. In this work, we conduct the first systematic study on the privacy policy compliance issue of VPA apps. We develop Skipper, which targets Amazon Alexa skills. It automatically depicts the skill into the declared privacy profile by analyzing their privacy policy documents with Natural Language Processing (NLP) and machine learning techniques, and derives the behavioral privacy profile of the skill through a black-box testing. We conduct a large-scale analysis on all skills listed on Alexa store, and find that a large number of skills suffer from the privacy policy noncompliance issues.

Abstract BRICK is a bounded reachability checker for embedded C programs. BRICK conducts a path-oriented style checking of the bounded state space of the program, that enumerates and checks all the possible paths of the program in the threshold one by one. To alleviate the path explosion problem, BRICK locates and records unsatisfiable core path segments during the checking of each path and uses them to prune the search space. Furthermore, derivative free optimization based falsification and loop induction are introduced to handle complex program features like nonlinear path conditions and loops efficiently.

Cyber-physical systems (CPSs) integrate discrete computations with continuous physical processes and can be highly nonlinear and nondeterministic. Unlike the verification of CPS, which is difficult to handle, the falsification of CPS fulfills certain requirements from testing by seeking witness behavior of these systems and is easier to conduct. However, existing falsification techniques may fail to support the general complex CPS in practice because they usually focus on certain restricted classes of systems. In this article, we present a path-oriented, derivative-free approach to falsify safety properties in nonlinear and nondeterministic CPS. In our approach, we model the behavior of CPS by hybrid automata. Then, we enumerate candidate paths of hybrid automata (HA), transform the feasibility of candidate paths into optimization problems, and solve these optimization problems by our newly proposed classification model-based, derivative-free optimization algorithm. We also provide two novel pruning techniques to further improve the efficiency and efficacy of our approach: 1) a nested optimization structure with better model refinements for continuous search space pruning and 2) a hardly feasible path prefixes guided backtracking for discrete search space pruning. We implement our approach into a tool called PDF. Our experiments showed that PDF supported the safety falsification of CPS in all of our benchmarks, and it achieved success rates no lower than 95% in only seconds on 22/28 of the benchmarks.

Neural network based (NN-based) classifiers are known vulnerable against adversarial examples, namely, adding slight perturbations to a benign image cause a classifier to make a false prediction. To evaluate the robustness of NN-based classifiers against adversarial examples, numerous adversarial attacks with high success rates have been proposed recently. NN-based image classifiers usually normalize valid images (e.g., RGB image where the value at each coordinate is an integer between 0 and 255) into a real continuous domain (e.g., 3-dimensional matrix where the value at each coordinate is a real number between 0 and 1) and make classification decisions on the normalized images. However, adversarial examples crafted in a real continuous domain may become benign once they are denormalized back into the corresponding discrete integer domain, known as the discretization problem. This problem has been mentioned in some prior works but received relatively limited attention. In this work, we report the first comprehensive study of existing works to understand the impacts of the discretization problem. By analyzing 35 representative methods and empirically studying 20 representative open source tools, we found 29/35 (theoretically) and 14/20 (empirically) are affected by the discretization problem, e.g., the success rate could dramatically drop from 100 to 10 percent after the domain transformation. As the first step towards addressing this problem in a black-box scenario, we propose a novel derivative-free optimization method, which can directly craft adversarial examples in the discrete integer domain. Experimental results show that the method achieves nearly 100 percent attack success rates for both targeted and untargeted attacks, comparable to the most popular white-box methods (FGSM, BIM and C&W), and significantly outperforms representative black-box methods (ZOO, AutoZOOM, NES-PGD, Bandits, FD, FD-PSO and GenAttack). Our results suggest that the discretization problem should be treated more seriously, and the discrete optimization algorithms show a promising future in crafting effective black-box attacks.

Smart contracts are computerized transaction protocols built on top of blockchain networks. Users are charged with fees, a.k.a. gas in Ethereum, when they create, deploy or execute smart contracts. Since smart contracts may contain vulnerabilities which may result in huge financial loss, developers and smart contract compilers often insert codes for security checks. The trouble is that those codes consume gas every time they are executed. Many of the inserted codes are however redundant. In this work, we present sOptimize, a tool that optimizes smart contract gas consumption automatically without compromising functionality or security. sOptimize works on smart contract bytecode, statically identifies 3 kinds of code patterns, and further removes them through verification-assisted techniques. The resulting code is guaranteed to be equivalent to the original one and can be directly deployed on blockchain. We evaluate sOptimize on a collection of 1,152 real-world smart contracts and show that it optimizes 43% of them, and the reduction on gas consumption is about 2.0% while in deployment and 1.2% in transactions, the amount can be as high as 954,201 gas units per contract.

Hybrid systems are widely used in safety-critical areas. Hybrid optimal control synthesis, which aims to generate an optimal sequence of control inputs for a given task, is one of the most important problems in the field. The classical Gradient-based methods are efficient but they require the system under control should be differentiable. Sampling-based methods have no such limitations, but the ability of existing ones to solve complex control missions is restricted.

With many trigger-action platforms that integrate Internet of Things (IoT) systems and online services, rich functionalities transparently connecting digital and physical worlds become easily accessible for the end users. On the other hand, such facilities incorporate multiple parties whose data control policies may radically differ and even contradict each other, and thus privacy violations may arise throughout the lifecycle (e.g., generation and transmission) of triggers and actions. In this work, we conduct an in-depth study on the privacy issues in multi-party trigger-action integration platforms (TAIPs). We first characterize privacy violations that may arise with the integration of heterogeneous systems and services. Based on this knowledge, we propose Taifu, a dynamic testing approach to identify privacy weaknesses from the TAIP. The key insight of Taifu is that the applets which actually program the trigger-action rules can be used as test cases to explore the behavior of the TAIP. We evaluate the effectiveness of our approach by applying it on the TAIPs that are built around the IFTTT platform. To our great surprise, we find that privacy violations are prevalent among them. Using the automatically generated 407 applets, each from a different TAIP, Taifu detects 194 cases with access policy breaches, 218 access control missing, 90 access revocation missing, 15 unintended flows, and 73 over-privilege access.

Abstract During program traversing, symbolic execution collects path conditions and feeds them to a constraint solver to obtain feasible solutions. However, complex path conditions, like nonlinear constraints, which widely appear in programs, are hard to be handled efficiently by the existing solvers. In this paper, we adapt the classical symbolic execution framework with a machine learning approach for constraint satisfaction. The approach samples and learns from different solutions to identify potentially feasible area. This sampling-learning style solving can be applied in different class of complex problems easily. Therefore, incorporating this approach, our framework, MLBSE, supports the symbolic execution of not only simple linear path conditions, but also nonlinear arithmetic operations, and even black-box function calls of library methods. Meanwhile, thanks to the theoretical foundation of the machine learning based approach, when the solver fails to solve a path condition, we can have an estimation of the confidence in the satisfiability (ECS) of the problem to give users insights about how the problem is analyzed and whether they could ultimately find a solution. We implement MLBSE on the basis of Symbolic Path Finder (SPF) into a fully automatic Java symbolic execution engine. Users can feed their code to MLBSE directly, which is very convenient to use. To evaluate its performance, 22 real case programs are used as the benchmarks for MLBSE to generate test cases, which involve a total number of 1042 methods that are full of nonlinear operations, floating-point arithmetic as well as native method calls. Experiment results show that the coverage achieved by MLBSE is much higher than the state-of-the-art tools.

Ordinary users can build their smart home automation system easily nowadays, but such user-customized systems could be error-prone. Using formal verification to prove the correctness of such systems is necessary. However, to conduct formal proof, formal specifications such as Linear Temporal Logic (LTL) formulas have to be provided, but ordinary users cannot author LTL formulas but only natural language.To address this problem, this paper presents a novel approach that can automatically generate formal LTL specifications from natural language requirements based on domain knowledge and our proposed ambiguity refining techniques. Experimental results show that our approach can achieve a high correctness rate of 95.4% in converting natural language sentences into LTL formulas from 481 requirements of real examples.

In this paper, we revisit model predictive control (MPC) for the classical wheeled mobile robot (WMR) navigation problem. We prove that the reachable set based hierarchical MPC (HMPC), a state-of-the-art MPC, cannot handle WMR navigation in theory due to the non-existence of non-trivial linear system with an under-approximate reachable set of WMR. Nevertheless, we propose a virtual linear leader guided MPC (VLL-MPC) to enable HMPC structure. Different from current HMPCs, we use a virtual linear system with an under-approximate path set rather than the traditional trace set to guide the WMR. We provide a valid construction of the virtual linear leader. We prove the stability of VLL-MPC, and discuss its complexity. In the experiment, we demonstrate the advantage of VLL-MPC empirically by comparing it with NMPC, LMPC and anytime RRT* in several scenarios.

Unlike standalone embedded devices, behaviors of a cyber-physical system (CPS) are highly dynamic. Many parameter values (e.g., those related to nature environment and third party black box functions) are unknown offline. Furthermore, distributed sub-CPSs may exchange data online. In this article, we first propose the concept of parametric hybrid automata (PHA) to describe such complex CPSs. As some PHA parameter values are unknown until runtime, conventional offline model checking is infeasible. Instead, we propose to carry out PHA model checking online, as a fault prediction mechanism. However, this usage is challenged by the high time cost of state reachability verification, which is the conventional focus of model checking. To address this challenge, we propose that the model checking shall focus on online scenario reachability validation instead. Furthermore, we propose a mechanism to compose/decompose scenarios. Our scenario reachability validation can exploit linear programming to achieve polynomial time cost. Evaluations on a state-of-the-art train control system show that our approach can cut online model checking time cost from over 1 h to within 200 ms.

Periodically online verification has been widely recognized as a practical and promising method to handle the non-deterministic and unpredictable behavior of dynamic CPS systems. However, it is a challenge to keep the online verification of CPS systems finishing quickly in time to give enough time for the running system to respond, if any error is detected. Nevertheless, the problems under verification for each cycle are highly similar to each other. Most of the differences are caused by run-time factors like changing of parameters' values or the reorganization of active components in the system. Under this investigation, this paper presents an incremental verification technique for online verification of CPS systems. A method is given to distinguish the differences between the problem under verification and the previous verified problem. Then, by reusing the problem space of the previous verified problem as a warm-start base, the modified part can be introduced into the base, which can be solved incrementally and efficiently. A set of case studies on a real-case train control system is presented in this paper to demonstrate the performance of the incremental online verification technique.

Control Cyber-Physical Systems (CPSs) constitute a major category of CPS. In control CPSs, in addition to the well-studied noises within the physical subsystem, we are interested in evaluating the impact of cross-domain noise : the noise that comes from the physical subsystem, propagates through the cyber subsystem, and goes back to the physical subsystem. Impact of cross-domain noise is hard to evaluate when the cyber subsystem is a black box, which cannot be explicitly modeled. To address this challenge, this article focuses on the two-level control CPS, a widely adopted control CPS architecture, and proposes an emulation based evaluation methodology framework. The framework uses hybrid model reachability to quantify the cross-domain noise impact, and exploits Lyapunov stability theories to reduce the evaluation benchmark size. We validated the effectiveness and efficiency of our proposed framework on a representative control CPS testbed. Particularly, 24.1% of evaluation effort is saved using the proposed benchmark shrinking technology.

Recent advances and industry standards in Internet of Things (IoT) have accelerated the real-world adoption of connected devices. To manage this hybrid system of digital real-time devices and analog environments, the industry has pushed several popular home automation IoT (HA-IoT) frameworks, such as If-This-Then-That (IFTTT), Apple HomeKit, and Google Brillo. Typically, users author device interactions by specifying the triggering sensor event and the triggered device command. In this seemingly simple software system, two dominant factors govern the system confidence properties with respect to the physical world. First, IoT users are largely nonexperts who lack the comprehensive consideration regarding potential impact and joint effect with existing rules. Second, while the increasing complexity of IoT devices enables fine-grained control (e.g., heater temperature) of continuous real-time environments, even two simply connected devices can have a huge state space to explore. In fact, bugs that wrongfully control devices and home appliances can have ramifications on system correctness and even user physical safety. It is crucial to help users to make sure the system they created meets their expectation. In this article we introduce how techniques from hybrid automata can be practically applied to assist nonexpert IoT users in the confidence checking of such hybrid HA-IoT systems. We propose an automated framework for end-to-end programming assistance. We build and check the Linear Hybrid Automata (LHA) model of the system automatically. We also present a quantifier elimination-based method to analyze the counterexample found and synthesize fix suggestions. We implemented a platform, MenShen, based on this framework and proposed techniques. We conducted sets of real HA-IoT case studies with up to 46 devices and 65 rules. Empirical results show that MenShen can find violations and generate rule fix suggestions in only 10 seconds.

Mobile applications with complex GUIs are very popular today. However, generating test cases for these applications is often tedious professional work. On the one hand, manually designing and writing elaborate GUI scripts requires expertise. On the other hand, generating GUI scripts with record and playback techniques usually depends on repetitive work that testers need to interact with the application over and over again, because only one path is recorded in an execution. Automatic GUI testing focuses on exploring combinations of GUI events. As the number of combinations is huge, it is still necessary to introduce a test interface for testers to reduce its search space. This paper presents a sketch-guided GUI test generation approach for testing mobile applications, which provides a simple but expressive interface for testers to specify their testing purposes. Testers just need to draw a few simple strokes on the screenshots. Then our approach translates the strokes to a testing model and initiates a model-based automatic GUI testing. We evaluate our sketch-guided approach on a few real-world Android applications collected from the literature. The results show that our approach can achieve higher coverage than existing automatic GUI testing techniques with just 10-minute sketching for an application.

Reachability analysis of linear hybrid automata (LHA) is an important problem. Classical model checking (CMC) technique is not scalable and not guaranteed to terminate. On the other hand, bounded model checking (BMC) is more cost-effective to conduct but can not guarantee the safety beyond the bound. In this paper, we seek to bridge the gap between BMC and CMC for reachability analysis of LHA. During BMC of LHA, typical procedures can discover sets of unsatisfiable constraint cores, which can be mapped back to path segments in the graph structure of LHA. If every path connecting the initial and target location has to go through such infeasible path segment, the target location is entirely not reachable. Based on this characteristic, we propose a LTL model checking based approach to check whether the target location is blocked. To further optimize the performance, we propose an automata based solution to check the LTL specification incrementally and adopt an on-the-fly algorithm to check the accepting condition to avoid an explicit construction of product automata.

Existing CSP model checkers are incapable of verifying multiple properties concurrently in one run of a model checker, and when trying to alleviate state space explosion problem, most of reduction work are usually done after rather than before the complete state space was produced. Thus, A new CSP model checking tool named ACSPChecker was developed based on answer set programming, which is a declarative logic programming paradigm for solving combinational search problems with the feature of completely free of sequential dependencies, to verifying multiple properties concurrently in one run of a model checker. Additionally, It integrated an abstraction method, which could be used to alleviate the state space explosion before the complete state space was produced. Furthermore, a preprocessing technique of properties was proposed to improve the verification efficiency by reducing the expense spending on replicated verification of the same sub formulas. The feasibility and efficiency of ACSPChecker are illustrated by the experiments with a classic concurrency problem - dining philosophers problem.

Symbolic execution is a widely-used program analysis technique. It collects and solves path conditions to guide the program traversing. However, due to the limitation of the current constraint solvers, it is difficult to apply symbolic execution on programs with complex path conditions, like nonlinear constraints and function calls. In this paper, we propose a new symbolic execution tool MLB to handle such problem. Instead of relying on the classical constraint solving, in MLB, the feasibility problems of the path conditions are transformed into optimization problems, by minimizing some dissatisfaction degree. The optimization problems are then handled by the underlying optimization solver through machine learning guided sampling and validation. MLB is implemented on the basis of Symbolic PathFinder and encodes not only the simple linear path conditions, but also nonlinear arithmetic operations, and even black-box function calls of library methods, into symbolic path conditions. Experiment results show that MLB can achieve much better coverage on complex real-world programs.

Cyber-Physical Systems (CPS) integrate discrete-time computing and continuous-time physical-world entities, which are often wirelessly interlinked. The use of wireless safety-critical CPS requires safety guarantees despite communication faults. This paper focuses on one important set of such safety rules: Proper-Temporal-Embedding (PTE), where distributed CPS entities must enter/leave risky states according to properly nested temporal pattern and certain duration spacing. Our solution introduces hybrid automata to formally describe and analyze CPS design patterns. We propose a novel leasing based design pattern, along with closed-form configuration constraints, to guarantee PTE safety rules under arbitrary wireless communication faults. We propose a formal procedure to transform the design pattern hybrid automata into specific wireless CPS designs. This procedure can effectively isolate physical world parameters from affecting the PTE safety of the resultant specific designs. We conduct two wireless CPS case studies, one on medicine and the other on control, to show that the resulted system is safe against communication failures. We also compare our approach with a polling based approach. Both approaches support PTE under arbitrary communication failures. The polling approach performs better under severely adverse wireless medium conditions; while ours performs better under benign or moderately adverse wireless medium conditions.

The behavior space of real time hybrid systems is very complex and hence expensive to conduct the classical full state space model checking. Compared to the classical model checking, bounded model checking (BMC) is much cheaper to conduct and has better scalability. This work presents a technique that can derive, in some cases, a proof of unbounded reach ability argument of Linear Hybrid Automata (LHA) from a BMC procedure. During BMC of LHA, typical procedures can discover sets of unsatisfiable constraint cores, a.k.a. UC or IIS, in the constraint set according to the bounded continuous state space of LHA. Currently, such unsatisfiable constraints are only fed back to the constraint set to accelerate the BMC solving. In this paper, we propose that such unsatisfiable constraint core can be exploited to give general unbounded verification result of the system model. As each constraint can be mapped back to certain semantical elements of the system model, the unsatisfiable constraint cores can be mapped back into path segments, which are not feasible, in the graph structure of the LHA model. Clearly, if all the potential paths to reach the target location in the graph structure have to go through such infeasible path segments, the target location is not reachable in general, not only in the given bound. Based on this observation, we propose to encode the infeasible path segments as linear temporal logic (LTL) formulas, and present the graph structure, the discrete part, of the LHA model as a transition system. Then, we can take advantage of the mature off-the-shelf LTL model checking techniques to verify whether there exists a path to reach the target location without touching any detected IIS path segment in the graph structure of the LHA model. We implement this technique into a bounded LHA checker BACH. The experiments show that most of the benchmarks can be verified by the enhanced BACH with a clearly better performance and scalability.

Hybrid systems model checking is a great success in guaranteeing the safety of computerized control cyber-physical systems (CPS). However, when applying hybrid systems model checking to Medical Device Plug-and-Play (MDPnP) CPS, we encounter two challenges due to the complexity of human body: 1) there are no good offline differential equation-based models for many human body parameters; 2) the complexity of human body can result in many variables, complicating the system model. In an attempt to address the challenges, we propose to alter the traditional approach of offline hybrid systems model checking of time-unbounded (i.e., infinite horizon, a.k.a., long run) future behavior to online hybrid systems model checking of time-bounded (i.e., finite horizon, a.k.a., short run) future behavior. According to this proposal, online model checking runs as a real-time task to prevent faults. To meet the real-time requirements, certain design patterns must be followed, which brings up the codesign issue. We propose two sets of system codesign patterns for hard real time and soft real time, respectively. To evaluate our proposals, a case study on laser tracheotomy MDPnP is carried out. The study shows the necessity of online model checking. Furthermore, test results based on real-world human subject trace show the feasibility and effectiveness of our proposed codesign.

Cyber-Physical Systems (CPS) integrate discrete-time computing and continuous-time physical-world entities, which are often wirelessly interlinked. The use of wireless safety critical CPS (control, healthcare etc.) requires safety guarantees despite communication faults. This paper focuses on one important set of such safety rules: Proper-Temporal-Embedding (PTE). Our solution introduces hybrid automata to formally describe and analyze CPS design patterns. We propose a novel lease based design pattern, along with closed-form configuration constraints, to guarantee PTE safety rules under arbitrary wireless communication faults. We propose a formal methodology to transform the design pattern hybrid automata into specific wireless CPS designs. This methodology can effectively isolate physical world parameters from affecting the PTE safety of the resultant specific designs. We conduct a case study on laser tracheotomy wireless CPS to show that the resulting system is safe and can withstand communication disruptions.

Dealing with crosscutting concerns has been a critical problem in software development processes. To facilitate handling crosscutting concerns at design phases, we proposed an aspect-oriented modeling and integration approach with UML activity diagrams. The primary concerns are depicted with UML activity diagrams as primary models, whereas crosscutting concerns are described with aspectual extended activity diagrams as aspect models. Aspect models can be integrated into primary models automatically. The AOM approach can reduce the complexity of design models. However, potential faults that violate desired properties of the software system might still be introduced during the modeling or integration processes. The verification technique is well-known for its ability to assure the correctness of models and uncover design problems before implementation. We propose a framework to verify aspect-oriented UML activity diagrams based on Petri net verification techniques. For verification purpose, we transform the integrated activity diagrams into Petri nets and prove the consistency of the transformation. Then, crosscutting concerns in system requirements are refined to properties in the form of CTL formulas. Finally, the Petri nets are verified against the formalized properties to report whether the aspect-oriented design models satisfies the requirements. Furthermore, we implement a tool named Jasmine-AOV to support the verification process. Case studies are conducted to evaluate the effectiveness of the proposed approach.

Regression testing is a widely used way to assure the quality of modified software. It requires executing a suite of test cases to ensure that modifications do not introduce any negative impact to software behavior. To collect test cases in the suite that can reveal modifications, different versions of software must be compared carefully. Existing approaches, relying on manual examination on programs or models to identify differences, are expensive. In the paper, we present a fully automatic approach to generating regression test cases based on activity diagram revision. By collecting execution traces and revising old activity diagrams, the approach firstly constructs new activity diagrams that can reveal software behavior changes. Then, both affected paths and new paths in activity diagrams are identified. Finally, an execution-based approach is applied to generate regression test cases whose execution can cover these paths. Experiments show the effectiveness of our approach.

Scenario-based specifications (SBSs), such as UML interaction models, offer an intuitive and visual way of describing design requirements, and are playing an increasingly important role in the design of software systems. This paper presents an approach to timing analysis of SBSs expressed by UML interaction models. The approach considers more general and expressive timing constraints in UML sequence diagrams (SDs), and gives a solution to the reachability analysis, constraint conformance analysis and bounded delay analysis problems, which reduces these problems into linear programs. With the synchronous interpretation of the SD compositions, the timing analysis algorithms in the approach form a decision procedure for a class of SBSs where any loop in any path is time-independent of the other parts in the path. These algorithms are also a semi-decision procedure for general SBSs with both the synchronous and asynchronous composition semantics. The approach also supports bounded timing analysis of SBSs, which investigates all the paths in the bound limit one by one, and performs the timing analysis for each finite path by linear programming. A tool prototype has been developed to support this approach. Copyright © 2010 John Wiley & Sons, Ltd. (This paper presents a linear programming-based approach to timing analysis of scenario-based specifications (SBSs) expressed by UML interaction models. With more general and expressive timing constraints in UML sequence diagrams, the algorithms in the approach solve the problems of the reachability, constraint conformance and bounded delay analysis of SBSs. These algorithms form a decision procedure for the loop-unlimited SBSs where any loop in any path is time-independent of the other parts in the path, and a semi-decision procedure for general SBSs.)

Existing reachability analysis techniques are easy to fail when applied to large compositional linear hybrid systems, since their memory usages rise up quickly with the increase of systems' size. To address this problem, we propose a tool BACH 2 that adopts a path-oriented method for bounded reachability analysis of compositional linear hybrid systems. For each component, a path is selected and all selected paths compose a path set for reachability analysis. Each path is independently encoded to a set of constraints while synchronization controls are encoded as a set of constraints too. By merging all the constraints into one set, the path-oriented reachability problem of a path set can be transformed to the feasibility problem of this resulting linear constraint set, which can be solved by linear programming efficiently. Based on this path-oriented method, BACH 2 adopts a shared label sequence guided depth first search (SLS-DFS) method to perform bounded reachability analysis of compositional linear hybrid system, where all potential path sets within the bound limit are identified and verified one by one. By this means, since only the structure of a system and the recently visited one path in each component need to be stored in memory, memory consumption of BACH 2 is very small at runtime. As a result, BACH 2 enables the verification of extremely large systems, as is demonstrated in our experiments.

Since Wireless Sensor Networks (WSNs) are increasingly used in many industrial and civilian application areas, the correctness of their low level protocol such as the Flooding Time Synchronization Protocol (FTSP) is critical. However ensuring such correctness is difficult because of the complexity of the runtime environment. Model checking is an effective method for this problem, since it is a formal verification approach which has an advantage in exploring all behaviors of the system and discovering subtle errors. In this paper, we present a novel timed automaton model for FTSP. The main insight of our method is that by using timed automata, we can introduce the transmission delay and node failures that exist in real WSNs into our model and check whether FTSP is robust to node failures under a more realistic environment. We generate the timed automata models of FTSP and verify them by the model checking tool UPPAAL. Our evaluation result depicts an error of FTSP when the algorithm runs in the scenario that two root nodes fail continuously.

Hybrid automata are well studied formal models for hybrid systems with both discrete and continuous state changes. However, the analysis of hybrid automata is quite difficult. Even for the simple class of linear hybrid automata, the reachability problem is undecidable. In the author's previous work, for linear hybrid automata we proposed a linear programming based approach to check one path at a time while the length of the path and the size of the automaton being checked can be large enough to handle problems of practical interest. Based on this approach, in this paper we present a prototype tool BACH to perform bounded reachability checking of linear hybrid automata. The experiment data shows that BACH has good performance and scalability, and supports our belief that BACH could become a powerful assistant to design engineers for the reachability analysis of linear hybrid automata.