Video Large Language Models (VideoLLMs) are increasingly deployed on numerous critical applications, where users rely on auto-generated summaries while casually skimming the video stream. We show that this interaction hides a critical safety gap: if harmful content is embedded in a video, either as full-frame inserts or as small corner patches, state-of-the-art VideoLLMs rarely mention the harmful content in the output, despite its clear visibility to human viewers. A root-cause analysis reveals three compounding design flaws: (1) insufficient temporal coverage resulting from the sparse, uniformly spaced frame sampling used by most leading VideoLLMs, (2) spatial information loss introduced by aggressive token downsampling within sampled frames, and (3) encoder-decoder disconnection, whereby visual cues are only weakly utilized during text generation. Leveraging these insights, we craft three zero-query black-box attacks, aligning with these flaws in the processing pipeline. Our large-scale evaluation across five leading VideoLLMs shows that the harmfulness omission rate exceeds 90\% in most cases. Even when harmful content is clearly present in all frames, these models consistently fail to identify it. These results underscore a fundamental vulnerability in current VideoLLMs' designs and highlight the urgent need for sampling strategies, token compression, and decoding mechanisms that guarantee semantic coverage rather than speed alone.

Precise event spotting (PES) aims to recognize fine-grained events at exact moments and has become a key component of sports analytics. This task is particularly challenging due to rapid succession, motion blur, and subtle visual differences. Consequently, most existing methods rely on domain-specific, end-to-end training with large labeled datasets and often struggle in few-shot conditions due to their dependence on pixel- or pose-based inputs alone. However, obtaining large labeled datasets is practically hard. We propose a Unified Multi-Entity Graph Network (UMEG-Net) for few-shot PES. UMEG-Net integrates human skeletons and sport-specific object keypoints into a unified graph and features an efficient spatio-temporal extraction module based on advanced GCN and multi-scale temporal shift. To further enhance performance, we employ multimodal distillation to transfer knowledge from keypoint-based graphs to visual representations. Our approach achieves robust performance with limited labeled data and significantly outperforms baseline models in few-shot settings, providing a scalable and effective solution for few-shot PES.

Xiaoyue Lu, Xianglin Yang, Haijun Liu, Jiahao Liu, Kuntai Cai, Yan Xiao, Jin Song Dong. Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). 2026.

Xing Ma, Yangjie Zhou, Wu Sun, Zihan Liu, Jingwen Leng, Yun Lin, Shixuan Sun, Minyi Guo, Jin Song Dong. Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). 2026.

Quantization is widely used to enable local deployment of large language models (LLMs) on resource-constrained devices. Recent work (e.g., QuRA) shows quantization can be exploited via rounding manipulation to implant backdoors. However, such an attack has been evaluated only on small models and does not directly apply to LLMs due to three key constraints: (1) limited poisoning data from small, task-agnostic calibration sets; (2) layer-wise quantization restricting adversarial access to global representations; and (3) lack of gradient access in quantization pipelines, blocking gradient-based attacks.

The real-time demand for web security makes Security Information and Event Management (SIEM) platforms and their applied security rule an integral part of the intrusion detection life-cycle. However, the heterogeneity of vendor-specific rules (e.g., Splunk SPL, Microsoft KQL, IBM AQL, Google YARA-L, and RSA ESA) makes cross-platform rule reuse extremely difficult, requiring deep domain knowledge for reliable conversion. As a result, an autonomous and accurate rule conversion framework can significantly lead to effort savings, preserving the value of existing rules. In this paper, we propose ARuleCon, an agentic SIEM-rule conversion approach. Using ARuleCon, the security professionals do not need to distill the source rules' logic and re-map it to target vendors, instead, they provide the source rules, the documentation of the target rules and ARuleCon can purposely convert to the target vendors without more intervention. To achieve this, ARuleCon is equipped with intermediate representation (IR) that aligns core detection logic into vendor-neutral layer, agentic RAG pipeline that retrieves authoritative official vendor documentation to address the convension/schema mismatches, and Python-based consistency check that running both source and target rules in controlled test environments to mitigate subtle semantic drifts. We present a comprehensive evaluation of ARuleCon ranging from textual alignment between the source and target rules, and the execution success of target rules, showcasing ARuleCon can convert rules with higher fidelity, outperforming the baseline LLM models by 15% averagely. Finally, we perform a case study and interview with our industry collaborators 1, which showcases that ARuleCon can significantly save the expert's time on understanding the cross-SIEM's documentation and remapping the logic.

This paper investigates the use of deep reinforcement learning (DRL) for the control of mobile robot teams within the context of navigation and task-based collaborative scenarios. We apply a DRL policy with a tailored neural network architecture as a solution to control, path planning, and higher-level guidance tasks. Our network architecture was trained using a unique multi-stage curriculum that progresses from single-agent navigation, to multi-agent pathfinding with obstacles, and finally to a complex collaborative firefighting scenario. This structured approach accelerates training convergence by systematically building sophisticated collaborative behaviours upon foundational skills, which enhances training stability and guides the agents towards learning effective and coordinated strategies The policy evaluation was conducted in both simulation and hybrid simulation-physical demonstrations utilising a real unmanned ground vehicle (UGV). The policy presented is capable of achieving multi-agent navigation tasks with a 95.83% accuracy in our testing environments, and has demonstrated emergent multi-agent behaviours. In more complex collaborative firefighting scenarios, the policy also demonstrated superior performance than baselines in reaching goals, e.g., navigating and extinguishing two fires with a 99.67% success rate, suggesting its strong potential for real-world deployment.

Large language models (LLMs) for code editing have achieved remarkable progress, yet recent empirical studies reveal a fundamental disconnect between technical accuracy and developer productivity . Despite their strong benchmark performance, developers complete tasks 19% slower when using AI assistance, with over 68.81% of recommendations disrupting their mental flow. This misalignment stems from the use of static commit snapshots that lack temporal information, causing models to optimize for end results rather than the incremental, context-sensitive steps that align with developers’ natural reasoning process. To bridge this gap, we present EditFlow , which benchmarks and optimizes subsequent code edit recommendation systems through the reconstruction of developer editing flows. EditFlow addresses three key challenges. First, collecting edit-order data that reflects developers’ flow is inherently difficult: manual annotation introduces prohibitive overhead, while development logs capture only single trajectories instead of all plausible editing flows. Second, benchmarking recommendation performance against developers’ ongoing editing flow requires a digital-twin-like simulation that can faithfully simulate the editing process. Third, existing heterogeneous systems vary drastically in scale and architecture, posing challenges for developing a unified optimization strategy that endows all models with mental-flow awareness regardless of design or capability. To overcome these challenges, we propose three tightly coupled components: (1) a prompt auto-tuning mechanism that learns an optimized prompt for inferring the relative order between two edits, (2) a digital twin that replays reconstructed edit sequences to simulate developers’ editing process, and (3) EditFlow , a unified optimization strategy that optimizes the flow continuity of subsequent edit suggestions based on developers’ ongoing flow. Evaluations across diverse benchmarks, including manually annotated commits, real-world industrial code, and open-source repositories, show that EditFlow improves order reconstruction accuracy by 63.81%, reduces flow violations by over 75%, and boosts recommendation precision by 66.99%. A user study with 32 developers further demonstrates 25.11% faster task completion and significantly higher perceived recommendation quality. To the best of our knowledge, EditFlow is the first to evaluate and optimize code edit recommendation systems from the perspective of developers’ mental flow, establishing flow-awareness as a new dimension for advancing human-AI code collaboration.

Skeleton action recognition models have secured more attention than video-based ones in various applications due to privacy preservation and lower storage requirements. Skeleton data are typically transmitted to cloud servers for action recognition, with results returned to clients via Apps/APIs. However, the vulnerability of skeletal models against adversarial perturbations gradually reveals the unreliability of these systems. Existing black-box attacks all operate in a decision-based manner, resulting in numerous queries that hinder efficiency and feasibility in real-world applications. Moreover, all attacks off the shelf focus on only restricted perturbations, while ignoring model weaknesses when encountered with non-semantic perturbations. In this paper, we propose two query-effIcient Skeletal Adversarial AttaCks, ISAAC-K and ISAAC-N. As a black-box attack, ISAAC-K utilizes Grad-CAM in a surrogate model to extract key joints where minor sparse perturbations are then added to fool the classifier. To guarantee natural adversarial motions, we introduce constraints of both bone length and temporal consistency. ISAAC-K finds stronger adversarial examples on ℓ∞norm, which can encompass those on other norms. Exhaustive experiments substantiate that ISAAC-K can uplift the attack efficiency of the perturbations under 10 skeletal models. Additionally, as a byproduct, ISAAC-N fools the classifier by replacing skeletons unrelated to the action. We surprisingly find that skeletal models are vulnerable to large perturbations where the part-wise non-semantic joints are just replaced, leading to a query-free no-box attack without any prior knowledge. Based on that, four adaptive defenses are eventually proposed to improve the robustness of skeleton recognition models.

Secure three-party computation (3PC) with semi-honest security under an honest majority offers notable efficiency in computation and communication; for Boolean circuits, each party sends a single bit for every AND gate, and nothing for XOR. However, round complexity remains a significant challenge, especially in high-latency networks. Some works can support multi-input AND and thereby reduce online round complexity, but they requireexponentialcommunication for generating the correlations in either preprocessing or online phase. How to extend the AND gate to multi-input while maintaining high correlation generation efficiency is still not solved. To address this problem, we propose a round-efficient 3PC framework ALKAID for Boolean circuits through improved multi-input AND gate. By mixing correlations and redundancy, we propose a concretely efficient correlation generation approach for small input bitsNN> 4. Exploiting the improved multi-input AND gates, we design fast depth-optimized parallel prefix adder and share conversion primitives in 3PC, achieved with new techniques and optimizations for better concrete efficiency. We further apply these optimized primitives to enhance the efficiency of secure non-linear functions in machine learning. We implement ALKAID and extensively evaluate its performance. Compared to state of the arts like ABY3 (CCS’2018), Trifecta (PoPETs’2023), and METEOR (WWW’2023), ALKAID enjoys 1.5×–2.5× efficiency improvements for boolean primitives and non-linear functions, with better or comparable communication.

GUI test migration aims to produce test cases with events and assertions to test specific functionalities of a target app. Existing migration approaches typically focus on the widget-mapping paradigm that maps widgets from source apps to target apps. However, since different apps may implement the same functionality in different ways, direct mapping may result in incomplete or buggy test cases, thus significantly impacting the effectiveness of testing the target functionality and the practical applicability of migration approaches. In this article, we propose a new migration paradigm (i.e., the abstraction-concretization paradigm) that first abstracts the test logic for the target functionality and then utilizes this logic to generate the concrete GUI test case. Furthermore, we introduce MACdroid , the first approach that migrates GUI test cases based on this paradigm. Specifically, we propose an abstraction technique that utilizes source test cases from source apps targeting the same functionality to extract a general test logic for that functionality. Then, we propose a concretization technique that utilizes the general test logic to guide an LLM in generating the corresponding GUI test case (including events and assertions) for the target app. We evaluate MACdroid on two widely used datasets (including 31 apps, 34 functionalities, and 123 test cases). On the FrUITeR dataset, the test cases generated by MACdroid successfully test 64% of the target functionalities, improving the baselines by 191%. On the Lin dataset, MACdroid successfully tests 75% of the target functionalities, outperforming the baselines by 42%. These results underscore the effectiveness of MACdroid in GUI test migration.

Analyzing Fast, Frequent, and Fine-grained ($F^3$) events presents a significant challenge in video analytics and multi-modal LLMs. Current methods struggle to identify events that satisfy all the $F^3$ criteria with high accuracy due to challenges such as motion blur and subtle visual discrepancies. To advance research in video understanding, we introduce $F^3Set$, a benchmark that consists of video datasets for precise $F^3$ event detection. Datasets in $F^3Set$ are characterized by their extensive scale and comprehensive detail, usually encompassing over 1,000 event types with precise timestamps and supporting multi-level granularity. Currently, $F^3Set$ contains several sports datasets, and this framework may be extended to other applications as well. We evaluated popular temporal action understanding methods on $F^3Set$, revealing substantial challenges for existing techniques. Additionally, we propose a new method, $F^3ED$, for $F^3$ event detections, achieving superior performance. The dataset, model, and benchmark code are available at https://github.com/F3Set/F3Set.

Recent studies have raised significant concerns regarding the vulnerability of Large Vision Language Models (LVLMs) to maliciously injected or perturbed input images, which can mislead their responses. Existing defense methods show that such vision attacks are sensitive to image modifications especially cropping, using majority voting across responses of modified images as corrected responses. However, these modifications often result in partial images and distort the semantics, which reduces response quality on clean images after voting. Instead of directly using responses from partial images for voting, we investigate using them to supervise (guide) the LVLM’s responses to the original images at inference time. We propose a black-box, training-free method called DPS (Defense through Partial-Perception Supervision). In this approach, the model is prompted using the responses generated by a model that perceives only a partial image. With DPS, the model can adjust its response based on partial image understanding when under attack, while confidently maintaining its original response for clean input. Empirical experiments show our method outperforms the baseline, cutting the average attack success rate by 76.3% across six datasets on three popular models.

Self-supervised learning (SSL) methods via joint embedding architectures have proven remarkably effective at capturing semantically rich representations with strong clustering properties, magically in the absence of label supervision. Despite this, few of them have explored leveraging these untapped properties to improve themselves. In this paper, we provide an evidence through various metrics that the encoder's output *encoding* exhibits superior and more stable clustering properties compared to other components. Building on this insight, we propose a novel positive-feedback SSL method, termed **Re**presentation **S**elf-**A**ssignment (ReSA), which leverages the model's clustering properties to promote learning in a self-guided manner. Extensive experiments on standard SSL benchmarks reveal that models pretrained with ReSA outperform other state-of-the-art SSL methods by a significant margin. Finally, we analyze how ReSA facilitates better clustering properties, demonstrating that it effectively enhances clustering performance at both fine-grained and coarse-grained levels, shaping representations that are inherently more structured and semantically meaningful.

Deep Reinforcement Learning (DRL) is a paradigm of artificial intelligence where an agent uses a neural network to learn which actions to take in a given environment. DRL has recently gained traction from being able to solve complex environments like driving simulators, 3D robotic control, and multiplayer-online-battle-arena video games. Numerous implementations of the state-of-the-art algorithms responsible for training these agents, like the Deep Q-Network (DQN) and Proximal Policy Optimization (PPO) algorithms, currently exist. However, studies make the mistake of assuming implementations of the same algorithm to be consistent and thus, interchangeable. In this paper, through a differential testing lens, we present the results of studying the extent of implementation inconsistencies, their effect on the implementations' performance, as well as their impact on the conclusions of prior studies under the assumption of interchangeable implementations. The outcomes of our differential tests showed significant discrepancies between the tested algorithm implementations, indicating that they are not interchangeable. In particular, out of the five PPO implementations tested on 56 games, three implementations achieved superhuman performance for 50% of their total trials while the other two implementations only achieved superhuman performance for less than 15% of their total trials. Furthermore, the performance among the high-performing PPO implementations was found to differ significantly in nine games. As part of a meticulous manual analysis of the implementations' source code, we analyzed implementation discrepancies and determined that code-level inconsistencies primarily caused these discrepancies. Lastly, we replicated a study and showed that this assumption of implementation interchangeability was sufficient to flip experiment outcomes. Therefore, this calls for a shift in how implementations are being used. In addition, we recommend for (1) replicability studies for studies mistakenly assuming implementation interchangeability, (2) DRL researchers and practitioners to adopt the differential testing methodology proposed in this paper to combat implementation inconsistencies, and (3) the use of large environment suites.

In industrial and open-source software engineering tasks, developers often perform project-wise code editing tasks, including feature enhancement, refactoring, and bug fixing, where the leading AI models are expected to support the productivity. Hence, researchers and practitioners have proposed and adopted many LLM-based solutions to facilitate their real-world development. However, they largely suffer from the balance among predicting scope, accuracy, and efficiency. For example, solutions like Cursor achieve high accuracy only in a local editing scope while its performance drops on cross-file edits. In contrast, solutions like CoEdPilot exhibit efficiency limitations when used to predict project-wise edits.In this work, we propose TRACE (Tool-integrated RecommendAtion for Code Editing), a novel subsequent code editing solution to push the boundary of scope, accuracy, and efficiency. Our rationale lies in that code edits are triggered for either semantic or syntactic reasons. Therefore, TRACE predicts subsequent edits by interleaving neural-based induction for semantic edit prediction and tool-based deduction for syntactic edit prediction. The tools can be any IDE facilities, such as refactoring tools (e.g., rename) or linting tools (e.g., use-def), providing decent performance of deducing edit-location and edit-generation. Technically, we address the challenge of (1) when to interleave between neural-based and tool-based prediction and (2) how to further improve the performance of neural-based prediction. As for the former, we learn a neural model to detect when to invoke IDE editing tools. As for the latter, we propose a novel and fine-grained editing representation to further boost the performance of neural editing models.Our extensive experiments show that, in comparison to the state-of-the-arts such as CoEdPilot, GrACE, and CCT5, TRACE significantly improves the performance of edit location (by 43.76%) and edit generation (by 11.16%). Our simulation experiment on an interactive editing setting shows that TRACE achieves an acceptance rate 6.15% higher than Cursor. Moreover, our user study consists of 24 participants on Cursor, CoEdPilot, and TRACE, on three code editing tasks. The results show that the experimental group with TRACE achieves leading performance on cross-file global edits. In addition, we observe concerning user behaviours on how participants deal with false predictions by the tools, shedding light on the design of future code-editing tools.

Recent advances in large language models (LLMs) offer promising potential for automating formal methods. However, applying them to formal verification remains challenging due to the complexity of specification languages, the risk of hallucinated output, and the semantic gap between natural language and formal logic. We introduce PAT-Agent, an end-to-end framework for natural language autoformalization and formal model repair that combines the generative capabilities of LLMs with the rigor of formal verification to automate the construction of verifiable formal models. In PAT-Agent, a Planning LLM first extracts key modeling elements and generates a detailed plan using semantic prompts, which then guides a Code Generation LLM to synthesize syntactically correct and semantically faithful formal models. The resulting code is verified using the Process Anal y sis Toolkit (PAT) model checker against user-specified properties, and when discrepancies occur, a Repair Loop is triggered to iteratively correct the model using counterexamples. To improve flexibility, we built a web-based interface that enables users, particularly non-FM-experts, to describe, customize, and verify system behaviors through user-LLM interactions. Experimental results on 40 systems show that PAT-Agent consistently outperforms baselines, achieving high verification success with superior efficiency. The ablation studies confirm the importance of both planning and repair components, and the user study demonstrates that our interface is accessible and supports effective formal modeling, even for users with limited formal methods experience.

Face recognition is essential for identity authentication, but the rich visual clues in facial images pose significant privacy risks, highlighting the critical importance of privacy-preserving solutions. For instance, numerous studies have shown that generative models are capable of effectively performing reconstruction attacks that result in the restoration of original visual clues. To mitigate this threat, we introduce FracFace, a fractal-based privacy-preserving face recognition framework. This approach effectively weakens the visual clues that can be exploited by reconstruction attacks by disrupting the spatial structure in frequency domain features, while retaining the vital visual clues required for identity recognition. To achieve this, we craft a Frequency Channels Refining module that reduces sparsity in the frequency domain. It suppresses visual clues that could be exploited by reconstruction attacks, while preserving features indispensable for recognition, thus making these attacks more challenging. More significantly, we design a Frequency Fractal Mapping module that obfuscates deep representations by remapping refined frequency channels into a fractal-based privacy structure. By leveraging the self-similarity of fractals, this module preserves identity relevant features while enhancing defense capabilities, thereby improving the overall robustness of the protection scheme. Experiments conducted on multiple public face recognition benchmarks demonstrate that the proposed FracFace significantly reduces the visual recoverability of facial features, while maintaining high recognition accuracy, as well as the superiorities over state-of-the-art privacy protection approaches.

Recent advances in Audio-Language Models (ALMs) have significantly improved multimodal understanding capabilities. However, the introduction of the audio modality also brings new and unique vulnerability vectors. Previous studies have proposed jailbreak attacks that specifically target ALMs, revealing that defenses directly transferred from traditional audio adversarial attacks or text-based Large Language Model (LLM) jailbreaks are largely ineffective against these ALM-specific threats. To address this issue, we propose ALMGuard, the first defense framework tailored to ALMs. Based on the assumption that safety-aligned shortcuts naturally exist in ALMs, we design a method to identify universal Shortcut Activation Perturbations (SAPs) that serve as triggers that activate the safety shortcuts to safeguard ALMs at inference time. To better sift out effective triggers while preserving the model’s utility on benign tasks, we further propose Mel-Gradient Sparse Mask (M-GSM), which restricts perturbations to Mel-frequency bins that are sensitive to jailbreaks but insensitive to speech understanding. Both theoretical analyses and empirical results demonstrate the robustness of our method against both seen and unseen attacks. Overall, \MethodName reduces the average success rate of advanced ALM-specific jailbreak attacks to 4.6\% across four models, while maintaining comparable utility on benign benchmarks, establishing it as the new state of the art. Our code and data are available at https://github.com/WeifeiJin/ALMGuard.

Large language models (LLMs) have emerged as a dominant AI paradigm due to their exceptional text understanding and generation capabilities. However, their tendency to generate inconsistent or erroneous outputs challenges their reliability, especially in high-stakes domains requiring accuracy and trustworthiness. Existing research primarily focuses on detecting and mitigating model misbehavior in general-purpose scenarios, often overlooking the potential of integrating domain-specific knowledge. In this work, we advance misbehavior detection by incorporating domain knowledge. The core idea is to design a general specification language that enables domain experts to customize domain-specific constraints in a lightweight and intuitive manner, supporting later runtime monitoring of LLM outputs. To achieve this, we design a novel specification language ESL, and introduce a runtime verification framework RvLLM to validate LLM output against domain-specific constraints defined in ESL. RvLLM operates in two main stages: interpretation and reasoning. During interpretation, it derives interpretations of the specification based on the context, which then guide the reasoning process to identify inconsistencies. When new knowledge is derived, RvLLM issues a follow-up query to the LLM to further verify the consistency. We evaluate RvLLM on three representative tasks: violation detection against Singapore Rapid Transit Systems Act, numerical comparison, and inequality solving. Experimental results show that RvLLM effectively detects erroneous outputs across various LLMs in a lightweight and flexible manner. The results reveal that despite their impressive capabilities, LLMs remain prone to low-level errors due to a lack of formal guarantees during inference, and our framework offers a potential long-term solution by leveraging expert domain knowledge to rigorously and efficiently verify LLM outputs.

Dynamic-shape tensor computation poses challenges for shape-specific compilation due to variable input dimensions. Existing compilers rely on shape samples, incurring high tuning costs and performance degradation on unseen inputs. We present Helix, a dynamic tensor compilation framework with sample-free compilation and architecture-guided optimization to achieve both compilation efficiency and shape-general performance. To avoid shape sampling, Helix constructs shape-agnostic compilation by decomposing computations across architectural layers. A bidirectional strategy combines top-down abstraction to align tensor computations with architectural hierarchies, and bottom-up kernel construction to build efficient execution strategies from reusable, architecture-aligned micro-kernels. A hybrid analyzer ensures accuracy through profiling at lower architectural levels, and achieves scalability through architecture-informed modeling at higher levels and runtime. This hierarchical design eliminates shape-specific tuning and enables shape-adaptive execution. Evaluations conducted on x86 CPUs, ARM CPUs, and NVIDIA GPUs demonstrate that Helix reduces compilation time by 174 × over the existing compilers and delivers 2.26 × and 3.29 × execution speedups over vendor libraries and dynamic-shape compilers, respectively.

Many Transformer-based pre-trained models for code have been developed and applied to code-related tasks. In this paper, we analyze 519 papers published on this topic during 2017-2023, examine the suitability of model architectures for different tasks, summarize their resource consumption, and look at the generalization ability of models on different datasets. We examine three representative pre-trained models for code: CodeBERT, CodeGPT, and CodeT5, and conduct experiments on the four topmost targeted software engineering tasks from the literature: Bug Fixing, Bug Detection, Code Summarization, and Code Search. We make four important empirical contributions to the field. First, we demonstrate that encoder-only models (CodeBERT) can outperform encoder-decoder models for general-purpose coding tasks, and showcase the capability of decoder-only models (CodeGPT) for certain generation tasks. Second, we study the most frequently used model-task combinations in the literature and find that less popular models can provide higher performance. Third, we find that CodeBERT is efficient in understanding tasks while CodeT5's efficiency is unreliable on generation tasks due to its high resource consumption. Fourth, we report on poor model generalization for the most popular benchmarks and datasets on Bug Fixing and Code Summarization tasks. We frame our contributions in terms of promises and perils, and document the numerous practical issues in advancing future research on transformer-based models for code-related tasks.

Recently, the rise of code-centric Large Language Models (LLMs) has reshaped the software engineering world with low-barrier tools like Copilot that can easily generate code. However, there is no correctness guarantee for the code generated by LLMs, which suffer from the hallucination problem, and their output is fraught with risks. Besides, the end-to-end process from specification to code through LLMs is a non-transparent and uncontrolled black box. This opacity makes it difficult for users to understand and trust the generated code. Addressing these challenges is both necessary and critical. In contrast, program refinement transforms high-level specification statements into executable code while preserving correctness. Traditional tools for program refinement are primarily designed for formal methods experts and lack automation and extensibility. We apply program refinement to guide LLM and validate the LLM-generated code while transforming refinement into a more accessible and flexible framework. To initiate this vision, we propose Refine4LLM, an approach that aims to:(1) Formally refine the specifications, (2) Automatically prompt and guide the LLM using refinement calculus, (3) Interact with the LLM to generate the code, (4) Verify that the generated code satisfies the constraints, thus guaranteeing its correctness, (5) Learn and build more advanced refinement laws to extend the refinement calculus. We evaluated Refine4LLM against the state-of-the-art baselines on program refinement and LLMs benchmarks. The experiment results show that Refine4LLM can efficiently generate more robust code and reduce the time for refinement and verification.

In the rapidly evolving landscape of neural network security, the resilience of neural networks against bit-flip attacks (i.e., an attacker maliciously flips an extremely small amount of bits within its parameter storage memory system to induce harmful behavior), has emerged as a relevant area of research. Existing studies suggest that quantization may serve as a viable defense against such attacks. Recognizing the documented susceptibility of real-valued neural networks to such attacks and the comparative robustness of quantized neural networks (QNNs), in this work, we introduce BFAVerifier, the first verification framework designed to formally verify the absence of bit-flip attacks against QNNs or to identify all vulnerable parameters in a sound and rigorous manner. BFAVerifier comprises two integral components: an abstraction-based method and an MILP-based method. Specifically, we first conduct a reachability analysis with respect to symbolic parameters that represent the potential bit-flip attacks, based on a novel abstract domain with a sound guarantee. If the reachability analysis fails to prove the resilience of such attacks, then we encode this verification problem into an equivalent MILP problem which can be solved by off-the-shelf solvers. Therefore, BFAVerifier is sound, complete, and reasonably efficient. We conduct extensive experiments, which demonstrate its effectiveness and efficiency across various activation functions, quantization bit-widths, and adversary capabilities.

Despite being widely used in network intrusion detection systems (NIDSs), machine learning (ML) has proven to be vulnerable to adversarial attacks. White-box and black-box adversarial ML attacks of NIDS have been explored in several studies. However, white-box attacks unrealistically assume that the attackers have full knowledge of the target NIDSs. Meanwhile, existing black-box attacks can not achieve high attack success rate due to the weak adversarial transferability between models (e.g., neural networks and tree models). Additionally, neither of them explains why adversarial examples exist and why they can transfer across models. To address these challenges, this paper introduces ETA, anExplainableTransfer-based Black-Box AdversarialAttack framework. ETA aims to achieve two primary objectives: 1) create transferable adversarial examples applicable to various ML detectors and 2) provide insights into the existence of adversarial examples and their transferability within NIDSs. Specifically, we first provide a general transfer-based adversarial attack method applicable across the entire ML space. Following that, we exploit a unique insight based on cooperative game theory and perturbation interpretations to explain adversarial examples and adversarial transferability. On this basis, we propose an Important-Sensitive Feature Selection (ISFS) method to guide the search for adversarial examples, achieving stronger transferability and ensuring traffic-space constraints. Finally, the experimental results on three NIDSs datasets show that our method performs significantly effectively against several classical and state-of-the-art ML classifiers, outperforming the latest baselines. We conduct three interpretation experiments and two cases to verify our interpretation method's correctness. Meanwhile, we uncover two major misconceptions about applying machine learning to NIDSs systems.

Abstract Quantization plays an important role in deploying neural networks on embedded, real-time systems with limited computing and storage resources (e.g., edge devices). It significantly reduces the model storage cost and improves inference efficiency by using fewer bits to represent the parameters. However, it was recently shown that critical properties may be broken after quantization, such as robustness and backdoor-freeness. In this work, we introduce the first method for synthesizing quantization strategies that verifiably maintain desired properties after quantization, leveraging a key insight that quantization leads to a data distribution shift in each layer. We propose to compute the preimage for each layer based on which the preceding layer is quantized, ensuring that the quantized reachable region of the preceding layer remains within the preimage. To tackle the challenge of computing the exact preimage, we propose an MILP-based method to compute its under-approximation. We implement our method into a tool and demonstrate its effectiveness and efficiency by providing certified quantization that successfully preserves model robustness and backdoor-freeness.

Recent years have seen the development of LLM-based code generation. Compared to generating code in a software project, incremental code edits are empirically observed to be more frequent. The emerging code editing approaches usually formulate the problem as generating an edit based on known relevant prior edits and context. However, practical code edits can be more complicated. First, an editing session can include multiple (ir)relevant edits to the code under edit. Second, the inference of the subsequent edits is non-trivial as the scope of its ripple effect can be the whole project. In this work, we propose CoEdPilot, an LLM-driven solution to recommend code edits by discriminating the relevant edits, exploring their interactive natures, and estimating its ripple effect in the project. Specifically, CoEdPilot orchestrates multiple neural transformers to identify what and how to edit in the project regarding both edit location and edit content. When a user accomplishes an edit with an optional editing description, an Subsequent Edit Analysis first reports the most relevant files in the project with what types of edits (e.g., keep, insert, and replace) can happen for each line of their code. Next, an Edit-content Generator generates concrete edit options for the lines of code, regarding its relevant prior changes reported by an Edit-dependency Analyzer. Last, both the Subsequent Edit Analysis and the Edit-content Generator capture relevant prior edits as feedback to readjust their recommendations. We train our models by collecting over 180K commits from 471 open-source projects in 5 programming languages. Our extensive experiments show that (1) CoEdPilot can well predict the edits (i.e., predicting edit location with accuracy of 70.8%-85.3%, and the edit content with exact match rate of 41.8% and BLEU4 score of 60.7); (2) CoEdPilot can well boost existing edit generators such as GRACE and CCT5 on exact match rate by 8.57% points and BLEU4 score by 18.08. Last, our user study on 18 participants with 3 editing tasks (1) shows that CoEdPilot can be effective in assisting users to edit code in comparison with Copilot, and (2) sheds light on the future improvement of the tool design. The video demonstration of our tool is available at https://sites.google.com/view/coedpilot/home.

Collaborative software development significantly enhances development productivity by enabling multiple contributors to work concurrently on different branches. Despite these advantages, such collaboration often increases the likelihood of causing conflicts. Resolving these conflicts brings huge challenges, primarily due to the necessity of comprehending the differences between conflicting versions. Researchers have explored various automatic conflict resolution techniques, including unstructured, structured, and learning-based approaches. However, these techniques are mostly heuristic-based or black-box in nature, which means they do not attempt to solve the root cause of the conflicts, i.e., the existence of different program behaviors exhibited by the conflicting versions.

Web applications are crucial infrastructures in the modern society, which have high demand of reliability and security. However, their frontend can be manipulable by the clients (e.g., the frontend code can be modified to bypass some validation steps), which incurs the runtime anomaly when operating the web service. Existing state-of-the-art anomaly detectors largely learn a deep learning model from the collected logs to predict abnormal logs with a probability. While effective in general, those approaches can suffer from (1) inaccuracy caused by subtle difference between the normal and abnormal/attack logs and (2) additional efforts for root cause analysis.

Since browser extensions are prevailingly executed in the background to enable extra functionalities and enhance the user experience for web browsers, the potential over-collection of personal data beyond the necessity for given purposes is always ignored by ordinary users. Existing privacy regulations, such as the principle of Data Minimization in GDPR, have provided the criteria that only directly relevant and necessary data for specified purposes should be collected. Various tools have made efforts to examine the compliance of data minimization and its equivalent in different application domains. To our knowledge, in the area of browser extensions, there is still a gap between the general data minimization principle and precisely defined extension behaviors. We propose MINDAExT, a framework that takes one step further to automatically examine end-to-end data minimization practices in browser extensions by description text analysis and hybrid program analysis techniques. In our large-scale measurement, covering around 200K extensions collected in October 2023, we find that 38.0 % of extensions are likely to collect private user data outside their essential functionality scopes. They are distributed across all categories, exhibiting distinct patterns of the target data types. Our evaluation shows that MINDAEXT can detect the data over-collection with a precision of 74.3 %.

Relation prediction in knowledge graphs (KGs) aims at predicting missing relations in incomplete triples, whereas the dominant paradigm by KG embeddings has a limitation to predict the relation between unseen entities. This situation is called an inductive setting, which is more common in the real-world scenario. To handle this issue, implicit symbolic rules have shown great potential in capturing the inductive capability. However, it is still challenging to obtain precise representations of logic rules from KGs. The argument variability and predicate non-commutativity in symbolic rule integration make the modeling of component symbols difficult. To this end, we propose a novel inductive relation prediction model named SymRITa with a logic transformer integrating rules. SymRITa firstly extracts the subgraph, whose embeddings are captured by a graph network. Meanwhile, symbolic rule graphs in the subgraph can be generated. Then, the symbolic rules are modeled by a proposed logic transformer. Specifically, the input format based on the subgraph-based embeddings is to focus on the argument variability in symbolic rules. In addition, a conjunction attention mechanism in the logic transformer can resolve predicate non-commutativity in the symbolic rule integration process. Finally, the subgraph-based and symbol-based embeddings obtained from the previous steps are combined for the training regime, and prediction results as well as rules explaining the reasoning process are explicitly output. Extensive experiments on twelve inductive datasets show that SymRITa achieves outstanding effectiveness compared to state-of-the-art inductive baselines. Moreover, the logic rules with corresponding confidences provide an interpretable paradigm.

This article investigates a class of constrained distributed fuzzy convex optimization problems, where the objective function is the sum of a set of local fuzzy convex objective functions, and the constraints include partial order relation and closed convex set constraints. In undirected connected node communication network, each node only knows its own objective function and constraints, and the local objective function and partial order relation functions may be nonsmooth. To solve this problem, a recurrent neural network approach based on differential inclusion framework is proposed. The network model is constructed with the help of the idea of penalty function, and the estimation of penalty parameters in advance is eliminated. Through theoretical analysis, it is proven that the state solution of the network enters the feasible region in finite time and does not escape again, and finally reaches consensus at an optimal solution of the distributed fuzzy optimization problem. Furthermore, the stability and global convergence of the network do not depend on the selection of the initial state. A numerical example and an intelligent ship output power optimization problem are given to illustrate the feasibility and effectiveness of the proposed approach.

Nowadays there are a wealth of devices and cameras at sports venues and facilities that collect different forms of data. Mining useful insights from such data are crucial for improving the performance of professional athletes. In this paper, we introduce a new interactive tennis analytics framework that can realistically simulate tennis matches using parameters mined from past match data and help reveal in-depth knowledge about tennis strategies. Our approach uses probabilistic model checking to formally evaluate the effectiveness of various strategies and tactics and recommend the best ones for improving players’ chances of winning. Our framework is easily understandable and actionable by players and coaches at any level. We have performed evaluations on tennis matches over the past decade to show the effectiveness of our strategy analytics framework.

Sports analytics encompasses the use of data science, AI, psychology, and IoT devices to improve sports performance, strategy, and decision-making. It involves collecting, processing, and interpreting data from various sources such as video recordings and scouting reports. The data is used to evaluate player and team performance, prevent injuries, and help coaches make informed decisions in game and training. We adopt Probabilistic Model Checking (PMC), a method commonly used in reliability analysis for complex safety systems, and explain how this method can be applied to sports strategy analytics to increase the chance of winning by taking into account the reliability of a player’s specific sub-skill sets. This paper describes how we have integrated PMC, machine learning, and computer vision to develop a new and complex system for sports strategy analytics. Finally, we discuss the vision of a new series of international sports analytics conferences (https://formal-analysis.com/isace/2023/).

When deploying pre-trained neural network models in real-world applications, model consumers often encounter resource-constraint platforms such as mobile and smart devices. They typically use the pruning technique to reduce the size and complexity of the model, generating a lighter one with less resource consumption. Nonetheless, most existing pruning methods are proposed with a premise that the model after being pruned has a chance to be fine-tuned or even retrained based on the original training data. This may be unrealistic in practice, as the data controllers are often reluctant to provide their model consumers with the original data. In this work, we study the neural network pruning in the data-free context, aiming to yield lightweight models that are not only accurate in prediction but also robust against undesired inputs in open-world deployments. Considering the absence of fine-tuning and retraining that can fix the mis-pruned units, we replace the traditional aggressive one-shot strategy with a conservative one that treats model pruning as a progressive process. We propose a pruning method based on stochastic optimization that uses robustness-related metrics to guide the pruning process. Our method is evaluated with a series of experiments on diverse neural network models. The experimental results show that it significantly outperforms existing one-shot data-free pruning approaches in terms of robustness preservation and accuracy.

Neural networks are an emerging data-driven programming paradigm widely used in many areas. Unlike traditional software systems consisting of decomposable modules, a neural network is usually delivered as a monolithic package, raising challenges for some maintenance tasks such as model restructure and re-adaption. In this work, we propose DeepArc, a novel modularization method for neural networks, to reduce the cost of model maintenance tasks. Specifically, DeepArc decomposes a neural network into several consecutive modules, each of which encapsulates consecutive layers with similar semantics. The network modularization facilitates practical tasks such as refactoring the model to preserve existing features (e.g., model compression) and enhancing the model with new features (e.g., fitting new samples). The modularization and encapsulation allow us to restructure or retrain the model by only pruning and tuning a few localized neurons and layers. Our experiments show that (1) DeepArc can boost the runtime efficiency of the state-of-the-art model compression techniques by 14.8%; (2) compared to the traditional model retraining, DeepArc only needs to train less than 20% of the neurons on average to fit adversarial samples and repair under-performing models, leading to 32.85% faster training performance while achieving similar model prediction performance.

Graph contrastive learning (GCL), aiming for an embedding space where semantically similar nodes are closer, has been widely applied in graph-structured data. Researchers have proposed many approaches to define positive and negative pairs (i.e., semantically similar and dissimilar pairs) on the graph, serving as labels to learn their embedding distances. Despite the effectiveness, those approaches usually suffer from two typical learning challenges. First, the number of candidate negative pairs is enormous. Thus, it is non-trivial to select representative ones to train the model in a more effective way. Second, the heuristics (e.g., graph views or meta-path patterns) to define positive and negative pairs are sometimes less reliable, causing considerable noise for both "labelled'' positive and negative pairs. In this work, we propose a novel sampling approach B2-Sampling to address the above challenges in a unified way. On the one hand, we use balanced sampling to select the most representative negative pairs regarding both the topological and embedding diversities. On the other hand, we use biased sampling to learn and correct the labels of the most error-prone negative pairs during the training. The balanced and biased samplings can be applied iteratively for discriminating and correcting training pairs, boosting the performance of GCL models. B2-Sampling is designed as a framework to support many known GCL models. Our extensive experiments on node classification, node clustering, and graph classification tasks show that B2-Sampling significantly improves the performance of GCL models with acceptable runtime overhead. Our website[11] https://sites.google.com/view/b2-sampling/home provides access to our codes and additional experiment results.

Researchers recently investigated to explain Graph Neural Networks (GNNs) on the access to a task-specific GNN, which may hinder their wide applications in practice. Specifically, task-specific explanation methods are incapable of explaining pretrained GNNs whose downstream tasks are usually inaccessible, not to mention giving explanations for the transferable knowledge in pretrained GNNs. Additionally, task-specific methods only consider target models' output in the label space, which are coarse-grained and insufficient to reflect the model's internal logic. To address these limitations, we consider a two-stage explanation strategy, i.e., explainers are first pretrained in a task-agnostic fashion in the representation space and then further fine-tuned in the task-specific label space and representation space jointly if downstream tasks are accessible. The two-stage explanation strategy endows post-hoc graph explanations with the applicability to pretrained GNNs where downstream tasks are inaccessible and the capacity to explain the transferable knowledge in the pretrained GNNs. Moreover, as the two-stage explanation strategy explains the GNNs in the representation space, the fine-grained information in the representation space also empowers the explanations. Furthermore, to achieve a trade-off between the fidelity and intelligibility of explanations, we propose an explanation framework based on the Information Bottleneck principle, named Explainable Graph Information Bottleneck (EGIB). EGIB subsumes the task-specific explanation and task-agnostic explanation into a unified framework. To optimize EGIB objective, we derive a tractable bound and adopt a simple yet effective explanation generation architecture. Based on the unified framework, we further theoretically prove that task-agnostic explanation is a relaxed sufficient condition of task-specific explanation, which indicates the transferability of task-agnostic explanations. Extensive experimental results demonstrate the effectiveness of our proposed explanation method.

Deep learning models are emerging to summarize source code to comment, facilitating tasks of code documentation and program comprehension. Scaled-up large language models trained on large open corpus have achieved good performance in such tasks. However, in practice, the subject code in one certain project can be specific, which may not align with the overall training corpus. Some code samples from other projects may be contradictory and introduce inconsistencies when the models try to fit all the samples. In this work, we introduce a novel approach, Adacom, to improve the performance of comment generators by on-the-fly model adaptation. This research is motivated by the observation that deep comment generators often need to strike a balance as they need to fit all the training samples. Specifically, for one certain target code $c$, some training samples $S_p$ could have made more contributions while other samples $S_o$ could have counter effects. However, the traditional fine-tuned models need to fit both $S_p$ and $S_o$ from a global perspective, leading to compromised performance for one certain target code $c$. In this context, we design Adacom to (1) detect whether the model might have a compromised performance on a target code $c$ and (2) retrieve a few helpful training samples $S_p$ that have contradictory samples in the training dataset and, (3) adapt the model on the fly by re-training the $S_p$ to strengthen the helpful samples and unlearn the harmful samples. Our extensive experiments on 7 comment generators and 4 public datasets show that (1) can significantly boost the performance of comment generation (BLEU4 score by on average 14.9\%, METEOR by 12.2\%, and ROUGE-L by 7.4\%), (2) the adaptation on one code sample is cost-effective and acceptable as an on-the-fly solution, and (3) can adapt well on out-of-distribution code samples.

Detecting temporally precise and fine-grained events from tennis videos is important in automatic video annotation. This paper addresses the challenges of recognizing a sequence of events from tennis video clips, focusing on accurate timestep identification and distinguishing subtle class differences. We propose a novel but simple end-to-end event detection network to accurately detect and identify the key events, which can be trained on a single GPU. We demonstrate that our model outperforms the existing baselines on our fine-grained tennis event dataset. The research contributes to the development of tennis video analytics and has broader implications in other sports domains.

Each week, there are 2-3 top-level professional tennis tournaments around the world offering attractive prize money and ranking points for the players. Even though match playing is an important part of the professional tennis player’s career development, sports injuries will happen if the player plays too many tournaments. By analyzing historical data and studying cases where players retired during matches, we have been able to identify specific scheduling patterns that correlate with a higher risk of injury. As a result, we propose a dynamic tennis injury prediction model as well as an explainable pattern-mining method to obtain player-specific injury patterns based on historical data. Both approaches take into account features such as the player’s physical condition, match performance, injury history, and recent tournament schedule. With these comprehensive approaches, we aim to balance competitive success and the preservation of players’ well-being.

A deep classifier is usually trained to (i) learn the numeric representation vector of samples and (ii) classify sample representations with learned classification boundaries. Time-travelling visualization, as an explainable AI technique, is designed to transform the model training dynamics into an animation of canvas with colorful dots and territories. Despite that the training dynamics of the high-level concepts such as sample representations and classification boundaries are now observable, the model developers can still be overwhelmed by tens of thousands of moving dots across hundreds of training epochs (i.e., frames in the animation), which makes them miss important training events.

Understanding how the predictions of deep learning models are formed during the training process is crucial to improve model performance and fix model defects, especially when we need to investigate nontrivial training strategies such as active learning, and track the root cause of unexpected training results such as performance degeneration. In this work, we propose a time-travelling visual solution DeepVisualInsight (DVI), aiming to manifest the spatio-temporal causality while training a deep learning image classifier. The spatio-temporal causality demonstrates how the gradient-descent algorithm and various training data sampling techniques can influence and reshape the layout of learnt input representation and the classification boundaries in consecutive epochs. Such causality allows us to observe and analyze the whole learning process in the visible low dimensional space. Technically, we propose four spatial and temporal properties and design our visualization solution to satisfy them. These properties preserve the most important information when projecting and inverse-projecting input samples between the visible low-dimensional and the invisible high-dimensional space, for causal analyses. Our extensive experiments show that, comparing to baseline approaches, we achieve the best visualization performance regarding the spatial/temporal properties and visualization efficiency. Moreover, our case study shows that our visual solution can well reflect the characteristics of various training scenarios, showing good potential of DVI as a debugging tool for analyzing deep learning training processes.

This paper presents the conceptualisation of a framework that combines digital twins with runtime verification and applies the techniques in the context of security monitoring and verification for satellites. We focus on special considerations needed for space missions and satellites, and we discuss how digital twins in such applications can be developed and how the states of the twins should be synchronised. In particular, we present state synchronisation methods to ensure secure and efficient long-distance communication between the satellite and its digital twin on the ground. Building on top of this, we develop a runtime verification engine for the digital twin that can verify properties in multiple temporal logic languages. We end the paper with our proposal to develop a fully verified satellite digital twin system as future work.

Time-travelling visualization answers how the predictions of a deep classifier are formed during the training. It visualizes in two or three dimensional space how the classification boundaries and sample embeddings are evolved during training. In this work, we propose TimeVis, a novel time-travelling visualization solution for deep classifiers. Comparing to the state-of-the-art solution DeepVisualInsight (DVI), TimeVis can significantly (1) reduce visualization errors for rendering samples’ travel across different training epochs, and (2) improve the visualization efficiency. To this end, we design a technique called temporality spatialization, which unifies the spatial relation (e.g., neighbouring samples in single epoch) and temporal relation (e.g., one identical sample in neighbouring training epochs) into one high-dimensional topological complex. Such spatio-temporal complex can be used to efficiently train one visualization model to accurately project and inverse-project any high and low dimensional data across epochs. Our extensive experiment shows that, in comparison to DVI, TimeVis not only is more accurate to preserve the visualized time-travelling semantics, but 15X faster in visualization efficiency, achieving a new state-of-the-art in time-travelling visualization.

Bug datasets lay significant empirical and experimental foundation for various SE/PL researches such as fault localization, software testing, and program repair. Current well-known datasets are constructed manually, which inevitably limits their scalability, representativeness, and the support for the emerging data-driven research.

Browser extensions have emerged as integrated characteristics in modern browsers, with the aim to boost the online browsing experience. Their advantageous position between a user and the Internet endows them with easy access to the user’s sensitive data, which has raised mounting privacy concerns from both legislators and extension users. In this work, we propose an end-to-end approach to automatically diagnosing the privacy compliance violations among extensions. It analyzes the compliance of privacy policy versus regulation requirements and their actual privacy-related practices during runtime. This approach can serve the extension users, developers and store operators as an efficient and practical detection mechanism for privacy compliance violations.

Trained with a sufficiently large training and testing dataset, Deep Neural Networks (DNNs) are expected to generalize. However, inputs may deviate from the training dataset distribution in real deployments. This is a fundamental issue with using a finite dataset, which may lead deployed DNNs to mis-predict in production.

WPA (Wi-Fi Protected Access) Enterprise is the de facto standard for safeguarding enterprise-level wireless networks. It relies on Transport Layer Security (TLS) to establish a secure tunnel during its authentication process, and thus the notoriously error-prone certificate validation may haunt it. Incorrect validation may lead to the SSL/TLS man-in-the-middle attack, or the evil twin attack in the context of wireless networking, where the supplicant connects and unwittingly sends authentication credentials to a fake access point.

Deep metric learning (DML) learns a generalizable embedding space where the representations of semantically similar samples are closer. Despite achieving good performance, the state-of-the-art models still suffer from the generalization errors such as farther similar samples and closer dissimilar samples in the space. In this work, we design an empirical influence function (EIF), a debugging and explaining technique for the generalization errors of state-of-the-art metric learning models. EIF is designed to efficiently identify and quantify how a subset of training samples contributes to the generalization errors. Moreover, given a user-specific error, EIF can be used to relabel a potentially noisy training sample as mitigation. In our quantitative experiment, EIF outperforms the traditional baseline in identifying more relevant training samples with statistical significance and 33.5% less time. In the field study on well-known datasets such as CUB200, CARS196, and InShop, EIF identifies 4.4%, 6.6%, and 17.7% labelling mistakes, indicating the direction of the DML community to further improve the model performance. Our code is available at https://github.com/lindsey98/Influencefunctionmetric_learning.

In this work, we introduce a tool, RegMiner, to automate the process of collecting replicable regression bugs from a set of Git repositories. In the code commit history, RegMiner searches for regressions where a test can pass a regression-fixing commit, fail a regressioninducing commit, and pass a previous working commit again. Technically, RegMiner (1) identifies potential regression-fixing commits from the code evolution history, (2) migrates the test and its code dependencies in the commit over the history, and (3) minimizes the compilation overhead during the regression search. Our experients show that RegMiner can successfully collect 1035 regressions over 147 projects in 8 weeks, creating the largest replicable regression dataset within the shortest period, to the best of our knowledge. In addition, our experiments further show that (1) RegMiner can construct the regression dataset with very high precision and acceptable recall, and (2) the constructed regression dataset is of high authenticity and diversity. The source code of RegMiner is available at https://github.com/SongXueZhi/RegMiner, the mined regression dataset is available at https://regminer.github.io/, and the demonstration video is available at https://youtu.be/yzcM9Y4unok.

Automated model repair techniques enable machines to synthesise patches that ensure models meet given requirements. B-repair, which is an existing model repair approach, assists users in repairing erroneous models in the B formal method, but repairing large models is inefficient due to successive applications of repair. In this work, we improve the performance of B-repair using simultaneous modifications, repair refactoring, and better classifiers. The simultaneous modifications can eliminate multiple invariant violations at a time so the average time to repair each fault can be reduced. Further, the modifications can be refactored to reduce the length of repair. The purpose of using better classifiers is to perform more accurate and general repairs and avoid inefficient brute-force searches. We conducted an empirical study to demonstrate that the improved implementation leads to the entire model process achieving higher accuracy, generality, and efficiency.

Although deep learning has demonstrated astonishing performance in many applications, there are still concerns about its dependability. One desirable property of deep learning applications with societal impact is fairness (i.e., non-discrimination). Unfortunately, discrimination might be intrinsically embedded into the models due to the discrimination in the training data. As a countermeasure, fairness testing systemically identifies discriminatory samples, which can be used to retrain the model and improve the model’s fairness. Existing fairness testing approaches however have two major limitations. First, they only work well on traditional machine learning models and have poor performance (e.g., effectiveness and efficiency) on deep learning models. Second, they only work on simple structured (e.g., tabular) data and are not applicable for domains such as text. In this work, we bridge the gap by proposing a scalable and effective approach for systematically searching for discriminatory samples while extending existing fairness testing approaches to address a more challenging domain, i.e., text classification. Compared with state-of-the-art methods, our approach only employs lightweight procedures like gradient computation and clustering, which is significantly more scalable and effective. Experimental results show that on average, our approach explores the search space much more effectively (9.62 and 2.38 times more than the state-of-the-art methods respectively on tabular and text datasets) and generates much more discriminatory samples (24.95 and 2.68 times) within a same reasonable time. Moreover, the retrained models reduce discrimination by 57.2 and 60.2 percent respectively on average.

The widespread adoption of Deep Neural Networks (DNNs) in important domains raises questions about the trustworthiness of DNN outputs. Even a highly accurate DNN will make mistakes some of the time, and in settings like self-driving vehicles these mistakes must be quickly detected and properly dealt with in deployment. Just as our community has developed effective techniques and mechanisms to monitor and check programmed components, we believe it is now necessary to do the same for DNNs. In this paper we present DNN self-checking as a process by which internal DNN layer features are used to check DNN predictions. We detail SelfChecker, a self-checking system that monitors DNN outputs and triggers an alarm if the internal layer features of the model are inconsistent with the final prediction. SelfChecker also provides advice in the form of an alternative prediction. We evaluated SelfChecker on four popular image datasets and three DNN models and found that SelfChecker triggers correct alarms on 60.56% of wrong DNN predictions, and false alarms on 2.04% of correct DNN predictions. This is a substantial improvement over prior work (SelfOracle, Dissector, and ConfidNet). In experiments with self-driving car scenarios, SelfChecker triggers more correct alarms than SelfOracle for two DNN models (DAVE-2 and Chauffeur) with comparable false alarms. Our implementation is available as open source.

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.

Fuzzing has been a widely-used technique for discovering software vulnerabilities. Many existing fuzzers leverage coverage-feedback to evolve seeds to maximize (optimize) program branch coverage. Recently, some techniques propose to train deep learning models to predict the branch coverage of an arbitrary input. Those techniques have proved their success in improving coverage and discovering bugs under different experimental settings. However, deep learning models, usually as a black magic box, are notoriously lack of explanation. Moreover, their performance can be sensitive to the collected runtime coverage information for training, indicating potentially unstable performance. To this end, in this work we conduct a systematic and extensive empirical study on 4 types of deep learning models across 6 projects to reproduce the actual performance of deep learning fuzzers, analyze the advantages and disadvantages of deep learning in the process of fuzzing applications, and explore the future direction of the combination of the two. Our empirical results reveal that the deep learning models can only be effective in very limited scenarios, which is largely restrained by training data imbalance, dependant labels, model over-generalization, and the insufficient expressiveness of the state-of-the-art models. Consequently, the estimated gradients by the models to cover a branch can be less helpful in many scenarios.

Search-based software testing (SBST) generates tests using search algorithms guided by measurements gauging how far a test case is away from exercising a coverage goal. The effectiveness of SBST largely depends on the continuity and monotonicity of the fitness landscape decided by these measurements and the search operators. Unfortunately, the fitness landscape is challenging when the function under test takes object inputs, as classical measurement hardly provide guidance for constructing legitimate object inputs. To overcome this problem, we propose test seeds, i.e., test code skeletons of legitimate objects which enable the use of classical measurements. Given a target branch in a function under test, we first statically analyze the function to build an object construction graph that captures the relation between the operands of the target method and the states of their relevant object inputs. Based on the graph, we synthesize test template code where each "slot" is a mutation point for the search algorithm. This approach can be seamlessly integrated with existing SBST algorithms, and we implemented EvoObj on top of EvoSuite. Our experiments show that EvoObj outperforms EvoSuite with statistical significance on 2750 methods over 103 open source Java projects using state-of-the-art SBST algorithms.

The website fingerprinting (or inter-domain WSF), enhanced by various machine learning techniques, has shown its power to identify websites a user has visited. To our best knowledge, a finer-grained problem of web page fingerprinting (or intra-domain WPF) has not been systematically studied by our research community. The WPF attackers, such as government agencies enforcing Internet censorship, are keen to identify the particular web pages (e.g., a political dissident’s social media page) visited by the target user.

This work follow the verification as planning paradigm and propose to use model-checking techniques to solve planning and goal reasoning problems for autonomous systems with high-degree of assurance. It presents a novel modelling framework — Goal Task Network (GTN) that encompass both goal reasoning and planning under a unified formal description that enables the use of assurance tools. The paper provides a systematic method that highlights how an industrial model checker (PAT) can be used to solve goal reasoning and planning problems modelled by GTNs. Further, this paper also introduces the design of an automated system framework for Goal Reasoning And Verification for Independent Trusted Autonomous Systems (GRAVITAS). The proposed framework is demonstrated in an experiment that simulates a survey mission performed by the REMUS-100 autonomous underwater vehicle.

Adversarial Examples threaten to fool deep learning models to output erroneous predictions with high confidence. Optimization-based methods for constructing such samples have been extensively studied. While being effective in terms of aggression, they typically lack clear interpretation and constraint about their underlying generation process, which thus hinders us from leveraging the produced adversarial samples for model protection in the reverse direction. Hence, we expect them to repair bugs in the pre-trained models by produced additional training data equipped with strong attack ability rather than time-consuming full re-training from scratch. To address these issues, we first study the black-box behaviors and the intrinsic deficiency of neighborhood information in previous optimization-based adversarial attacks and defenses, respectively. Then we introduce a new method dubbed FeaCP, which uses correct predicted samples in disjoint classes to guide the generation of more explainable adversarial samples in the ambiguous region around the decision boundary instead of uncontrolled “blind spots”, via convex combination in a feature component-wise manner which takes the individual importance of feature ingredients into account. Our method incorporates the prior fact that for well-separated samples, the path connecting them would go through model's decision-boundary that lies in a low-density region, however, wherein adversarial examples are spread with high probability, thus having an impact on the ultimate trained model. In our work, the path is constructed by proposed inhomogeneous feature-wise convex interpolation rather than operating on sample-wise level, limiting the search space of FeaCP to obtain an adaptive neighborhood. Finally, we provide detailed insights and extend our method to adversarial fine-tuning using vicinity distribution to optimize the approximated decision boundary, and validate the significance of our FeaCP to model performance. The experimental results show that our method provides competitive performance on various datasets and networks.

A key feature of the booming smart home is the integration of a wide assortment of technologies, including various standards, proprietary communication protocols and heterogeneous platforms. Due to customization, unsatisfied assumptions and incompatibility in the integration, critical security vulnerabilities are likely to be introduced by the integration. Hence, this work addresses the security problems in smart home systems from anintegrationperspective, as a complement to numerous studies that focus on the analysis of individual techniques. We propose HomeScan, an approach that examines the security of the implementations of smart home systems. It extracts the abstract specification of application-layer protocols and internal behaviors of entities, so that it is able to conduct an end-to-end security analysis against various attack models. Applying HomeScanon three extensively-used smart home systems, we have found twelve non-trivial security issues, which may lead to unauthorized remote control and credential leakage.

Regression faults, which make working code stop functioning, are often introduced when developers make changes to the software. Many regression fault localization techniques have been proposed. However, issues like inaccuracy and lack of explanation are still obstacles for their practical application. In this work, we propose a trace-based approach to identifying not only where the root cause of a regression bug lies, but also how the defect is propagated to its manifestation as the explanation. In our approach, we keep the trace of original correct version as reference and infer the faulty steps on the trace of regression version so that we can build a causality graph of how the defect is propagated. To this end, we overcomes two technical challenges. First, we align two traces derived from two program versions by extending state-of-the-art trace alignment technique for regression fault with novel relaxation technique. Second, we construct causality graph (i.e., explanation) by adopting a technique calledalignment slicing and mendingto isolate the failure-inducing changes and explain the failure. Our comparative experiment with the state-of-the-art techniques including dynamic slicing, delta-debugging, and symbolic execution on 24 real-world regressions shows that (1) our approach is more accurate on isolating the failure-inducing changes, (2) the generated explanation requires acceptable manual effort to inspect, and (3) our approach requires lower runtime overhead. In addition, we also conduct an applicability experiment based on Defects4J bug repository, showing the potential limitations of our trace-based approach and providing guidance for its practical use.

Decision Making forms the basis of any successful athlete's career. The importance of making the right decision at crucial junctures during a game is eventually the difference between winning or losing a match. Team sports have an important characteristic in that they are usually a set of non-discrete events and a good decision by one athlete, doesn't necessarily lead to a reward. It is a sequence of good decisions that finally lead to the reward, which explains why goals are usually so rare in a game of Soccer. Through this paper, we explore Soccer and look at the number of possibilities that are available at any given time to a player and what is their best possible action. We propose a Model-driven Domain specific Sequential model that aims to predict the best possible action that can be taken by a Soccer Athlete (player), to maximize the probability of scoring a goal.

Reflection is a notion that naturally emerges from philosophy, mathematics, and sciences. In short, reflection is the ability of an entity to alter its own behaviour. This paper suggests that reflection is crucial to the development of complex and trustworthy software systems. We present RL, a reflective computational model that aims to support the development of a large-scale framework for modelling and manipulating structured data. We give the formal semantics for this computational model. We also share preliminary work on a proof-of-concept implementation of RL and discuss future work.

Deep neural networks (DNN) are increasingly applied in safety-critical systems, e.g., for face recognition, autonomous car control and malware detection. It is also shown that DNNs are subject to attacks such as adversarial perturbation and thus must be properly tested. Many coverage criteria for DNN since have been proposed, inspired by the success of code coverage criteria for software programs. The expectation is that if a DNN is well tested (and retrained) according to such coverage criteria, it is more likely to be robust. In this work, we conduct an empirical study to evaluate the relationship between coverage, robustness and attack/defense metrics for DNN. Our study is the largest to date and systematically done based on 100 DNN models and 25 metrics. One of our findings is that there is limited correlation between coverage and robustness, i.e., improving coverage does not help improve the robustness. Our dataset and implementation have been made available to serve as a benchmark for future studies on testing DNN.

We are in the era that sport is increasingly defined by data. Rich data is a powerful enabling foundation for novel insights on the game and on player actions, and consequently used for fan engagement and better decision making. Detailed data that has specifications of each shot is currently missing in tennis, as the game dynamics is fast and it is beyond human ability to manually record all specifications of each and every shot, even using scoring software. In this paper, we present an intelligent system to automatically recognize player actions, ball and player movements, and important game events. The system annotates the video with a suitable set of keywords for fast retrieval in broadcast production. Various techniques of computer vision, alignment, filtering, and pre-trained deep learning models are utilized by our system. The evaluation of our results on multiple broadcast videos show great accuracy and timeliness. The implications of the work presented in this paper are profound in the current workflow in broadcast coverage of a tennis match where normally multiple video operators and judges are needed to identify events and retrieve the related clips from multiple cameras.

Although deep neural networks (DNNs) have demonstrated astonishing performance in many applications, there are still concerns on their dependability. One desirable property of DNN for applications with societal impact is fairness (i.e., non-discrimination). In this work, we propose a scalable approach for searching individual discriminatory instances of DNN. Compared with state-of-the-art methods, our approach only employs lightweight procedures like gradient computation and clustering, which makes it significantly more scalable than existing methods. Experimental results show that our approach explores the search space more effectively (9 times) and generates much more individual discriminatory instances (25 times) using much less time (half to 1/7).

In Search-based Software Testing (SBST), test generation is guided by fitness functions that estimate how close a test case is to reach an uncovered test goal (e.g., branch). A popular fitness function estimates how close conditional statements are to evaluating to true or false, i.e., the branch distance. However, when conditions read Boolean variables (e.g., if(x && y)), the branch distance provides no gradient for the search, since a Boolean can either be true or false. This flag problem can be addressed by transforming individual procedures such that Boolean flags are replaced with numeric comparisons that provide better guidance for the search. Unfortunately, defining a semantics-preserving transformation that is applicable in an interprocedural case, where Boolean flags are passed around as parameters and return values, is a daunting task. Thus, it is not yet supported by modern test generators.

Neural networks are becoming a popular tool for solving many real-world problems such as object recognition and machine translation, thanks to its exceptional performance as an end-to-end solution. However, neural networks are complex black-box models, which hinders humans from interpreting and consequently trusting them in making critical decisions. Towards interpreting neural networks, several approaches have been proposed to extract simple deterministic models from neural networks. The results are not encouraging (e.g., low accuracy and limited scalability), fundamentally due to the limited expressiveness of such simple models.

Service composition aims at achieving a business goal by composing existing service-based applications or components. The response time of a service is crucial, especially in time-critical business environments, which is often stated as a clause in service-level agreements between service providers and service users. To meet the guaranteed response time requirement of a composite service, it is important to select a feasible set of component services such that their response time will collectively satisfy the response time requirement of the composite service. In this work, we use the BPEL modeling language that aims at specifying Web services. We extend it with timing parameters and equip it with a formal semantics. Then, we propose a fully automated approach to synthesize the response time requirement of component services modeled using BPEL, in the form of a constraint on the local response times. The synthesized requirement will guarantee the satisfaction of the global response time requirement, statically or dynamically. We implemented our work into a tool, Selamat and performed several experiments to evaluate the validity of our approach.

A key feature of the booming smart home is the integration of a wide assortment of technologies, including various standards, proprietary communication protocols and heterogeneous platforms. Due to customization, unsatisfied assumptions and incompatibility in the integration, critical security vulnerabilities are likely to be introduced by the integration. Hence, this work addresses the security problems in smart home systems from an integration perspective, as a complement to numerous studies that focus on the analysis of individual techniques. We propose HOMESCAN, an approach that examines the security of the implementations of smart home systems. It extracts the abstract specification of application-layer protocols and internal behaviors of participants, so that it is able to conduct an end-to-end security analysis against various attack models. Applying HOMESCAN on three extensively-used smart home systems, we have found twelve non-trivial security vulnerabilities, which may lead to unauthorized remote control and credential leakage.

Blockchain technology relies on consensus algorithms to resolve conflicts in Byzantine environments. New blockchain algorithms are rapidly designed and implemented without a properly conducted formal analysis and verification. In this paper, we conducted a study on Tendermint which is a proof-of-stake consensus algorithm. We verified that the consensus protocol is deadlock-free and is able to reach consensus when at least 2/3 of the network is in agreement. We also proved that a minority set of nodes that compose more than 1/3 of the network is enough to censor the majority of the network and prevent the network from reaching consensus and conclude that the algorithm has some shortcomings on availability.

Dynamic slicing is a common way of identifying the root cause when a program fault is revealed. With the dynamic slicing technique, the programmers can follow data and control flow along the program execution trace to the root cause. However, the technique usually fails to work on omission bugs, i.e., the faults which are caused by missing executing some code. In many cases, dynamic slicing over-skips the root cause when an omission bug happens, leading the debugging process to a dead end. In this work, we conduct an empirical study on the omission bugs in the Defects4J bug repository. Our study shows that (1) omission bugs are prevalent (46.4%) among all the studied bugs; (2) there are repeating patterns on causes and fixes of the omission bugs; (3) the patterns of fixing omission bugs serve as a strong hint to break the slicing dead end. Based on our findings, we train a neural network model on the omission bugs in Defects4J repository to recommend where to approach when slicing can no long work. We conduct an experiment by applying our approach on 3193 mutated omission bugs which slicing fails to locate. The results show that our approach outperforms random benchmark on breaking the dead end and localizing the mutated omission bugs (63.8% over 2.8%).

Abstract CSP# (communicating sequential programs) is a modelling language designed for specifying concurrent systems by integrating CSP-like compositional operators with sequential programs updating shared variables. In this work, we define an observation-oriented denotational semantics in an open environment for the CSP# language based on the UTP framework. To deal with shared variables, we lift traditional event-based traces into mixed traces which consist of state-event pairs for recording process behaviours. To capture all possible concurrency behaviours between action/channel-based communications and global shared variables, we construct a comprehensive set of rules on merging traces from processes which run in parallel/interleaving. We also define refinement to check process equivalence and present a set of algebraic laws which are established based on our denotational semantics. We further encode our proposed denotational semantics into the PVS theorem prover. The encoding not only ensures the semantic consistency, but also builds up a theoretic foundation for machine-assisted verification of CSP# specifications.

Nowadays, protocols often use time to provide better security. For instance, critical credentials are often associated with expiry dates in system designs. However, using time correctly in protocol design is challenging, due to the lack of time related formal specification and verification techniques. Thus, we propose a comprehensive analysis framework to formally specify as well as automatically verify timed security protocols. A parameterized method is introduced in our framework to handle timing parameters whose values cannot be decided in the protocol design stage. In this work, we first propose timed applied p-calculus as a formal language for specifying timed security protocols. It supports modeling of continuous time as well as application of cryptographic functions. Then, we define its formal semantics based on timed logic rules, which facilitates efficient verification against various authentication and secrecy properties. Given a parameterized security protocol, our method either produces a constraint on the timing parameters which guarantees the security property satisfied by the protocol, or reports an attack that works for any parameter value. The correctness of our verification algorithm has been formally proved. We evaluate our framework with multiple timed and untimed security protocols and successfully find a previously unknown timing attack in Kerberos V.

As feature-rich Android applications (apps for short) are increasingly popularized in security-sensitive scenarios, methods to verify their security properties are highly desirable. Existing approaches on verifying Android apps often have limited effectiveness. For instance, static analysis often suffers from a high false-positive rate, whereas approaches based on dynamic testing are limited in coverage. In this work, we propose an alternative approach, which is to apply the software model checking technique to verify Android apps. We have built a general framework named DroidPF upon Java PathFinder (JPF), towards model checking Android apps. In the framework, we craft an executable mock-up Android OS which enables JPF to dynamically explore the concrete state spaces of the tested apps; we construct programs to generate user interaction and environmental input so as to drive the dynamic execution of the apps; and we introduce Android specific reduction techniques to help alleviate the state space explosion. DroidPF focuses on common security vulnerabilities in Android apps including sensitive data leakage involving a non-trivial flow- and context-sensitive taint-style analysis. DroidPF has been evaluated with 131 apps, which include real-world apps, third-party libraries, malware samples and benchmarks for evaluating app analysis techniques like ours. DroidPF precisely identifies nearly all of the previously known security issues and nine previously unreported vulnerabilities/bugs.

Decision making seeks the optimal choice for maximum rewards or minimal costs under certain conditions, requirements and constraints. Decision making problems in practice are usually complicated as they may be partially observable, stochastic, and dynamic. Such complexities make the traditional decision making methods like mathematical programming difficult to find the optimal choices effectively and efficiently. In this work, we conduct a case study with the 4-player Kuhn Poker game by combining machine learning with probabilistic model checking to generate optimal decisions. Experimental results show that the agent employing our method outperforms the conservative and bluffing players regardless of the positions of players.

Software debugging has long been regarded as a time and effort consuming task. In the process of debugging, developers usually need to manually inspect many program steps to see whether they deviate from their intended behaviors. Given that intended behaviors usually exist nowhere but in human mind, the automation of debugging turns out to be extremely hard, if not impossible. In this work, we propose a feedback-based debugging approach, which (1) builds on light-weight human feedbacks on a buggy program and (2) regards the feedbacks as partial program specification to infer suspicious steps of the buggy execution. Given a buggy program, we record its execution trace and allow developers to provide light-weight feedback on trace steps. Based on the feedbacks, we recommend suspicious steps on the trace. Moreover, our approach can further learn and approximate bug-free paths, which helps reduce required feedbacks to expedite the debugging process. We conduct an experiment to evaluate our approach with simulated feedbacks on 3409 mutated bugs across 3 open source projects. The results show that our feedback-based approach can detect 92.8% of the bugs and 65% of the detected bugs require less than 20 feedbacks. In addition, we implement our proof-of-concept tool, Microbat, and conduct a user study involving 16 participants on 3 debugging tasks. The results show that, compared to the participants using the baseline tool, Whyline, the ones using Microbat can spend on average 55.8% less time to locate the bugs.

In this paper, we propose an approach to detecting project-specific recurring designs in code base and abstracting them into design templates as reuse opportunities. The mined templates allow programmers to make further customization for generating new code. The generated code involves the code skeleton of recurring design as well as the semi-implemented code bodies annotated with comments to remind programmers of necessary modification. We implemented our approach as an Eclipse plugin called MICoDe. We evaluated our approach with a reuse simulation experiment and a user study involving 16 participants. The results of our simulation experiment on 10 open source Java projects show that, to create a new similar feature with a design template, (1) on average 69% of the elements in the template can be reused and (2) on average 60% code of the new feature can be adopted from the template. Our user study further shows that, compared to the participants adopting the copy-paste-modify strategy, the ones using MICoDe are more effective to understand a big design picture and more efficient to accomplish the code reuse task.

A BAR system specifies a cooperation between agents who can be altruistic when they follow the specified behaviours, Byzantine when they randomly deviate from specifications and rational when they deviate to increase their own benefits. We consider whether a rational agent indeed follows the specification of a probabilistic BAR system as verifying whether the system is a Nash-equilibrium in the corresponding stochastic games. In this article, we propose an intuitive specification for probabilistic BAR systems and an algorithm to automatically verify Nash-equilibrium. To validate our implementation of the algorithm, we present two case studies – the three-player Rock-paper-scissors game and a probabilistic secret sharing protocol.

The heavy use of event-callback mechanism in frameworks like Android causes challenges for static analysis. Modelling of callback mechanisms for Android applications (app for short) is becoming a major method to address such challenges. In this work, we aim to construct a generic callback-related model that supports path-sensitive analysis. We consider three unresolved challenges in the existing modelling approaches: 1) building connections between different components; 2) identifying path-sensitive conditions; 3) handling the system-driven callbacks and fine-grained lifecycle callbacks. We propose algorithms for constructing a generic path-sensitive callback model and present a prototype model constructor, AndroChecker, to validate our approach. We evaluate 20 real-world apps using AndroChecker. The evaluation result shows that our method and tool have a strong capability in modelling path conditions and inter-component invocations.

Concurrent Programs are hard to analyze or debug due to the complex program logic and unpredictable execution environment. In practice, ordinary programmers often adopt existing well-designed concurrency related API (e.g., those in java.util.concurrent) so as to avoid dealing with these issues. These API can however often be used incorrectly, which results in hardto-debug concurrent bugs. In this work, we propose an approach for enforcing the correct usage of concurrency-related Java API. Our idea is to annotate concurrency-related Java classes with annotations related to misuse of these API and develop lightweight type checker to detect concurrent API misuse based on the annotations. To automate this process, we need to solve two problems: (1) how do we obtain annotations of the relevant API; and (2) how do we systematically detect concurrent API misuse based on the annotations? We solve the first problem by extracting annotations from the API documentation using natural language processing techniques. We solve the second problem by implementing our type checkers in the Checker Framework to detect concurrent API misuse. We apply our approach to extract annotations for all classes in the Java standard library and use them to detect concurrent API misuse in open source projects on GitHub. We confirm that concurrent API misuse is common and often results in bugs or inefficiency.

Use cases are widely used to capture user requirements based on interactions between different roles in the system. They are mostly documented in natural language and sometimes aided with graphical illustrations in the form of use case diagrams. Use cases serve as an important means to communicate among stakeholders, requirement engineers and system engineers as they are easy to understand and are produced early in the software development process. Having high quality use cases are beneficial in many ways, e.g., in avoiding inconsistency/incompleteness in requirements, in guiding system design, in generating test cases. In this work, we propose an approach to improve the quality of use cases using techniques including natural language processing and machine learning. The central idea is to discover potential problems in use cases through active learning and human interaction and provide feedbacks in natural language. We conduct user studies with a real-world use case document. The results show that our method is helpful in improving use cases with a reasonable amount of user interaction.

Recently, many large enterprises (e.g., Netflix, Amazon) have decomposed their monolithic application into services, and composed them to fulfill their business functionalities. Many hosting services on the cloud, with different Quality of Service (QoS) (e.g., availability, cost), can be used to host the services. This is an example of competing services. QoS is crucial for the satisfaction of users. It is important to choose a set of services that maximize the overall QoS, and satisfy all QoS requirements for the service composition. This problem, known as optimal service selection, is NP-hard. Therefore, an effective method for reducing the search space and guiding the search process is highly desirable. To this end, we introduce a novel technique, called Probabilistic Hierarchical Refinement (ProHR). ProHR effectively reduces the search space by removing competing services that cannot be part of the selection. ProHR provides two methods, probabilistic ranking and hierarchical refinement, that enable smart exploration of the reduced search space. Unlike existing approaches that perform poorly when QoS requirements become stricter, ProHR maintains high performance and accuracy, independent of the strictness of the QoS requirements. ProHR has been evaluated on a publicly available dataset, and has shown significant improvement over existing approaches.

No abstract available.

No abstract available.

Security of authentication protocols heavily relies on the confidentiality of credentials (or authenticators) like passwords and session IDs. However, unlike browser-based web applications for which highly evolved browsers manage the authenticators, Android apps have to construct their own management. We find that most apps simply locate their authenticators into the persistent storage and entrust underlying Android OS for mediation. Consequently, these authenticators can be leaked through compromised backup channels. In this work, we conduct the first systematic investigation on this previously overlooked attack vector. We find that nearly all backup apps on Google Play inadvertently expose backup data to any app with internet and SD card permissions. With this exposure, the malicious apps can steal other apps' authenticators and obtain complete control over the authenticated sessions. We show that this can be stealthily and efficiently done by building a proof-of-concept app named AuthSniffer. We find that 80 (68.4%) out of the 117 tested top-ranked apps which have implemented authentication schemes are subject to this threat. Our study should raise the awareness of app developers and protocol analysts about this attack vector.

The advance of analytics technology has attracted more attention and adoption from sports, although modeling and analyzing the dynamic (and uncertain) behaviors of sports are challenging. Formal methods have been strongly recommended to deal with complex systems by their rigorous semantics and powerful reasoning capabilities. In this paper, we present our initiative as the first to apply probabilistic model checking techniques to strategy analytics for tennis based on Markov Decision Processes (MDP). Our approach can derive insights such as prediction of winning chances and identification of best improvement. We evaluate the effectiveness of our approach through real-life case study.

As the boom of social networking, Single Sign-On (SSO) services developed by major commercial service providers like Facebook, Google and Twitter, have been widely used by web-based service providers as an alternative authentication scheme. Despite rich research has focused on browser-based web applications, little has been conducted on the implementation of SSO on mobile platforms. However, we reveal that due to the fundamental difference of isolation mechanism in mobile OS and applications from the origin-based isolation in browsers, the SSO encounters a novel attack surface and adversarial models. We perform the first formal analysis on the implementation of the most widely used SSO service -- Facebook Login. Our study takes as input the available implementation and dynamic execution traces of Facebook SDK for Android, from which we abstract the implementation-level protocol. The protocol is then modeled in typed Pi-calculus, and automatically checked against the mobile platform specific attack models in a protocol verifier Proverif. Our study has successfully identified a major vulnerability, which allows an attacker to steal authentication credentials from victims and log into their Facebook accounts.

Distributed systems like cloud-based services are ever more popular. Assessing the reliability of distributed systems is highly non-trivial. Particularly, the order of executions among distributed components adds a dimension of non-determinism, which invalidates existing reliability assessment methods based on Markov chains. Probabilistic model checking based on models like Markov decision processes is designed to deal with scenarios involving both probabilistic behavior (e.g., reliabilities of system components) and non-determinism. However, its application is currently limited by state space explosion, which makes reliability assessment of distributed system particularly difficult. In this work, we improve the probabilistic model checking through a method of abstraction and reduction, which controls the communications among system components and actively reduces the size of each component. We prove the soundness and completeness of the proposed approach. Through an implementation in a software toolkit and evaluations with several systems, we show that our approach often reduces the size of the state space by several orders of magnitude, while still producing sound and accurate assessment.

Software that support various groups of customers usually require complicated configurations to attain different functionalities. To model the configuration options, feature model is proposed to capture the commonalities and competing variabilities of the product variants in software family or Software Product Line (SPL). A key challenge for deriving a new product is to find a set of features that do not have inconsistencies or conflicts, yet optimize multiple objectives (e.g., minimizing cost and maximizing number of features), which are often competing with each other. Existing works have attempted to make use of evolutionary algorithms (EAs) to address this problem. In this work, we incorporated a novel feedback-directed mechanism into existing EAs. Our empirical results have shown that our method has improved noticeably over all unguided version of EAs on the optimal feature selection. In particular, for case studies in SPLOT and LVAT repositories, the feedback-directed Indicator-Based EA (IBEA) has increased the number of correct solutions found by 72.33% and 75%, compared to unguided IBEA. In addition, by leveraging a pre-computed solution, we have found 34 sound solutions for Linux X86, which contains 6888 features, in less than 40 seconds.

Model checking suffers from the state space explosion problem. Compositional verification techniques such as assume-guarantee reasoning (AGR) have been proposed to alleviate the problem. However, there are at least three challenges in applying AGR. Firstly, given a system M1 ? M2, how do we automatically construct and refine (in the presence of spurious counterexamples) an assumption A2, which must be an abstraction of M2? Previous approaches suggest to incrementally learn and modify the assumption through multiple invocations of a model checker, which could be often time consuming. Secondly, how do we keep the state space small when checking M1 ? A2 = f if multiple refinements of A2 are necessary? Lastly, in the presence of multiple parallel components, how do we partition the components? In this work, we propose interpolation-guided compositional verification. The idea is to tackle three challenges by using interpolations to generate and refine the abstraction of M2, to abstract M1 at the same time (so that the state space is reduced even if A2 is refined all the way to M2), and to find good partitions. Experimental results show that the proposed approach outperforms existing approaches consistently.

The analysis of software architecture plays an important role in understanding the system structures and facilitate proper implementation of user requirements. Despite its importance in the software engineering practice, the lack of formal description and verification support in this domain hinders the development of quality architectural models. To tackle this problem, in this work, we develop an approach for modeling and verifying software architectures specified using Monterey Phoenix (MP) architecture description language. MP is capable of modeling system and environment behaviors based on event traces, as well as supporting different architecture composition operations and views. First, we formalize the syntax and operational semantics for MP; therefore, formal verification of MP models is feasible. Second, we extend MP to support shared variables and stochastic characteristics, which not only increases the expressiveness of MP, but also widens the properties MP can check, such as quantitative requirements. Third, a dedicated model checker for MP has been implemented, so that automatic verification of MP models is supported. Finally, several experiments are conducted to evaluate the applicability and efficiency of our approach.

Model checking has been pervasive and successful in finding bugs in hardware and software systems, including real-time and probabilistic systems. Applying model checking to decision making is relative new and has an excellent potential to be compliment to data analytics and other Artificial Intelligent (AI) or Operational Research (OR) based decision making techniques. Our last 8 years research has focused on the development of PAT (Process Analysis Toolkit) [18] whichsupports modelling languages that combine the expressiveness of event, state, time and probability based modeling techniques to which model checking can be directly applied. The next direction for PAT is to move from verification to analytics, we call it "Event Analytics" with a special focus on "Strategy Analytics".

Zeno runs, where infinitely many actions occur within finite time, may arise in Timed Automata models. Zeno runs are not feasible in reality and must be pruned during system verification. Thus it is necessary to check whether a run is Zeno or not so as to avoid presenting Zeno runs as counterexamples during model checking. Existing approaches on non-Zenoness checking include either introducing an additional clock in the Timed Automata models or additional accepting states in the zone graphs. In addition, there are approaches proposed for alternative timed modeling languages, which could be generalized to Timed Automata. In this work, we investigate the problem of non-Zenoness checking in the context of model checking LTL properties, not only evaluating and comparing existing approaches but also proposing a new method. To have a systematic evaluation, we develop a software toolkit to support multiple non-Zenoness checking algorithms. The experimental results show the effectiveness of our newly proposed algorithm, and demonstrate the strengths and weaknesses of different approaches.

In this paper, we describe our analysis of a recently proposed electric vehicle charing protocol. The protocol builds on complicated cryptographic primitives such as commitment, zero-knowledge proofs, BBS+ signature and etc. Moreover, interesting properties such as secrecy, authentication, anonymity, and location privacy are claimed on this protocol. It thus presents a challenge for formal verification, as existing tools for security protocol analysis lack support for all the required features. In our analysis, we employ and combine the strength of two state-of-the-art symbolic verifiers, Tamarin and Prove if, to check all important properties of the protocol.

Code clones have to be made explicit and be managed in software maintenance. Researchers have developed many clone detection tools to detect and analyze code clones in software systems. These tools report code clones as similar code fragments in source files. However, clone-related maintenance tasks (e.g., refactorings) often involve a group of code clones appearing in larger syntactic context (e.g., code clones in sibling classes or code clones calling similar methods). Given a list of low-level code-fragment clones, developers have to manually summarize from bottom up low-level code clones that are relevant to the syntactic context of a maintenance task. In this paper, we present a clone summarization technique to summarize code clones with respect to their common syntactic context. The clone summarization allows developers to locate and maintain code clones in a top-down manner by type hierarchy and usage dependencies. We have implemented our approach in the Clonepedia tool and conducted a user study on JHotDraw with 16 developers. Our results show that Clonepedia users can better locate and refactor code clones, compared with developers using the Clone Detective tool.

Use cases, as the primary techniques in the user requirement analysis, have been widely adopted in the requirement engineering practice. As developed early, use cases also serve as the basis for function requirement development, system design and testing. Errors in the use cases could potentially lead to problems in the system design or implementation. It is thus highly desirable to detect errors in use cases. Automatically analyzing use case documents is challenging primarily because they are written in natural languages. In this work, we aim to achieve automatic defect detection in use case documents by leveraging on advanced parsing techniques. In our approach, we first parse the use case document using dependency parsing techniques. The parsing results of each use case are further processed to form an activity diagram. Lastly, we perform defect detection on the activity diagrams. To evaluate our approach, we have conducted experiments on 200+ real-world as well as academic use cases. The results show the effectiveness of our method.

Non-determinism in concurrent or distributed software systems (i.e., various possible execution orders among different distributed components) presents new challenges to the existing reliability analysis methods based on Markov chains. In this work, we present a toolkit RaPiD for the reliability analysis of non-deterministic systems. Taking Markov decision process as reliability model, RaPiD can help in the analysis of three fundamental and rewarding aspects regarding software reliability. First, to have reliability assurance on a system, RaPiD can synthesize the overall system reliability given the reliability values of system components. Second, given a requirement on the overall system reliability, RaPiD can distribute the reliability requirement to each component. Lastly, RaPiD can identify the component that affects the system reliability most significantly. RaPiD has been applied to analyze several real-world systems including a financial stock trading system, a proton therapy control system and an ambient assisted living room system.

Service composition uses existing service-based applications as components to achieve a business goal. The composite service operates in a highly dynamic environment; hence, it can fail at any time due to the failure of component services. Service composition languages such as BPEL provide a compensation mechanism to rollback the error. But such a compensation mechanism has several issues. For instance, it cannot guarantee the functional properties of the composite service after compensation. In this work, we propose an automated approach based on a genetic algorithm to calculate the recovery plan that could guarantee the satisfaction of functional properties of the composite service after recovery. Given a composite service with large state space, the proposed method does not require exploring the full state space of the composite service; therefore, it allows efficient selection of recovery plan. In addition, the selection of recovery plans is based on their quality of service (QoS). A QoS-optimal recovery plan allows effective recovery from the state of failure. Our approach has been evaluated on real-world case studies, and has shown promising results.

Abstract Recently, a promising programming model calledOrchas been proposed to support a structured way of orchestrating distributed Web Services. Orc is intuitive because it offers concise constructors to manage concurrent communication, time-outs, priorities, failure of Web Services or communication and so forth. The semantics of Orc is precisely defined. However, there is noautomaticverification tool available to verify critical properties against Orc programs. Our goal is to verify the orchestration programs (written in Orc language) which invoke web services to achieve certain goals. To investigate this problem and build useful tools, we explore in two directions. Firstly, we define a Timed Automata semantics for the Orc language, which we prove is semantically equivalent to the operational semantics of Orc. Consequently, Timed Automata models are systematically constructed from Orc programs. The practical implication is that existing tool supports for Timed Automata, e.g., Uppaal, can be used to simulate and model check Orc programs. An experimental tool has been implemented to automate this approach. Secondly, we start with encoding the operational semantics of Orc language in Constraint Logic Programming (CLP), which allows a systematic translation from Orc to CLP. Powerful constraint solvers like CLP are then used to prove traditional safety properties and beyond, e.g., reachability, deadlock-freeness, lower or upper bound of a time interval, etc. Counterexamples are generated when properties are not satisfied. Furthermore, the stepwise execution traces can be automatically generated as the simulation steps. The two different approaches give an insight into the verification problem of Web Service orchestration. The Timed Automata approach has its merits in visualized simulation and efficient verification supported by the well developed tools. On the other hand, the CPL approach gives better expressiveness in both modeling and verification. The two approaches complement each other, which gives a complete solution for the simulation and verification of Computation Orchestration.

Classical workflow nets (WF-nets for short) are an important subclass of Petri nets that are widely used to model and analyze workflow systems. Soundness is a crucial property of workflow systems and guarantees that these systems are deadlock-free and bounded. Aalst et al. proved that the soundness problem is decidable for WF-nets and can be polynomially solvable for free-choice WF-nets. This paper proves that the soundness problem is PSPACE-hard for WF-nets. Furthermore, it is proven that the soundness problem is PSPACE-complete for bounded WF-nets. Based on the above conclusion, it is derived that the soundness problem is also PSPACE-complete for bounded WF-nets with reset or inhibitor arcs (ReWF-nets and InWF-nets for short, resp.). ReWF- and InWF-nets are two extensions to WF-nets and their soundness problems were proven by Aalst et al. to be undecidable. Additionally, we prove that the soundness problem is co-NP-hard for asymmetric-choice WF-nets that are a larger class and can model more cases of interaction and resource allocation than free-choice ones.

Compositional techniques such as assume-guarantee reasoning (AGR) can help to alleviate the state space explosion problem associated with model checking. However, compositional verification is difficult to be automated, especially for timed systems, because constructing appropriate assumptions for AGR usually requires human creativity and experience. To automate compositional verification of timed systems, we propose a compositional verification framework using a learning algorithm for automatic construction of timed assumptions for AGR. We prove the correctness and termination of the proposed learning-based framework, and experimental results show that our method performs significantly better than traditional monolithic timed model checking.

Model checking has established as an effective method for automatic system analysis and verification. It is making its way into many domains and methodologies. Applying model checking techniques to a new domain (which probably has its own dedicated modeling language) is, however, far from trivial. Translation-based approach works by translating domain specific languages into input languages of a model checker. Because the model checker is not designed for the domain (or equivalently, the language), translation-based approach is often ad hoc. Ideally, it is desirable to have an optimized model checker for each application domain. Implementing one with reasonable efficiency, however, requires years of dedicated efforts. In this tutorial, we will briefly survey a variety of model checking techniques. Then we will show how to develop a model checker for a language combining real-time and probabilistic features using the PAT (Process Analysis Toolkit) step-by-step, and show that it could take as short as a few weeks to develop your own model checker with reasonable efficiency. The PAT system is designed to facilitate development of customized model checkers. It has an extensible and modularized architecture to support new languages (and their operational semantics), new state reduction or abstraction techniques, new model checking algorithms, etc. Since its introduction 5 years ago, PAT has attracted more than 2500 registered users (from 500+ organisations in 60 countries) and has been applied to develop model checkers for 20 different languages.

Service composition makes use of existing service-based applications as components to achieve a business goal. In time critical business environments, the response time of a service is crucial, which is also reflected as a clause in service level agreements (SLAs) between service providers and service users. To allow the composite service to fulfill the response time requirement as promised, it is important to find a feasible set of component services, such that their response time could collectively allow the satisfaction of the response time of the composite service. In this work, we propose a fully automated approach to synthesize the response time requirement of component services, in the form of a constraint on the local response times, that guarantees the global response time requirement. Our approach is based on parameter synthesis techniques for real-time systems. It has been implemented and evaluated with real-world case studies.

Testing provides a probabilistic assurance of system correctness. In general, testing relies on the assumptions that the system under test is deterministic so that test cases can be sampled. However, a challenge arises when a system under test behaves non-deterministiclly in a dynamic operating environment because it will be unknown how to sample test cases.

The principle of least privilege requires that software components should be granted only necessary privileges, so that compromising one component does not lead to compromising others. However, writing privilege separated software is difficult and as a result, a large number of software is monolithic, i.e., it runs as a whole without separation. Manually rewriting monolithic software into privilege separated software requires significant effort and can be error prone. We propose ProgramCutter, a novel approach to automatically partitioning monolithic software using dynamic data dependency analysis. ProgramCutter works by constructing a data dependency graph whose nodes are functions and edges are data dependencies between functions. The graph is then partitioned into subgraphs where each subgraph represents a least privilege component. The privilege separated software runs each component in a separated process with confined system privileges. We evaluate it by applying it on four open source software. We can reduce the privileged part of the program from 100% to below 22%, while having a reasonable execution time overhead. Since ProgramCutter does not require any expert knowledge of the software, it not only can be used by its developers for software refactoring, but also by end users or system administrators. Our contributions are threefold: (i) we define a quantitative measure of the security and performance of privilege separation; (ii) we propose a graph-based approach to compute the optimal separation based on dynamic information flow analysis; and (iii) the separation process is automatic and does not require expert knowledge of the software.

We present an automatic approach to detecting symmetry relations for general concurrent models. Despite the success of symmetry reduction in mitigating state explosion problem, one essential step towards its soundness and effectiveness, i.e., how to discover sufficient symmetries with least human efforts, is often either overlooked or oversimplified. In this work, we show how a concurrent model can be viewed as a constraint satisfaction problem (CSP), and present an algorithm capable of detecting symmetries arising from the CSP which induce automorphisms of the model. To the best of our knowledge, our method is the first approach that can automatically detect both process and data symmetries as demonstrated via a number of systems.

Hadoop is a popular open source implementation of MapReduce, that has a number of prominent users including Yahoo!, Facebook, and Twitter. Though several works have focused on deploying algorithms on Hadoop MapReduce, research efforts into applying formal methods to prove the correctness of hadoop systems are limited. In this paper we propose a holistic approach to verify the correctness of hadoop systems using model checking techniques. We model Hadoop's parallel architecture to constraint it to valid start up ordering and identify and prove the benefits of data locality, deadlock-freeness and non-termination among others.

UML diagrams are gaining increasing usage in Object-Oriented system designs. UML state machines are specifically used in modeling dynamic behaviors of classes. It has been widely agreed that verification of system designs at an early stage will dramatically reduce the development cost. Tool support for verification UML designs can also encourage consistent usage of UML diagrams throughout the software development procedure. In this work, we present a tool, named USMMC, which turns model checking of UML state machines into practice. USMMC is a self-contained toolkit, which provides editing, interactive simulation as well as powerful model checking support for UML state machines. The evaluation results show the effectiveness and scalability of our tool.

Modeling and verifying complex real-time systems are challenging research problems. The de facto approach is based on Timed Automata, which are finite state automata equipped with clock variables. Timed Automata are deficient in modeling hierarchical complex systems. In this work, we propose a language called Stateful Timed CSP and an automated approach for verifying Stateful Timed CSP models. Stateful Timed CSP is based on Timed CSP and is capable of specifying hierarchical real-time systems. Through dynamic zone abstraction, finite-state zone graphs can be generated automatically from Stateful Timed CSP models, which are subject to model checking. Like Timed Automata, Stateful Timed CSP models suffer from Zeno runs, that is, system runs that take infinitely many steps within finite time. Unlike Timed Automata, model checking with non-Zenoness in Stateful Timed CSP can be achieved based on the zone graphs. We extend the PAT model checker to support system modeling and verification using Stateful Timed CSP and show its usability/scalability via verification of real-world systems.

Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking that: (1) All executions of concurrent operations are serializable, and (2) the serialized executions are correct with respect to the sequential semantics. In this work, we describe a method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. The method does not require that linearization points in the implementations be given, which is often difficult or impossible. However, the method takes advantage of linearization points if they are given. The method is based on refinement checking of finite-state systems specified as concurrent processes with shared variables. To tackle state space explosion, we develop and apply symmetry reduction, dynamic partial order reduction, and a combination of both for refinement checking. We have built the method into the PAT model checker, and used PAT to automatically check a variety of implementations of concurrent objects, including the first algorithm for scalable nonzero indicators. Our system is able to find all known and injected bugs in these implementations.

Modeling and analyzing software architectures are useful for helping to understand the system structures and facilitate proper implementation of user requirements. Despite its importance in the software engineering practice, the lack of formal description and verification support hinders the development of quality architectural models. In this work, we develop an approach for modeling and verifying software architectures specified using Monterey Phoenix (MP) architecture description language. Firstly, we formalize the syntax and operational semantics for MP. This language is capable of modeling system and environment behaviors based on event traces, as well as supporting different architecture composition operations and views. Secondly, a dedicated model checker for MP is developed based on PAT verification framework. Finally, several case studies are presented to evaluate the usability and effectiveness of our approach.

Multi-agent systems, which are composed of autonomous agents, have been successfully employed as a modeling paradigm in many scenarios. However, it is challenging to guarantee the correctness of their behaviors due to the complex nature of the autonomous agents, especially when they have stochastic characteristics. In this work, we propose to apply probabilistic model checking to analyze multi-agent systems. A modeling language called PMA is defined to specify such kind of systems, and LTL property and logic of knowledge combined with probabilistic requirements are supported to analyze system behaviors. Initial evaluation indicates the effectiveness of our current progress; meanwhile some challenges and possible solutions are discussed as our ongoing work.

Model checking provides a way to automatically verify hardware and software systems, whereas the goal of planning is to produce a sequence of actions that leads from the initial state to the desired goal states. Recently research indicates that there is a strong connection between model checking and planning problem solving. In this paper, we investigate the feasibility of using different model checking tools and techniques for solving classic planning problems. To achieve this, we carried out a number of experiments on different planning domains in order to compare the performance and capabilities of various tools. Our experimental results indicate that the performance of some model checkers is comparable to that of state-of-theart planners for certain categories of problems. In particular, a new planning module with specifically designed searching algorithm is implemented on top of the established model checking framework, Process Analysis Toolkit (PAT), to serve as a planning solution provider for upper layer applications. A case study on a public transportation management system has been developed to demonstrate the idea of using the PAT model checker as a planning service.

No abstract available.

Model checking is emerging as an effective software verification method. Although it is desirable to have a dedicated model checker for each application domain, implementing one is rather challenging. In this work, we develop an extensible and integrated architecture in PAT3 (PAT version 3.*) to support the development of model checkers for wide range application domains. PAT3 adopts a layered design with an intermediate representation layer (IRL), which separates modeling languages from model checking algorithms so that the algorithms can be shared by different languages. IRL contains several common semantic models to support wide application domains, and builds both explicit model checking and symbolic model checking under one roof. PAT3 architecture provides extensibility in many possible aspects: modeling languages, model checking algorithms, reduction techniques and even IRLs. Various model checkers have been developed under this new architecture in recent months. This paper discusses the structure and extensibility of this new architecture.

BDD-based symbolic model checking is capable of verifying systems with a large number of states. In this work, we report an extensible framework to facilitate symbolic encoding and checking of hierarchical systems. Firstly, a novel library of symbolic encoding functions for compositional operators (e.g., parallel composition, sequential composition, choice operator, etc.) are developed so that users can apply symbolic model checking techniques to hierarchical systems with little knowledge of symbolic encoding techniques (like BDD or CUDD). Secondly, as the library is language-independent, we build an extensible framework with various symbolic model checking algorithms so that the library can be easily applied to encode and verify different modeling languages. Lastly, the applicability and scalability of our framework are demonstrated by applying the framework in the development of symbolic model checkers for three modeling languages as well as a comparison with the NuSMV model checker.

In this demonstration, a systematically domain-specific model checker, NesC@PAT, is presented. The tool takes NesC programs as input, and automatically verifies WSNs against properties specified in the form of deadlock freeness, state reachability or linear temporal logic formulas. We will show that NesC@PAT is able to find errors caused by rarely unexpected scenarios, which are difficult to be detected by general simulating or debugging.

Abstract: Ontologies are intended to facilitate semantic interoperability among distributed and intelligent information systems. Because of the distributed nature of the World Wide Web, Web ontologies have been developing in multiple forms of heterogeneity. For interoperating among information systems through heterogeneous ontologies, ontology mapping is a prerequisite process to generate alignment between two ontologies. In order to improve alignment accuracy, our approach is to clarify and enrich the semantics of ontological entities before mapping. For this purpose, we present a semi-automatic framework of entity classification and enrichment by applying three philosophical notions: identity condition, existential rigidity, and external dependency. Our objective is to supply a set of philosophy-driven anchors into ontologies for their mapping process by using a sortal taxonomy as a background knowledge model.

In recent years, many Web service composition languages have been proposed. Web service choreography describes collaboration protocols of cooperating Web service participants from a global view. Web service orchestration describes collaboration of the Web services in predefined patterns based on local decision about their interactions with one another at the message/execution level. In this work, we present model-based methods to close the gap between the two views. Building on the strength of model checking techniques, Web service choreography and orchestration are verified against temporal properties or against each other (to show that they are consistent). Specialized optimization techniques are developed to handle large Web service models. Furthermore, we propose a method to mechanically synthesize a prototype Web service orchestration from choreography, by repairing the choreography if necessary and projecting relevant behaviors to each service provider.

10.1145/1858996.1859072

Specification and verification of real-time systems are important research topics which have practical implications. In this work, we present a self-contained toolkit to analyze real-time systems, which supports system modeling, animated simulation and automatic verification (based on advanced model checking techniques like dynamic zone abstraction). In this tool, we adopt an event-based modeling language for describing real-time systems with hierarchical structure. Experiments show that our tool has compatible performance with the state-of-the-art verifiers, and complement them with additional capabilities like LTL model checking, timed refinement checking.

Interval-based specification languages have been used to formally model and rigorously reason about real-time computing systems. This usually involves logical reasoning and mathematical computation with respect to continuous or discrete time. When these systems are complex, analyzing their models by hand becomes error-prone and difficult. In this article, we develop a verification system to facilitate the formal analysis of interval-based specification languages with machine-assisted proof support. The verification system is developed using a generic theorem prover, Prototype Verification System (PVS). Our system elaborately encodes a highly expressive set-based notation, Timed Interval Calculus (TIC), and can rigorously carry out the verification of TIC models at an interval level. We validated all TIC reasoning rules and discovered subtle flaws in the original rules. We also apply TIC to model Duration Calculus (DC), which is a popular interval-based specification language, and thus expand the capacity of the verification system. We can check the correctness of DC axioms, and execute DC proofs in a manner similar to the corresponding pencil-and-paper DC arguments.

We share the views that specifications are preferably executable. In this tutorial, we introduce our latest effort on combining the expressiveness of integrated formal specification languages with the power of mechanical system analysis method like model checking. We present a process analysis toolkit (PAT) which is a self-contained framework for system specification, simulation and verification. PAT supports a modeling language named CSP# (short for communicating sequential programs).

High level specification languages like CSP use mathematical objects as abstractions to represent systems and processes. System behaviors are described as process expressions combined with compositional operators, which are associated with elegant algebraic laws for system analysis. Nonetheless, modeling systems with non-trivial data and functional aspects using CSP remains difficult. In this work, we propose a modeling language named CSP# (short for communicating sequential programs) which integrates high-level modeling operators with low-level procedural codes, for the purpose of efficient mechanical system verification. We demonstrate that data operations can be modeled as terminating sequential programs, which can be composed using high-level compositional operators. CSP# is supported by the PAT model checker and has been applied to a number of systems.

Abstract Simulink has been widely used in industry to model and simulate embedded systems. With the increasing usage of embedded systems in real-time safety-critical situations, Simulink becomes deficient to analyze (timing) requirements with high-level assurance. In this article, we apply Timed Interval Calculus (TIC), a real-time specification language, to complement Simulink with TIC formal verification capability. We elaborately construct TIC library functions to model Simulink library blocks which are used to compose Simulink diagrams. Next, Simulink diagrams are automatically transformed into TIC models which preserve functional and timing aspects. Important requirements such as timing bounded liveness can be precisely specified in TIC for whole diagrams or some components. Lastly, validation of TIC models can be rigorously conducted with a high degree of automation using a generic theorem prover. Our framework can enlarge the design space by representing environment properties to open systems, and handle complex diagrams as the analysis of continuous and discrete behavior is supported.

No abstract available.

Timed Interval Calculus (TIC) is a highly expressive set-based notation for specifying and reasoning about embedded real-time systems. However, it lacks mechanical proving support, as its verification usually involves infinite time intervals and continuous dynamics. In this paper, we develop a system based on a generic theorem prover, Prototype Verification System (PVS), to assist formal verification of TIC at a high grade of automation. TIC semantics has been constructed by the PVS typed higher-order logic. Based on the encoding, we have checked all TIC reasoning rules and discovered subtle flaws. A translator has been implemented in Java to automatically transform TIC models into PVS specifications. A collection of supplementary rules and PVS strategies has been defined to facilitate the rigorous reasoning of TIC models with functional and non-functional (for example, real-time) requirements at the interval level. Our approach is generic and can be applied further to support other real-time notations.

Verification techniques like SAT-based bounded model checking have been successfully applied to a variety of system models. Applying bounded model checking to compositional process algebras is, however, not a trivial task. One challenge is that the number of system states for process algebra models is not statically known, whereas exploring the full state space is computationally expensive. This paper presents a compositional encoding of hierarchical processes as SAT problems and then applies state-of-the-art SAT solvers for bounded model checking. The encoding avoids exploring the full state space for complex systems so as to deal with state space explosion. We developed an automated analyzer which combines complementing model checking techniques (i.e., bounded model checking and explicit on-the-fly model checking) to validate system models against event-based temporal properties. The experiment results show the analyzer handles large systems.

Timed Automata have proven to be useful for specification and verification of real-time systems. System design using Timed Automata relies on explicit manipulation of clock variables. A number of automated analyzers for Timed Automata have been developed. However, Timed Automata lack of composable patterns for high-level system design. Logic-based specification languages like Timed CSP and TCOZ are well suited for presenting compositional models of complex real-time systems. In this work, we define a set of composable Timed Automata patterns based on hierarchical constructs in timed enriched process algebras. The patterns facilitate hierarchical design of complex systems using Timed Automata. They also allow a systematic translation from Timed CSP/TCOZ models to Timed Automata so that analyzers for Timed Automata can be used to reason about TCOZ models. A prototype has been developed to support system design using Timed Automata patterns or, if given a TCOZ specification, to automate the translation from TCOZ to Timed Automata.

The design of an embedded control system starts with an investigation of properties and behaviors of the process evolving within its environment, and an analysis of the requirement for its safety performance. In early stages, system requirements are often specified as scenarios of behavior using sequence charts for different use cases. This specification must be precise, intuitive and expressive enough to capture different aspects of embedded control systems. As a rather rich and useful extension to the classical message sequence charts, Live Sequence Charts (LSC), which provide a rich collection of constructs for specifying both possible and mandatory behaviors, are very suitable for designing an embedded control system. However, it is not a trivial task to realize a high-level design model in executable program codes effectively and correctly. This paper tackles the challenging task by providing a mapping algorithm to automatically synthesize SystemVerilog programs from given LSC specifications.

This paper proposes a novel heterogeneous software architecture FTA (fault tolerant architecture). FTA incorporates idealized fault tolerant component concept and coordinated error recovery mechanism in the early system design phase. It can be reused in the high level model design of specific mission critical distributed systems with reliability requirements. The formal model of FTA in the Object-Z language is presented to provide precise idioms to the system designers. Formal proof using the Object-Z reasoning rules are constructed to demonstrate the fault tolerant properties of FTA. By analyzing the customization process, we also present a FTA template, expressed in x-frames using XVCL (XML-based variant configuration language) methodology, to automate the customization process. We apply a sales control system case study to illustrate the customization of FTA.

Many researchers at W3C currently focus on developing the next generation of the Web --- the Semantic Web. The development of the Web ontology languages, RDF, OWL and SWRL, is reminiscent of the early development of system specification languages in software engineering communities. Indeed, from the expressiveness point of view, Web ontology languages are subsets of Alloy, UML/OCL, VDM, Z and Object-Z. One can futher predict that the modeling languages for capturing the behaviours of the Semantic Web Services and Agents can be drawn from the rich collections of software dynamic modeling techniques, i.e., state machines, process algebra and integrated design methods. This tutorial will present a concise Modeling Languages Spectrum that includes a few key representative modeling languages ranging from simple static Web Ontology modeling techniques to expressive dynamic integrated modeling techniques. Comparisons and transformations between those languages will be discussed. Furthermore, based on transformation approaches, the latest research results on applying software modeling techniques and tools to the Semantic Web domain will be also demonstrated.

HighSpec is an interactive system for composing and checking OZTA specifications. The integrated high level specification language, OZTA, is a combination of Object-Z (OZ) and Timed Automata (TA). Building on the strength of Object-Z's in specifying data structures and Timed Automata's in modelling dynamic and real-time behaviors, OZTA is well suited for presenting complete and coherent requirement models for complex real-time systems. HighSpec supports editing, type-checking as well as projecting OZTA models into TA models and Alloy Models so that TA model checkers-UPPAAL and the Alloy Analyzer can be utilized for verification. Most importantly, HighSpec supports a novel yet effective mechanism advocated by OZTA for structural TA design, i.e., using a set of composable timed patterns to capture high level timing requirements and process behaviors and generate the TA part of model in a top-down way. HighSpec can also generate LaTeX document as an alternative media for the spread and read of established OZTA models.

This paper reports a recent research investigation on an integrated formal approach to model and verify sensor constraints in the context awareness systems.

This paper proposes a novel heterogeneous software architecture GFTSA (Generic Fault Tolerant Software Architecture) which can guide the development of safety critical distributed systems. GFTSA incorporates an idealized fault tolerant component concept, and coordinated error recovery mechanism in the early system design phase. It can be reused in the high level model design of specific safety critical distributed systems with reliability requirements. To provide precise common idioms & patterns for the system designers, formal language Object-Z is used to specify GFTSA. Formal proofs based on Object-Z reasoning rules are constructed to demonstrate that the proposed GFTSA model can preserve significant fault tolerant properties. The inheritance & instantiation mechanisms of Object-Z can contribute to the customization of the GFTSA formal model. By analyzing the customization process, we also present a template of GFTSA, expressed in x-frames using the XVCL (XML-based Variant Configuration Language) methodology to make the customization process more direct & automatic. We use an LDAS (Line Direction Agreement System) case study to illustrate that GFTSA can guide the development of specific safety critical distributed systems

Interaction-based and state-based modeling are two complementary approaches of behavior modeling. The former focuses on global interactions between system components. The latter concentrates on the internal states of individual components. Both approaches have been proven useful in practice. One challenging and important research objective is to combine the modeling power of both effectively and then use the combination as the basis for automatic design synthesis. We present a combination of interaction-based and state-based modeling, namely, live sequence charts and Z, for system specification. We then propose a way of generating distributed design from the combinations. Our approach handles systems with intensive interactive behaviors as well as complex state structures.

Started in the beginning of 2001, the semantic Web is regarded by many as the next generation of the Web. Ontology languages are the building blocks of semantic Web as they provide basic vocabularies for data markups: the ontologies. The correctness of shared ontologies is crucial to the proper functioning of agents. Hence ensuring the consistency of ontologies is a central issue in both the design and deployment phases of any semantic Web-aware application. Our experiences show that semantic Web is a novel and fruitful application domain for formal languages and their mature reasoning tool support. In order to ease the application of formal methods and tools to the semantic Web, we developed an integrated tools environment to support systematic development of OWL ontologies and then transformation, reasoning assistance and querying of them.

In recent years, researchers have begun to explore the potential of associating Web content with explicit meaning so that the Web content becomes more machine-readable and intelligent agents can retrieve and process information readily. The semantic Web (SW) proposed by W3C is one of the most promising and accepted approaches. It may have great impacts to the current Web. SW not only emerges from the knowledge representation and the Web communities, but also brings the two communities closer together. The software engineering community can also play an important role in the semantic Web development. Modeling and verification techniques can be useful at many stages during the design, maintenance and deployment of semantic Web ontology. We believe semantic Web will be a new research and application domain for software modeling techniques and tools.

When designing a complex system, Object-Z is a powerful logic-based language for modeling the system state aspects, and timed automata is an excellent graph-based notation for capturing timed control behaviour of the system. This paper presents an effective combination of the two techniques with novel composition and communication mechanisms. The combined notation enhances Object-Z with realtime modeling capability and also extends timed automata with enhanced structure and state modeling features.

Object-Z with history invariants can present precise and abstract models for complex systems. The system behavior patterns are often implicitly embedded within various state/operational constraints and history invariants. Without explicit system behavior representations, it is difficult to implement those abstract models. In this paper, we present a sound and systematic approach to automatically extract explicit system behaviors (as FSMs) from the abstract Object-Z specifications. Safety and liveness and additional crucial requirements for open systems are ensured.

Live sequence charts (LSCs) are a broad extension to message sequence charts (MSCs) to capture complex inter-object communication rigorously. A tool support for LSCs, named PlayEngine, is developed to interactively "play-in" and "play-out" scenarios. However, PlayEngine cannot automatically expose system design inconsistencies, e.g., conflicts between universal charts and etc. CSP is a formal language to specify sequential behaviors of a process and communication between processes, which has powerful tool supports, e.g., FDR. Semantically, system behaviors specified by LSCs correspond to CSP's traces and failures. This close semantic correspondence makes FDR a potential model checker for LSCs. The challenge is to discover a systematic way of constructing semantic preserving CSP models from LSCs. In this work, we investigate theoretical relations between LSCs and CSP. LSCs are formalized using trace and failure semantics so as to facilitate the semantic transformation from LSCs to CSP. The practical implication is that mature tool supports for CSP can be reused to validate LSCs. In particular, FDR is used to establish the consistency of an LSC model and perform various verifications.

The design of embedded and hybrid systems requires powerful mechanisms for modeling data, state, concurrency and real-time behaviour. The {first} part of this paper illustrates a powerful design notation Timed Communicating Object Z (TCOZ) that has both channel based and sensor/actuator based interfaces. We believe that TCOZ is well suited for presenting more complete and coherent design models for complex embedded and hybrid systems. However, the challenge is how to analyze and check these models with tools support. One effective approach is to project (transform) the design models into multiple domains, then to use existing specialized tools in those domains to perform the checking and analyzing tasks. The second part of this paper demonstrates one particular projection from TCOZ designs to Timed Automata (TA) models so that TA model checkers can be used to check time related properties.

Semantic Web is regarded as the next generation of the World Wide Web. It provides not only the structure of the Web but also meaningful semantics for the information presented. To make semantic Web services understandable for distributed agents, formal definitions of the ontologies and their consistencies are essential. However, the existing tools for reasoning about semantic Web ontologies are still primitive. We believe that mature software engineering tools, such as theorem provers, can contribute to the reasoning phase. In this paper, we present an approach of encoding the semantic Web ontology (DAML+OIL) into the generic theorem prover Isabelle/HOL for automatic reasoning. Furthermore, a translation tool was developed to transform semantic Web ontologies into their extended Isabelle theories. With additional intermediate lemmas, Isabelle can be used to perform both subsumption (class) level and instantiation (instance) level reasoning of the semantic Web ontologies.

Software systems have become increasingly distributed, dynamic and mobile. The complex state and dynamic interfaces of software components and their concurrent interactions provide challenging research issues in system specification and design. An effective combination of structured state-based formalism and dynamic action-based calculus may be a good solution for modeling complex distributed mobile systems. In this paper, we investigate the semantic links between Object-Z and /spl pi/ calculus and consequently introduce a powerful specification technique PiOZ that brings the strengths of the two together. The operational semantics of PiOZ integrates state transition semantics of Object-Z and /spl pi/-calculus reduction rules. The typing rules of PiOZ are developed and reasoning of a system property is presented.

Following the success of XML, W3C envisions the semantic Web (Berners-Lee et al., 2001) as the next generation of Web in which data are given well-defined and machine-understandable semantics so that they can be processed by intelligent software agents. Semantic Web can be regarded as an emerging area from the knowledge representation and the Web communities. The software engineering community can also play an important role in the semantic Web development. Modeling and verification techniques can be useful at many stages during the design, maintenance and deployment of semantic Web ontology. We believe semantic Web will be a new research and application domain for software modeling techniques and tools. For example, recent research results have shown that UML, Z (Woodcock and Davis, 1996) and Alloy (Jackson, 2002) can provide modeling, reasoning and consistency checking services for semantic Web.

Semantic Web, the next generation of Web, gives data well-defined and machine-understandable meaning so that they can be processed by remote intelligent agents cooperatively. Ontology languages are the building blocks of Semantic Web as they prescribe how data are defined and related. The existing reasoning and verification tools for Semantic Web are improving however still elementary. We believe that Semantic Web can be a novel application domain for software modeling languages and tools. Z is a formal modeling language for specifying software systems and Z/EVES is a proof tool for Z. In this paper, we firstly present Z semantics for ontology language DAML+OIL. This semantic model is embedded as a Z section daml2zin Z/EVES, which serves as an environment for checking and verifying Web ontologies. Then we present a tool for automatically transforming ontology documents into the specialized Z codes understood by Z/EVES. Finally, we use a recent real application, the military plan ontologies, to demonstrate the different reasoning tasks that Z/EVES can perform. Furthermore, undiscovered errors in the original ontologies were found by Z/EVES and some of these errors are even beyond Semantic Web modeling and reasoning capabilities.

The understanding of Semantic Web documents is built upon ontologies that define concepts and relationships of data. Hence, the correctness of ontologies is vital. Ontology reasoners such as RACER and FaCT have been developed to reason ontologies with a high degree of automation. However, complex ontology-related properties may not be expressible within the current web ontology languages, consequently they may not be checkable by RACER and FaCT. We propose to use the software engineering techniques and tools, i.e., Z/EVES and Alloy Analyzer, to complement the ontology tools for checking Semantic Web documents.In this approach, Z/EVES is first applied to remove trivial syntax and type errors of the ontologies. Next, RACER is used to identify any ontological inconsistencies, whose origins can be traced by Alloy Analyzer. Finally Z/EVES is used again to express complex ontology-related properties and reveal errors beyond the modeling capabilities of the current web ontology languages. We have successfully applied this approach to checking a set of military plan ontologies.

Formal modeling techniques can be used to define and verify software architectures precisely. The paper applies the integrated formal specification technique, Timed Communicating Object Z (TCOZ), to generic software architecture modeling and verification.

SOFL (structured-object-based-formal language) has been extended to a formal object-oriented language and method while keeping its structured features. This extension allows powerful object-oriented reuse mechanisms, such as class inheritance and object composition, to be utilized in the early design phases. This paper presents the semantics for this extended SOFL, and further demonstrates the extendibility and reusability of the object-oriented semantic models of SOFL.

We present an integrated approach to support both top-down and bottom-up design of software systems by combining UML (Unified Modeling Language) and the Formal Engineering Method SOFL (Structured Object-oriented Formal Language). We demonstrate by examples that the top-down principle used in conventional Structured Design can be effectively utilized to carry out object-oriented design that is usually seen as a way to suit bottom-up analysis and design. Furthermore, we also explain how the integrated approach helps to improve the preciseness and understandability of design documentations.

Abstract. Formal methods can be used in effective combination only if the semantic links between individual methods are clearly established. This paper discusses the semantic design of TCOZ, a language blended from Object-Z and TCSP. The semantic model adopted is the infinite timed failures model of TCSP, extended to include initial state and update events for modelling operations on internal state. An infinite trace model has been used so as to ensure proper account is taken of the potentially unbounded non-determinism allowed by Z schemas.

The challenge for system specification is how to visually and precisely capture static, dynamic and real-time system properties in a highly structured way. Timed Communicating Object-Z (TCOZ) is an integrated formal notation that build on Object-Z's strengths in modeling complex data structures, and on Timed CSP's strengths in modeling real-time interactions. In this paper, we demonstrate approaches of using XML/XSL as a transformation tool to visualize TCOZ models into various UML diagrams and to animate TCOZ specifications with a multi-paradigm programming language-Oz.

This paper presents the XML/XSL approach to the developmentofaweb environment for the formal specification language Object-Z. The projection techniques and tools from Object-Z (in XML) to UML (in XMI) are developed using XSL Transformations (XSLT). Furthermore, Object-Z (itself) is used to specify and design the essential functionalities of the web environment and the projection tools to UML. In a sense, the paper also demonstrates a formal approach to modeling web applications. Keywords Object-Z, XML/XSL/XMI, UML 1.

This paper describes a timed, multithreaded object modeling notation for specifying real-time, concurrent, and reactive systems. The notation Timed Communicating Object Z (TCOZ) builds on Object Z's strengths in modeling complex data and algorithms, and on Timed CSP's strengths in modeling process control and real-time interactions. TCOZ Is novel in that it includes timing primitives, properly separates process control and data/algorithm issues and supports the modeling of true multithreaded concurrency. TCOZ is particularly well-suited for specifying complex systems whose components have their own thread of control. The expressiveness of the notation is demonstrated by a case study in specifying a multilift system that operates in real-time.

Safety critical systems, such as aviation systems controlled by software, often have hard real-time requirements. Producing the correct result at the right time is the fundamental goal of such systems. Formally specifying the system functions and the timing requirements is the crucial step towards achieving such a goal. Aviation systems often need to be modified or upgraded on a regular basis, i.e. functionality and timing constraints may be altered. Therefore, the formal specification of such systems needs to be easily reused, maintained and modified. This paper demonstrates how the task scheduling aspects of an aircraft mission computer can be formalised in TCOZ.

Active objects have their own thread of control and passive objects are controlled by others. In Object-Z, all objects are modelled as passive objects. Timed Communicating Object Z (TCOZ) extends the Object-Z notation with Timed CSP's process and timing constructs. The blending of the concepts of object and non-terminating process leads to the notion of active object in TCOZ. This paper considers the concept of active object, its role and implications in formal real-time object-oriented specification.

Object-Z is an extension to the Z language designed to facilitate specification in an object-oriented style. It is an excellent tool for modeling data and algorithms, but its object semantics are single threaded and operations are atomic. Therefore, it is difficult to use Object-Z to capture the behaviour of concurrent real-time reactive systems. On the other hand, Timed CSP is good at modeling real-time concurrent behaviour, but has little support for modeling the state of a complex system. This paper introduces a blending of Object-Z and Timed CSP, known as TCOZ. The blended notation is particularly suited for specifying complex systems whose components have their own thread of control.

Formal methods are considered to be an important technique towards achieving the levels of assurance needed for high integrity systems. Formal specification is the essential part of the formal development process. The use of formal specification techniques on critical systems has shown significant growth in the last few years. In particular, there are a number of successful applications of using formal specification techniques in the aviation industry. Safety critical systems, such as aviation systems controlled by software, often have hard real time requirements. Producing the correct result at the right time is the fundamental goal of such systems. Formally specifying the system functions and the timing requirements is the crucial step towards achieving such a goal. Furthermore, aviation systems often need to be modified or upgraded on a regular basis, i.e. functionality and timing constraints may be altered. Therefore, the formal specification of such systems needs to be easily maintained and modified. We are interested in applying formal object modelling techniques to specify scheduling requirements of the multi parallel processes of an aircraft operational flight program (OFP). Our aim is not only to formalise the scheduling requirements for a particular aircraft, but more importantly to demonstrate an incremental and extendible modelling approach such that our model can be readily reused to specify other aircraft OFP scheduling requirements.

There are two constructs in the formal specification language Object-Z for modelling polymorphic and recursive structures. One construct, the free type, is adopted from the Z specification language. The other, class-union, facilitates polymorphic class declarations. Free type and class-union constructs are respectively based upon the functional value point of view and the object reference point of view. Consequently, the roles these two constructs perform in system modelling are different. The free type and class-union constructs are compared and discussed through various examples. The aim of this comparison and discussion is to present guidelines on how to appropriately and effectively use these two constructs to specify polymorphic and recursive structures.

When modelling a large and complex system, clarity of the specification becomes an important factor. In object-oriented specification, the states of individual objects are captured by the values of their attributes. Frequently however, there are dependencies between the attributes of an object. An appropriate indication of which attributes are primary (independent) and which are secondary (dependent) can add significantly to clarity. This paper details the notion of secondary attributes, their roles and implications in formal object-oriented specification.