Robustness verification is a promising technique for rigorously proving Recurrent Neural Networks (RNNs) robustly. A key challenge is to over-approximate the nonlinear activation functions with linear constraints, which can transform the verification problem into an efficiently solvable linear programming problem. Existing methods over-approximate the nonlinear parts with linear bounding planes individually, which may cause significant over-estimation and lead to lower verification accuracy. In this paper, in order to tightly enclose the three-dimensional nonlinear surface generated by the Hadamard product, we propose a novel truncated rectangular prism formed by two linear relaxation planes and a refinement-driven method to minimize both its volume and surface area for tighter over-approximation. Based on this approximation, we implement a prototype DeepPrism for RNN robustness verification. The experimental results demonstrate that DeepPrism has significant improvement compared with the state-of-the-art approaches in various tasks of image classification, speech recognition and sentiment analysis.

While recent studies show the effectiveness of in-context learning (ICL) for tabular data prediction, they also reveal significant fairness issues in large language models (LLMs).Prior work to mitigate fairness issues often employs interventions relying on subjective demonstration selection.Its effectiveness varies significantly with the specific demonstration content, leading to low controllability.Moreover, the improvement of fairness is highly unstable across different models and tasks.To address the challenges of low controllability and limited stability in fairness interventions, we propose Fairness-Aware Context-Contrastive Decoding (Fair-CCD).Fair-CCD first constructs Structural Bias Templates (SBTs), motivated by behavioral patterns observed in demonstrations, to encode the relationship between sensitive attributes and predicted labels in a structured and controllable form.During inference, Fair-CCD injects multiple SBTs and contrasts the model's responses, generating two differential signals that guide fairness adjustment and preserve task performance.By leveraging attention signals to scale decoding adjustments guided by the difference signals, Fair-CCD achieves stable and adaptive bias mitigation across models and tasks.Extensive experimental results demonstrate that Fair-CCD consistently improves fairness metrics without degrading task accuracy.

Abstract Today’s distributed systems operate in complex environments that inevitably involve faults and even adversarial behaviors. Predicting their performance under such environments directly from formal designs remains a long-standing challenge. We present the first formal framework that systematically enables performance prediction of distributed systems across diverse faulty scenarios. Our framework features a fault injector together with a wide range of faults, reusable as a library, and model compositions that integrate the system and the fault injector into a unified model suitable for statistical analysis of performance properties such as throughput and latency. We formalize the framework in Maude and implement it as an automated tool, PerF . Applied to representative distributed systems, PerF accurately predicts system performance under varying fault settings, with estimations from formal designs consistent with evaluations on real deployments.

Exception handling is crucial but challenging in program development. It needs to identify and handle all potential exceptions within programs to ensure system security and stabilization. Traditional exception handling relies on the expertise and experience of programmers, which often leads to oversights. Therefore, identifying exceptional code and recommending handling solutions are hot research topics with significant practical value. This paper presents a model called CodeHunter for exception localization and type prediction. The model first utilizes BERT-based model to represent code features and then uses Bi-LSTM for sequence labeling to pinpoint exceptional code. Additionally, this model also considers contextual features of the exception code and learns weights for the code within the try block and its context through the self-attention mechanism. Subsequently, it performs exception localization and predicts exception types. We conduct experiments on three different datasets. The results demonstrate that in the task of exception localization, our model can achieve a maximum accuracy of 98.6%, exceeding SOTA baselines by 11.2%. In the task of exception type prediction, our model can surpass the accuracy of SOTA baselines by a maximum of 18.7%, achieving 92.0% Top-1 accuracy. The rationality of techniques used in our model is also proved by the ablation testing. The model is implemented as an IDE plugin for programming convenience.

In the automotive industry, automated hardware-software integration testing is of vital importance for ensuring software quality and reducing project costs. However, in practice, the generation of automated test cases for such testing faces many challenges, primarily due to the complexity, implicit, and difficulty in identifying requirement dependencies. To address this issue, this paper proposes a requirement dependency-driven automated test case generation method. This method utilizes large language models to directly extract structured models, e.g., flowcharts, from natural language requirements documents. By analyzing these flowcharts, it can accurately identify implicit requirements dependencies and generate test scenarios, thereby specifying the execution order and temporal constraints for test case generation. In a real-world case study with the Beijing Automotive Industry Corporation (BAIC), the method successfully processed 300 functional requirements and identified a total of 4731 implicit dependencies. The content accuracy rate of the generated flowcharts reached 81.24%, and the business scenario coverage rate of the test cases reached 82.67%. These results preliminarily demonstrate the effectiveness and feasibility of our approach, significantly enhancing the level of automation in automotive integrated testing and providing strong technical support and reference for related practices in the industry.

The growing adoption of deep reinforcement learning (DRL) in safety-critical domains like autonomous driving has been hindered by the fundamental conflict between performance optimization and safety assurance. While DRL excels in high-dimensional state spaces and long-term planning, unexpected safety violations pose catastrophic risks. This work introduces a novel safety-aware DRL framework that integrates formal reachability analysis into the training pipeline. Our approach features two innovations: 1) a pre-trained reachability analysis module quantifying runtime safety risks through reachable state set computation, and 2) dynamic safety constraints enabling real-time policy adaptation. By embedding safety verification into the optimization loop, our method systematically balances exploration efficiency with risk mitigation. Empirical validation in autonomous driving scenarios demonstrates superior safety performance compared to conventional DRL methods, achieving significant collision avoidance while maintaining competitive efficiency. This framework bridges formal verification and DRL, providing a safety-aware solution for safety-critical systems. Future work will focus on computational efficiency optimization in dense obstacle environments.

Deep Reinforcement Learning (DRL) has gained prominence as an effective approach for control systems. However, its practical deployment is impeded by state perturbations that can severely impact system performance. Addressing this critical challenge requires robustness verification about system performance, which involves tackling two quantitative questions: (i) how to establish guaranteed bounds for expected cumulative rewards, and (ii) how to determine tail bounds for cumulative rewards. In this work, we present the first approach for robustness verification of DRL-based control systems by introducing reward martingales, which offer a rigorous mathematical foundation to characterize the impact of state perturbations on system performance in terms of cumulative rewards. Our verified results provide provably quantitative certificates for the two questions. We then show that reward martingales can be implemented and trained via neural networks, against different types of control policies. Experimental results demonstrate that our certified bounds tightly enclose simulation outcomes on various DRL-based control systems, indicating the effectiveness and generality of the proposed approach.

Abstract This paper serves as a comprehensive system description of version 2.0 of the Marabou framework for formal analysis of neural networks. We discuss the tool’s architectural design and highlight the major features and components introduced since its initial release.

Abstract The rapid advance of deep reinforcement learning techniques enables the oversight of safety-critical systems through the utilization of Deep Neural Networks (DNNs). This underscores the pressing need to promptly establish certified safety guarantees for such DNN-controlled systems. Most of the existing verification approaches rely on qualitative approaches, predominantly employing reachability analysis. However, qualitative verification proves inadequate for DNN-controlled systems as their behaviors exhibit stochastic tendencies when operating in open and adversarial environments. In this paper, we propose a novel framework for unifying both qualitative and quantitative safety verification problems of DNN-controlled systems. This is achieved by formulating the verification tasks as the synthesis of valid neural barrier certificates (NBCs). Initially, the framework seeks to establish almost-sure safety guarantees through qualitative verification. In cases where qualitative verification fails, our quantitative verification method is invoked, yielding precise lower and upper bounds on probabilistic safety across both infinite and finite time horizons. To facilitate the synthesis of NBCs, we introduce theirk-inductive variants. We also devise a simulation-guided approach for training NBCs, aiming to achieve tightness in computing precise certified lower and upper bounds. We prototype our approach into a tool called and showcase its efficacy on four classic DNN-controlled systems.

Deep neural networks (DNNs) have shown powerful performance in various applications and are increasingly being used in decisionmaking systems. However, concerns about fairness in DNNs always persist. Some efficient white-box fairness testing methods about individual fairness have been proposed. Nevertheless, the development of black-box methods has stagnated, and the performance of existing methods is far behind that of white-box methods. In this paper, we propose a novel black-box individual fairness testing method called Model-Agnostic Fairness Testing (MAFT). By leveraging MAFT, practitioners can effectively identify and address discrimination in DL models, regardless of the specific algorithm or architecture employed. Our approach adopts lightweight procedures such as gradient estimation and attribute perturbation rather than non-trivial procedures like symbol execution, rendering it significantly more scalable and applicable than existing methods. We demonstrate that MAFT achieves the same effectiveness as state-of-the-art white-box methods whilst improving the applicability to large-scale networks. Compared to existing black-box approaches, our approach demonstrates distinguished performance in discovering fairness violations w.r.t effectiveness (~ 14.69×) and efficiency (~ 32.58×).

FinTech software, crucial for both safety and timely market deployment, presents a compelling case for automated acceptance testing against regulatory business rules. However, the inherent challenges of comprehending unstructured natural language descriptions of these rules and crafting comprehensive test cases demand human intelligence. The emergence of Large Language Models (LLMs) holds promise for automated test case generation, leveraging their natural language processing capabilities. Yet, their dependence on human intervention for effective prompting hampers efficiency. In response, we introduce a groundbreaking, fully automated approach for generating high-coverage test cases from natural language business rules. Our methodology seamlessly integrates the versatility of LLMs with the predictability of algorithmic methods. We fine-tune pre-trained LLMs for improved information extraction accuracy and algorithmically generate comprehensive testable scenarios for the extracted business rules. Our prototype, LLM4Fin, is designed for testing real-world stock-trading software. Experimental results demonstrate LLM4Fin’s superiority over both state-of-the-art LLM, such as ChatGPT, and skilled testing engineers. We achieve remarkable performance, with up to 98.18% and an average of 20%−110% improvement on business scenario coverage, and up to 93.72% on code coverage, while reducing the time cost from 20 minutes to a mere 7 seconds. These results provide robust evidence of the framework’s practical applicability and efficiency, marking a significant advancement in FinTech software testing.

Deep Neural Networks (DNNs) are vulnerable to specially designed attacks due to their limited robustness. Abstraction methods can help extract critical features for learning, thereby reducing the disturbance caused by insignificant information. In this paper, we propose a pixelation-based abstraction method to enhance the empirical robustness of DNNs. The method partitions image pixels into superpixels and assigns each an appropriate colour from a continuously updated palette. Two hyperparameters control the abstraction level, allowing for resolution adjustment. Training and evaluation are conducted on pixelated datasets. Extensive experiments across benchmarks and loss landscape analysis demonstrate that our method (i) reduces attack success rates by up to 26.37% while maintaining high accuracy; (ii) exhibits a significant defense against diverse attack methods; and (iii) achieves smoother loss landscapes, underscoring its potential to enhance model robustness.

The polychronous or multi-clock paradigm is adequate to model large distributed systems where achieving a full timed synchronization is not only very costly but also often not necessary. It concerns systems made of a set of components with loose synchronization constraints. We study an approach where those components are orchestrated using logical clocks , made popular by L. Lamport and synchronous languages. The temporal and causal specification of those systems is built by defining a set of clock relations that would constrain the instant when clocks can tick or must not tick, thus defining families of valid schedules . In this article, we propose a specification language, called \(\mathit {LTL}_c/\mathit {CCSL}\) , for specifying temporal properties of multi-clock systems. While traditional temporal logics (LTL, MTL, CTL*), whether linear or branching, rely on a global step, our language, \(\mathit {LTL}_c/\mathit {CCSL}\) , builds a partial order on logical clocks, thus allowing both a hierarchical approach based on refinement of clock hierarchies and compositionality, as what happens in one clock domain may remain largely independent of what may happen in other domains. This good property helps preserve the properties without requiring to perform the proofs again. An \(\mathit {LTL}_c/\mathit {CCSL}\) specification consists of a clock temporal logic \(\mathit {LTL}_c\) , accompanied by a clock calculus called CCSL for specifying clock relations. We build the syntax and semantics of \(\mathit {LTL}_c\) and link its semantics with CCSL. After that, we mainly focus on the verification aspect of \(\mathit {LTL}_c/\mathit {CCSL}\) specifications using a model checking technique. We show how \(\mathit {LTL}_c/\mathit {CCSL}\) can be used for specifying multi-clock systems with an example.

Trigger-Action Programming (TAP) is a new programming paradigm enabling end-users to customize their smart devices by defining simple trigger-action rules. While it offers appealing convenience to end-users, TAP renders devices vulnerable to operation chaos and security risk resulting from potential defects in the rules. Verifying TAP rules defined by end-users is thereby necessary to detect such vulnerabilities at the early stage. However, such rules are difficult to analyze because their executions are often device-specific and environment-driven. Existing approaches require modeling them with their host devices and running environments, which is labor-consuming and hard to be automated. Moreover, the composition of devices causes state explosion, rendering the conflict analysis time-consuming. In this paper, we first build a large corpus of TAP rules developed by end-users. Analyzing this corpus results in six types of conflicts and reveals that nearly 90% of end-users made conflicts in their customized rules, and on average, 3.7 rules contain a conflict, which concurs with the necessity of developing practical conflict analysis techniques. Empirical analysis motivates us to propose a lightweight SMT-based approach for conflict analysis from a programmatic perspective. Compared to the existing approaches, our approach does not require modeling devices; thus, it could be fully automatic and flexible in efficiently detecting various types of conflicts. We implement the approach in a tool TapChecker. We analyze 12,514 TAP rules collected from real-world TAP platforms (10,535) and laboratory experiments (1,979). Experimental results show that our approach outperforms the state-of-the-art tool regarding the number of detected conflicts and efficiency.

Dealing with the ever-growing complexity of railway systems requires scalable approaches for detecting inconsistent safety requirements in practice. Despite significant efforts to automate the requirements consistency detection, current inconsistency analysis techniques of railway safety requirements still suffer from scalability issues. This paper proposes a two-layer approach for detecting inconsistencies in time-related safety requirements of railway systems, integrating two distinct formal methods from a pragmatic perspective. At the SafeNL layer, we employ an SMT-based approach to extract conflict patterns and use them to filter out inconsistent requirements descriptions, thus avoiding the more expensive general use of the SMT-based approach. At the CCSL layer, temporal dependencies in requirements are transformed into causal relations, which are then detected for circular inconsistencies using a graph search technique. Our evaluations demonstrate the utility and scalability of our approach.

Knowledge Tracing (KT) is a crucial task in the field of online education, since it aims to predict students' performance on exercises based on their learning history. One typical solution for knowledge tracing is to combine the classic models in educational psychology, such as Item Response Theory (IRT) and Cognitive Diagnosis (CD), with Deep Neural Networks (DNN) technologies. In this solution, a student and related exercises are mapped into feature vectors based on the student's performance at the current time step, however, it does not consider the impact of historical behavior sequences, and the relationships between historical sequences and students. In this paper, we develop DAKTN, a novel model which assimilates the historical sequences to tackle this challenge for better knowledge tracing. To be specific, we apply a pooling layer to incorporate the student behavior sequence in the embedding layer. After that, we further design a local activation unit, which can adaptively calculate the representation vectors by taking the relevance of historical sequences into consideration with respect to candidate student and exercises. Through experimental results on three real-world datasets, DAKTN significantly outperforms state-of-the-art baseline models. We also present the reasonableness of DAKTN by ablation testing.

This paper proposes a novel, abstraction-based, certified training method for robust image classifiers. Via abstraction, all perturbed images are mapped into intervals before feeding into neural networks for training. By training on intervals, all the perturbed images that are mapped to the same interval are classified as the same label, rendering the variance of training sets to be small and the loss landscape of the models to be smooth. Consequently, our approach significantly improves the robustness of trained models. For the abstraction, our training method also enables a sound and complete black-box verification approach, which is orthogonal and scalable to arbitrary types of neural networks regardless of their sizes and architectures. We evaluate our method on a wide range of benchmarks in different scales. The experimental results show that our method outperforms state of the art by (i) reducing the verified errors of trained models up to 95.64%; (ii) totally achieving up to 602.50x speedup; and (iii) scaling up to larger models with up to 138 million trainable parameters. The demo is available at https://github.com/zhangzhaodi233/ABSCERT.git.

The robustness of deep neural networks (DNNs) is crucial to the hosting system’s reliability and security. Formal verification has been demonstrated to be effective in providing provable robustness guarantees. To improve its scalability, over-approximating the non-linear activation functions in DNNs by linear constraints has been widely adopted, which transforms the verification problem into an efficiently solvable linear programming problem. Many efforts have been dedicated to defining the so-called tightest approximations to reduce overestimation imposed by over-approximation. In this paper, we study existing approaches and identify a dominant factor in defining tight approximation, namely the approximation domain of the activation function. We find out that tight approximations defined on approximation domains may not be as tight as the ones on their actual domains, yet existing approaches all rely only on approximation domains. Based on this observation, we propose a novel dual-approximation approach to tighten overapproximations, leveraging an activation function’s underestimated domain to define tight approximation bounds. We implement our approach with two complementary algorithms based respectively on Monte Carlo simulation and gradient descent into a tool called DualApp. We assess it on a comprehensive benchmark of DNNs with different architectures. Our experimental results show that DualApp significantly outperforms the state-of-the-art approaches with 100% − 1000% improvement on the verified robustness ratio and 10.64% on average (up to 66.53%) on the certified lower bound.

Formally verifying deep reinforcement learning (DRL) systems suffers from both inaccurate verification results and limited scalability. The major obstacle lies in the large overestimation introduced inherently during training and then transforming the inexplicable decision-making models, i.e., deep neural networks (DNNs), into easy-to-verify models. In this paper, we propose an inverse transform-then-train approach, which first encodes a DNN into an equivalent set of efficiently and tightly verifiable linear control policies and then optimizes them via reinforcement learning. We accompany our inverse approach with a novel neural network model called piece-wise linear decision neural networks (PLDNNs), which are compatible with most existing DRL training algorithms with comparable performance against conventional DNNs. Our extensive experiments show that, compared to DNN-based DRL systems, PLDNN-based systems can be more efficiently and tightly verified with up to $438$ times speedup and a significant reduction in overestimation. In particular, even a complex $12$-dimensional DRL system is efficiently verified with up to 7 times deeper computation steps.

Abstract Occlusion is a prevalent and easily realizable semantic perturbation to deep neural networks (DNNs). It can fool a DNN into misclassifying an input image by occluding some segments, possibly resulting in severe errors. Therefore, DNNs planted in safety-critical systems should be verified to be robust against occlusions prior to deployment. However, most existing robustness verification approaches for DNNs are focused on non-semantic perturbations and are not suited to the occlusion case. In this paper, we propose the first efficient, SMT-based approach for formally verifying the occlusion robustness of DNNs. We formulate the occlusion robustness verification problem and prove it is NP-complete. Then, we devise a novel approach for encoding occlusions as a part of neural networks and introduce two acceleration techniques so that the extended neural networks can be efficiently verified using off-the-shelf, SMT-based neural network verification tools. We implement our approach in a prototype called OccRob and extensively evaluate its performance on benchmark datasets with various occlusion variants. The experimental results demonstrate our approach’s effectiveness and efficiency in verifying DNNs’ robustness against various occlusions, and its ability to generate counterexamples when these DNNs are not robust.

The Clock Constraint Specification Language (CCSL) has been widely acknowledged as a promising system-level specification for the modeling and analysis of timing behaviors of real-time and embedded systems. However, along with the increasing complexity of modern systems coupled with strict time-to-market constraints, it becomes more and more difficult for requirement engineers to accurately figure out CCSL specifications from natural language-based requirement documents, since they lack both expertise in formal CCSL modeling and design automation tools to support quick and automatic generation of CCSL specifications. To solve the above problem, in this paper we introduce a novel and efficient Reinforcement Learning (RL)-based synthesis approach that can facilitate requirement engineers to quickly figure out their expected CCSL specifications. For a given incomplete CCSL specification, our approach adopts RL-based enumeration to explore all the feasible solutions to fill the holes within CCSL constraints, and leverages curiosity-driven exploration to accelerate the enumeration process. Based on the combination of our proposed curiosity-driven exploration heuristic and deductive reasoning techniques, our approach can not only prune unfruitful enumeration solutions effectively, but also optimize the enumeration process to search for the tightest solution quickly, thus the overall synthesis process can be accelerated dramatically. Comprehensive experimental results demonstrate that our approach significantly outperforms state-of-the-art methods in terms of both synthesis time and synthesis accuracy.

Due to deeply intertwined physical and hardware/software components together with an increasing number of interconnected heterogeneous devices powered by artificial intelligence (AI) techniques, the design complexity of cyber–physical systems (CPSs) becomes skyrocketing. Model-driven engineering (MDE) methods have been proven to be effective in increasing the productivity of CPS design. However, there is still a lack of MDE approaches that enable design space exploration as well as the code generation for the design of Artificial Intelligence of Things (AIoT)-based CPSs. To mitigate the situation, this article presents a unified modeling language named AIoTML for AIoT-based CPSs, which enables the construction of AI-based components across different modeling levels for the purposes of intelligent sensing and control. By extending the constructs of state-of-the-art domain-specific language (DSL) ThingML, AIoTML can seamlessly unify the modeling of both autonomous executions of AIoT devices and their surrounding physical environment, which facilitates both platform-independent simulation and control optimization for platform-specific CPSs. The compiler developed for AIoTML provides a family of code generators to support the construction of digital twins on various heterogeneous target AIoT platforms. Comprehensive evaluations on two complex real-world designs demonstrate the effectiveness of our AIoTML approach in the fast development of AIoT-based CPSs with high control quality.

As a promising requirement-level specification language for timing behavior modeling, the clock constraint specification language (CCSL) has become popular in the model-driven design community for safety-critical embedded systems. However, due to the skyrocketing design complexity, in practice, it is hard for requirement engineers to accurately construct requirement models with expected timing behaviors using CCSL, especially, for safe timing behaviors. Although more and more CCSL synthesis approaches are designed to facilitate the generation of CCSL specifications, most of them cannot be used directly for the synthesis of requirements models. This is because existing CCSL synthesis methods: 1) focus on filling the holes of CCSL constraints rather than completing requirements models and 2) rely heavily on limited observations of system behaviors, while the (temporal) safety properties of target systems are neglected. To address these issues, this article proposes a novel method that enables the automated synthesis of safe timing behaviors for requirements models. By specifying the safety timing properties of target systems using safely-LTL, our approach adopts CCSL as an intermediate representation of requirement synthesis, where incomplete requirements models coupled with safely-LTL-based properties are encoded into CCSL constraints with holes. Guided by the samples (expected behaviors) provided by requirement engineers, our approach can automatically figure out the complete version of incomplete requirements models. Comprehensive experimental results on two complex case studies demonstrate that our approach can not only quickly and efficiently synthesize requirement models but also guarantee that the synthesized models satisfy specified safety properties in Safely-LTL form.

Consistency verification of safety requirements is crucial for the success of safety-critical systems, particularly railway systems. However, this task often requires significant time spent on interaction and communication between domain experts, who possess in-depth knowledge of safety requirements in a specific domain, and formal experts, who have the necessary skills to apply verification tools and techniques. To enhance time efficiency and productivity, we propose an approach to empower domain experts with formal methods for verifying safety requirements’ consistency. This involves transforming natural requirements into formal models and using formal methods for verification. The approach also localizes inconsistent requirements to provide feedback to domain experts. Communication between domain experts and formal experts can be facilitated through the pattern language SafeNL. By adopting this approach, domain experts can utilize formal verification without extensive consultation with formal experts. Two practical case studies with CASCO Signal Ltd. validate its effectiveness, practicality, as well as a significant reduction of time compared to traditional methods (at least 90% reduction). This reduction in time is primarily due to reduced communication needs and more efficient localization. Evaluations show that SafeNL is user-friendly and the approach performs well in modular systems while scalability is somewhat limited.

Abstract Deep Reinforcement Learning (DRL) has demonstrated its strength in developing intelligent systems. These systems shall be formally guaranteed to be trustworthy when applied to safety-critical domains, which is typically achieved by formal verification performed after training. This train-then-verify process has two limits: (i) trained systems are difficult to formally verify due to their continuous and infinite state space and inexplicable AI components (i.e., deep neural networks), and (ii) the ex post facto detection of bugs increases both the time- and money-wise cost of training and deployment. In this paper, we propose a novel verification-in-the-loop training framework called Trainify for developing safe DRL systems driven by counterexample-guided abstraction and refinement. Specifically, Trainify trains a DRL system on a finite set of coarsely abstracted but efficiently verifiable state spaces. When verification fails, we refine the abstraction based on returned counterexamples and train again on the finer abstract states. The process is iterated until all predefined properties are verified against the trained system. We demonstrate the effectiveness of our framework on six classic control systems. The experimental results show that our framework yields more reliable DRL systems with provable guarantees without sacrificing system performance such as cumulative reward and robustness than conventional DRL approaches.

The robustness of deep neural networks is crucial to modern AI-enabled systems and should be formally verified. Sigmoid-like neural networks have been adopted in a wide range of applications. Due to their non-linearity, Sigmoid-like activation functions are usually over-approximated for efficient verification, which inevitably introduces imprecision. Considerable efforts have been devoted to finding the so-called tighter approximations to obtain more precise verification results. However, existing tightness definitions are heuristic and lack theoretical foundations. We conduct a thorough empirical analysis of existing neuron-wise characterizations of tightness and reveal that they are superior only on specific neural networks. We then introduce the notion of network-wise tightness as a unified tightness definition and show that computing network-wise tightness is a complex non-convex optimization problem. We bypass the complexity from different perspectives via two efficient, provably tightest approximations. The results demonstrate the promising performance achievement of our approaches over state of the art: (i) achieving up to 251.28% improvement to certified lower robustness bounds; and (ii) exhibiting notably more precise verification results on convolutional networks.

Deep learning has become a promising programming paradigm in software development, owing to its surprising performance in solving many challenging tasks. Deep neural networks (DNNs) are increasingly being deployed in practice, but are limited on resource-constrained devices owing to their demand for computational power. Quantization has emerged as a promising technique to reduce the size of DNNs with comparable accuracy as their floating-point numbered counterparts. The resulting quantized neural networks (QNNs) can be implemented energy-efficiently. Similar to their floating-point numbered counterparts, quality assurance techniques for QNNs, such as testing and formal verification, are essential but are currently less explored. In this work, we propose a novel and efficient formal verification approach for QNNs. In particular, we are the first to propose an encoding that reduces the verification problem of QNNs into the solving of integer linear constraints, which can be solved using off-the-shelf solvers. Our encoding is both sound and complete. We demonstrate the application of our approach on local robustness verification and maximum robustness radius computation. We implement our approach in a prototype tool QVIP and conduct a thorough evaluation. Experimental results on QNNs with different quantization bits confirm the effectiveness and efficiency of our approach, e.g., two orders of magnitude faster and able to solve more verification tasks in the same time limit than the state-of-the-art methods.

Deep Reinforcement Learning (DRL) is a promising technology for solving intractable control tasks.Its applications in safety-critical fields require high-reliability guarantees.However, formal verification of DRL systems is challenging because deep neural networks (DNNs) embedded in the applications are uninterpretable.In this paper, we propose a novel approach to linear temporal logic (LTL) model checking of DRL systems by extracting interpretable policies from DNNs.The extracted policy can retain comparable performance to the original DNN.More importantly, its decision domain is finite and thus directly verifiable against LTL properties using existing model checking techniques.Experimental results on four classic control systems demonstrate the effectiveness of our approach.

Abstract In the Internet of Things, smart devices are expected to correctly capture and process data from environments, regardless of perturbation and adversarial attacks. Therefore, it is important to guarantee the robustness of their intelligent components, e.g. neural networks, to protect the system from environment perturbation and adversarial attacks. In this paper, we propose a formal verification technique for rigorously proving the robustness of neural networks. Our approach leverages a tight liner approximation technique and constraint substitution, by which we transform the robustness verification problem into an efficiently solvable linear programming problem. Unlike existing approaches, our approach can automatically generate adversarial examples when a neural network fails to verify. Besides, it is general and applicable to more complex neural network architectures such as CNN, LeNet and ResNet. We implement the approach in a prototype tool called WiNR and evaluate it on extensive benchmarks, including Fashion MNIST, CIFAR10 and GTSRB. Experimental results show that WiNR can verify neural networks that contain over 10 000 neurons on one input image in a minute with a 6.28% probability of false positive on average.

Today’s distributed systems must satisfy bothqualitativeandquantitativeproperties. These properties are analyzed using very different formal frameworks: expressive untimed and non-probabilistic frameworks, such as TLA+ and Hoare/separation logics, for qualitative properties; and timed/probabilistic-automaton-based ones, such as Uppaal and Prism, for quantitative ones. This requires developing two quite different models of the same system, without guarantees of semantic consistency between them. Furthermore, it is very hard or impossible torepresentintrinsic features of distributed object systems—such as unbounded data structures, dynamic object creation, and an unbounded number of messages—using finite automata. In this paper we bridge this semantic gap, overcome the problem of manually having to develop two different models of a system, and solve the representation problem by: (i) defining a transformation from a very general class of distributed systems (a generalization of Agha’s actor model) that maps an untimed non-probabilistic distributed system model suitable for qualitative analysis to a probabilistic timed model suitable for quantitative analysis; and (ii) proving the two models semantically consistent. We formalize our models in rewriting logic, and can therefore use the Maude tool to analyze qualitative properties, and statistical model checking with PVeStA to analyze quantitative properties. We have automated this transformation and integrated it, together with the PVeStA statistical model checker, into theActors2PMaudetool. We illustrate the expressiveness of our framework and our tool’s ease of use by automatically transforming untimed, qualitative models of numerous distributed system designs—including an industrial data store and a state-of-the-art transaction system—into quantitative models to analyze and compare the performance of different designs.

The robustness of neural networks can be quantitatively indicated by a lower bound within which any perturbation does not alter the original input’s classification result. A certified lower bound is also a criterion to evaluate the performance of robustness verification approaches. In this paper, we present a tighter linear approximation approach for the robustness verification of Convolutional Neural Networks (CNNs). By the tighter approximation, we can tighten the robustness verification of CNNs, i.e., proving they are robust within a larger 10 perturbation distance. Furthermore, our approach is applicable to general sigmoid-like activation functions. We implement DeepCert, the resulting verification toolkit. We evaluate it with open-source benchmarks, including LeNet and the models trained on MNIST and CIFAR. Experimental results show that DeepCert outperforms other state-of-the-art robustness verification tools with at most 286.28% improvement to the certified lower bound and 1566.76 times speedup for the same neural networks.

Deep Neural Networks (DNNs) have achieved high accuracy on image classification. However, a small disturbance to an input may fool the networks to misclassify the label, which can cause a series of security and social problems. Thus, the robustness of DNNs must be ensured, particularly to those safety-critical systems. In this paper, we focus on the problem of measuring the robustness of ReLU-based DNNs, which can be equivalently formulated to solve a Mixed Integer Linear Programming problem (MILP). The complexity of solving MILP is directly related to the number of integer variables. We propose an efficient method for robustness measurement and verification by pruning the search space of MILP problems. Particularly, we design a greedy algorithm based on linear programming (LP) to determine the reasonable boundary. Then the search space is pruned by setting the boundary to integer variables in MILP. The comparison experiments on five classifiers trained on MNIST and CIFAR-10 datasets show our method outperforms other related tools in terms of efficiency and accuracy.

Nowadays the robustness of Deep Neural Networks (DNN) is gaining much more attention than ever. That is because DNNs are intensively adopted in safety-critical AI-enabled applications such as autonomous driving and authentication control. Formal methods have been proved to be effective to provide provable guarantee to the robustness of DNNs. However, they are suffering from bad scalability due to intrinsic high computational complexity of the verification problem. In this paper, we propose a novel attack-guided approach for efficiently verifying the robustness of neural networks. The novelty of our approach is that we use existing attack approaches to generate coarse adversarial examples, by which we can significantly simply final verification problem. In particular, we are focused on the neural networks that take ReLU activation functions, which are widely adopted for solving classification problems. The experimental results show that our approach outperforms those verification tools based on constraint solving by up to 69 times speedup, while it can compute minimum adversarial examples. The improvement is particularly significant on those adversarially trained networks.

Formal robustness verification of deep neural networks (DNNs) is a promising approach for achieving a provable reliability guarantee to AI-enabled software systems. Limited scalability is one of the main obstacles to the verification problem. In this paper, we propose eager falsification to accelerate the robustness verification of DNNs. It divides the verification problem into a set of independent subproblems and solves them in descending order of their falsification probabilities. Once a subproblem is falsified, the verification terminates with a conclusion that the network is not robust. We introduce a notion of label affinity to measure the falsification probability and present an approach to computing the probability based on symbolic interval propagation. Our approach is orthogonal to existing verification techniques. We integrate it into four state-of-the-art verification tools, i.e., MIPVerify, Neurify, DeepZ, and DeepPoly, and conduct extensive experiments on 8 benchmark datasets. The experimental results show that our approach can significantly improve these tools by up to 200x speedup when the perturbation distance is in a reasonable range.

The Clock Constraint Specification Language (CCSL) has become popular for modeling and analyzing timing behaviors of real-time embedded systems. However, it is difficult for requirement engineers to accurately figure out CCSL specifications from natural language-based requirement descriptions. This is mainly because: i) most requirement engineers lack expertise in formal modeling; and ii) few existing tools can be used to facilitate the generation of CCSL specifications. To address these issues, this paper presents a novel approach that combines the merits of both Reinforcement Learning (RL) and deductive techniques in logical reasoning for efficient co-synthesis of CCSL specifications. Specifically, our method leverages RL to enumerate all the feasible solutions to fill the holes of incomplete specifications and deductive techniques to judge the quality of each trial. Our proposed deductive mechanisms are useful for not only pruning enumeration space, but also guiding the enumeration process to reach an optimal solution quickly. Comprehensive experimental results on both well-known benchmarks and complex industrial examples demonstrate the performance and scalability of our method. Compared with the state-of-the-art, our approach can drastically reduce the synthesis time by several orders of magnitude while the accuracy of synthesis can be guaranteed.

The advance of deep learning makes it possible to empower safety-critical systems with intelligent capabilities.However, its intelligent component, i.e., deep neural network, is difficult to formally verify due to the large scale and intrinsic complexity of the verification problem.Abstraction has been proved to be an effective way of improving the scalability.A challenging problem in abstraction is that it is difficult to achieve a balance between the size reduced and output overestimation caused by abstraction.In this work, we propose an effective fine-grained approach to abstract neural networks.Our approach is fine-grained in that we identify four cases that should be abstracted independently under a certain neuron prioritization strategy.This allows us to merge more neurons in networks and meanwhile maintain a relatively low output overestimation.Experimental results show that our approach outperforms other existing abstraction approaches by significantly reducing the scale of target deep neural networks with small overestimation.

The Clock Constraint Specification Language (CCSL) is a logical time based modeling language to formalize timing behaviors of real-time and embedded systems. However, it cannot capture timing behaviors that contain uncertainties, e.g., uncertainty in execution time and period. This limits the application of the language to real-world systems, as uncertainty often exists in practice due to both internal and external factors. To capture uncertainties in timing behaviors, in this paper we extend CCSL by introducing parameters into constraints. We then propose an approach to transform parametric CCSL constraints into SMT formulas for efficient verification. We apply our approach to an industrial case which is proposed as the FMTV (Formal Methods for Timing Verification) Challenge in 2015, which shows that timing behaviors with uncertainties can be effectively modeled and verified using the parametric CCSL.

The software development profession suffers from severe gender biases, which could be explicit and implicit. However, SE literature has not systematically explored and evaluated the methods for reducing gender biases, especially for implicit gender biases. This paper reports on a field experiment to examine whether the intergroup contact theory could reduce implicit gender biases in software development. In the field experiment, 280 undergraduate students taking a project-centric introductory software engineering course were assigned to 70 teams with different contact configurations. We measured and compared their explicit and implicit gender biases before and after contacts in their teams. The study yields a rich set of findings. First, we confirmed the positive effects of intergroup contact theory in reducing gender biases, particularly the implicit gender biases in both general and SE-specific contexts. We further revealed that such effects were subjected to different contact configurations. The intergroup contact theory's effects were maximized in teams where the number of females is greater than or equal to the number of males. When the female is the minority group in a team, contacts among members contribute to reducing male members' implicit gender biases but fail to result in the same scale of effects on female members' implicit gender biases. The findings provide insights into using intergroup contact theory in reducing implicit gender biases in software development contexts.

Due to the merits of intuitive and visual modeling of design requirements, unified modeling language (UML) sequence diagrams are widely used as scenario-based specifications in the design of cyber-physical systems (CPSs). However, when more and more CPS products are deployed within an uncertain environment, existing sequence diagram analysis approaches cannot be used to accurately capture and quantify their timing behaviors at an early design stage. To address this problem, this article extends UML sequence diagrams to allow the modeling of stochastic system inputs, message processing time, and network delays, which strongly affect the system timing behaviors. We develop a statistical model checking-based framework that can automatically convert stochastic sequence diagrams into networks of priced timed automata to enable the quantitative analysis under various performance queries. The experimental results of two industrial designs in the railway field demonstrate the effectiveness of our approach.

Internet of Things (IoT) is being widely adopted to facilitate living environments such as cities and homes to become smart. Devices in IoT systems are capable of automatically adjusting their behaviors according to the change of environments. The capability is usually driven by the policies which are predefined inside devices. Policies can be customized by end users. Inconsistencies or conflicts among policies may cause malfunction of systems and therefore must be eliminated before deployment. In this paper, we propose a novel algebraic approach to modeling and verifying policy-driven smart devices in IoT systems on the basis of a domain-specific modeling language called PobSAM (Policy-based Self-Adaptive Model) and an efficient rewriting system called Maude. We formalize the operational semantics of PobSAM using Maude, which is an executable specification as well as a formal verification tool. The Maude formalization can be used to verify smart devices that are specified in PobSAM. We conduct a case study on a smart home setting to evaluate the effectiveness and efficiency of our approach.

The Clock Constraint Specification Language (CCSL) has been widely investigated in verifying causal and temporal timing behaviors of real-time embedded systems. However, due to limited expertise in formal modeling, it is difficult for requirement engineers to completely and accurately derive CCSL specifications from natural language-based design descriptions. To address this problem, we present a novel approach that facilitates automated synthesis of CCSL specifications under the guidance of sampled (expected) timing behaviors of target systems. By encoding sampled behaviors and incomplete CCSL constraints provided by requirement engineers using our proposed transformation templates, the CCSL specification synthesis problem can be naturally converted into a SKETCH synthesis problem, which enables the automated generation of CCSL specifications with high accuracy. Experiments on both well-known benchmarks and synthetic examples demonstrate the effectiveness and scalability of our approach.

Dynamic Software Updating (DSU) is a useful technique for updating running software without incurring any downtime. Its correctness must be guaranteed because updating a running software is a complicated and safety-critical process. In this paper, we present a formal tool called KupC for modeling and verifying dynamic updating of C programs. The tool is built on $$\mathbb {K}$$ –a formal semantic framework for programming languages. We formalize a patch-based dynamic updating mechanism in $$\mathbb {K}$$ based on the formal executable operational semantics of C. The formalization automatically yields an interpreter and several verification tools, which can be used to formally analyze the correctness of dynamic updating for C programs. To our knowledge, KupC is the first formal tool for code-level verification of dynamic software updating.

The Clock Constraint Specification Language ( CCSL ) is a formalism for specifying logical-time constraints on events for the design of real-time embedded systems. A central verification problem of CCSL is to check whether events are schedulable under logical constraints. Although many efforts have been made addressing this problem, the problem is still open. In this paper, we show that the bounded scheduling problem is NP -complete and then propose an efficient SMT-based decision procedure which is sound and complete. Based on this decision procedure, we present a sound algorithm for the general scheduling problem. We implement our algorithm in a prototype tool and illustrate its utility in schedulability analysis in designing real-world systems and automatic proving of algebraic properties of CCSL constraints. Experimental results demonstrate its effectiveness and efficiency.

People have to expose to collaborators from different countries in global software engineering (GSE) teams. They often rely on their perceptions of the country stereotypes to form their initial beliefs of the foreign collaborators and to make decisions on how to work with them. In this article, we employ the Stereotype Content Model (SCM) to investigate how explicit and implicit country stereotypes influence people' trust towards foreign collaborators and their decisions on cooperative behaviors. We conduct an empirical study with 92 professional software engineers with GSE experience. The results show that both SCM's explicit and implicit warmth, as well as the explicit competency, have significant impacts on the GSE team members' trust and cooperative behaviors in their initial interactions with unfamiliar foreign collaborators. Our findings indicate that Globally distributed collaboration practitioners may still need to overcome the over-reliance on country-of-origin cues when making attributions on unfamiliar foreign collaborators.

Consistency verification of safety requirements is an important but still challenging task for safety-critical systems such as rail transit systems. That is mainly because requirements are typically written in natural language and with strong time constraints. Driven by the practical need from industry, in this paper we propose a systematic approach to specify safety requirements in a quasi-natural language and automatically verify their consistency using formal methods. Specifically, we define a domain specific language SafeNL to specify safety requirements, and then automatically transform them into formal constraints defined in the Clock Constraint Specification Language (CCSL). The transformed constraints can be automatically and efficiently verified by model checking. We conduct two practical case studies to analyze the safety requirements of an interlocking system in CASCO Signal Ltd. Results of the studies show the validity and utility of our approach can pragmatically contribute to industrial practice. We also report some lessons learned from case studies.

Many transaction systems distribute, partition, and replicate their data for scalability, availability, and fault tolerance. However, observing and maintaining strong consistency of distributed and partially replicated data leads to high transaction latencies. Since different applications require different consistency guarantees, there is a plethora of consistency properties—from weak ones such as read atomicity through various forms of snapshot isolation to stronger serializability properties—and distributed transaction systems (DTSs) guaranteeing such properties. This paper presents a general framework for formally specifying a DTS in Maude, and formalizes in Maude nine common consistency properties for DTSs so defined. Furthermore, we provide a fully automated method for analyzing whether the DTS satisfies the desired property for all initial states up to given bounds on system parameters. This is based on automatically recording relevant history during a Maude run and defining the consistency properties on such histories. To the best of our knowledge, this is the first time that model checking of all these properties in a unified, systematic manner is investigated. We have implemented a tool that automates our method, and use it to model check state-of-the-art DTSs such as P-Store, RAMP, Walter, Jessy, and ROLA.

In automobile industry, it is a common approach to develop automobile real-time operating systems under some standards. For instance, OSEK/VDX is a world-wide adopted open standard. Traditional workflow is to first understand the standard, design and develop a system, then test its conformance to the standard, and finally deploy. There are several issues with the traditional workflow, e.g., ambiguities in standards may lead to incorrect design and implementation of real-world systems; the conformance of real-world systems to standards is difficult to check; and bug fixing after implementation is costly. To remedy the situation, in this paper, we present a unified executable formal automobile kernel under OSEK/VDX standard by defining the operational semantics of the system services in the standard using a rewrite-based executable semantic framework called$\mathbb {K}$. The formal kernel isunifiedin that it serves multiple purposes such as: 1) formal modeling of the OSEK/VDX standard helps detect ambiguities in the standard; 2) the executable kernel is essentially a formal model of the standard, which can be used to verify the correctness of automobile applications; and 3) verified applications can be used as test cases to check the conformance of a real-world automobile operating system against the OSEK/VDX standard. Using the formal kernel, we identify several ambiguities in the OSEK/VDX standard and a potential deadlock vulnerability in an industrial automobile application.

Dynamic Software Updating (DSU) is a promising technique for updating running software systems without incurring downtime. It is particularly useful to those systems which need to provide 24x7 services. Many efforts have been made to dynamic updating of the programs developed in mainstreaming languages such as C and Java. With the popularity of Python, many software servers are developed using Python and therefore they are desired to be dynamically updatable. However, there are few studies on dynamic updating of Python. To our knowledge, there exists only one updating approach for Python programs. The approach requires a dedicated Python interpreter in order to manipulate threads for updating, and consequently, it cannot be directly applied to mainstreaming Python interpreters. In this paper, we propose a novel dynamic updating approach to Python based on the built-in reloading mechanism that is supported by most of Python interpreters. Our approach is generic in that it is applicable to ordinary Python interpreters without any change to them. We implement a prototype called PyReload based on the proposed approach. PyReload is compatible with several mainstreaming Python interpreters such as CPython, Pypy and Jython. A case study is conducted to show the usage of PyReload. For performance, experimental results show that PyReload needs a shorter time for updating than the existing approach does.

BigTiMo calculus is for structure-aware mobile systems and it combines the TiMo calculus and the Bigraph model. Compared with TiMo, BigTiMo can model not only the locations of the components but also the connectivity of the components. Thus, our BigTiMo process can communicate not only locally with other process, but also remotely with other process. In this paper, we introduce the syntax and the operational semantics of the BigTiMo calculus. We also develop an executable formal specification of our Big-TiMo calculus in a declarative language called Maude. In addition, we verify safety properties of the mobile systems described by BigTiMo using state exploration and LTL model checking in Maude.

Scheduling is a central yet challenging problem in real-time embedded systems. The Clock Constraint Specification Language (CCSL) provides a formalism to specify logical constraints of events in real-time embedded systems. A prerequisite for the events is that they must be schedulable under constraints. That is, there must be a schedule which controls all events to occur infinitely often. Schedulability analysis of CCSL raises important algorithmic problems such as computational complexity and design of efficient decision procedures. In this work, we compare the scheduling problems of CCSL specifications to the real-time scheduling problem. We show how to encode a simple task model in CCSL and discuss some benefits and differences compared to more classical scheduling strategies.

Rust is a new and promising high-level system programming language. It provides both memory safety and thread safety through its novel mechanisms such as ownership, moves and borrows. Ownership system ensures that at any point there is only one owner of any given resource. The ownership of a resource can be moved or borrowed according to the lifetimes. The ownership system establishes a clear lifetime for each value and hence Rust does not necessarily need garbage collection. These novel features bring Rust high performance, fine-grained low-level control over memory without garbage collection, which differentiate Rust from other existing prevalent languages. For formal analysis of Rust programs and helping programmers learn its new mechanisms and features, a formal semantics of Rust is desired and useful as a fundament for developing related tools. In this paper, we present a formal executable operational semantics of a subset of Rust, called KRust. The semantics is defined in K, a rewriting-based executable semantic framework for programming languages. The executable semantics yields automatically a formal interpreter and verification tools for Rust programs. KRust has been validated by testing with 182 tests, including 157 tests from the official Rust

The Clock Constraint Specification Language (CCSL) is a formal language companion to MARTE (shorthand for Modeling and Analysis of Real-Time and Embedded systems), a UML profile used to facilitate the design and analysis of real-time and embedded systems. CCSL is proposed to specify constraints on the occurrences of events in systems. However, the language lacks efficient verification support to formally analyze temporal properties, which are important properties to real-time and embedded systems. In this paper, we propose an SMT-based approach to model checking of the temporal properties specified in Linear Temporal Logic (LTL) for CCSL by transforming CCSL constraints and LTL formulas into SMT formulas. We implement a prototype tool for the proposed approach and use the state-of-the-art tool Z3 as its underlying SMT solver. We model two practical real-time and embedded systems, i.e., a traffic light controller and a power window system in CCSL , and model check LTL properties of them using the proposed approach. Experimental results demonstrate the effectiveness and efficiency of our approach.

PKMv3 is the third version of Privacy and Key Management protocol, which plays an important role by providing key distribution and security access control in IEEE802.16m, the standard of Worldwide Interoperability for Microwave Access.The protocol should be guaranteed safe in terms of confidentiality, authentication and integrity.In this paper, we develop an executable formal specification of PKMv3 in an algebraic language called Maude and verify safety properties of the protocol using state exploration and LTL model checking in Maude.Unlike existing approaches, we consider the behaviors of intruders and time feature in our verification and verify both safety properties and time-related properties of the protocol.

Structure coverage driven test generation is the key approach for automatic testing at source code level. However, the defect detection ability of the generated test cases should be carefully evaluated since the correlation between coverage and test effectiveness is in doubt. In this paper, we propose a test generation approach based on mutation testing with the intent to derive test cases towards finding defects rather than just covering certain syntactic structures. Moreover, instead of generating test cases from the code under test directly, we base our approach on UML activity diagrams to make it possible to decide verdicts of test inputs. Mutation operators for activity diagrams are defined and the test generation algorithms are based on solving mutated path constraints. Experimental results have shown that by applying the proposed mutated testing approach, test cases with higher defect detection ability can be generated.

Even though software systems in some domains are expected to provide continuous services, most of them must undergo some form of changes. It leads to the emergence of dynamic software updating, a technique for updating a running software system without incurring any downtime. One of the challenges of designing a correct dynamic update is to identify a set of update points where the update can be safely applied to a running system. In this paper, we present a formal approach to modeling dynamic software updates and use the formal model to identify safe update points. In our approach, we formalize dynamic updates as state machines, and verify by model checking a set of desired properties which the running system is expected to satisfy after being updated. If counterexamples are found, we exclude those states that cause the counterexamples, and do model checking again. The process is iterated until all desired properties are successfully verified. We then finally obtain a set of safe update points. A case study is also presented to demonstrate the feasibility of the proposed approach.

This work evaluates Maude, an expressive and executable algebraic specification language, as a potential test sequence generation engine in the context of constraint-based test sequence generation for automotive operating systems. Our approach defines requirement specifications for automotive operating systems compliant with the OSEK/VDX international standard, and specifies constraint patterns in Maude. The correctness of the Maude specification is verified using LTL model checking and the test sequences from each classified environment are generated using reach ability computation provided by the Maude rewriting engine. Experimental evaluation shows that constraint-based test generation using Maude can be as effective as that of using NuS MV, a state machine based specification language specialized for model checking and specification-based testing, but more expressive and flexible.

With the growing demands for automotive auxiliary functions, more and more complex applications have been developed based on OSEK/VDX OS. However, how to check the developed applications is becoming a challenge for developers. Although some invaluable formal methods have been proposed to check actual software, these methods cannot be directly employed to check OSEK/VDX applications. In this paper, we describe and develop an approach to check OSEK/VDX applications using SMT-based bounded model checking. We also implement a prototype tool and conduct many experiments on several examples. The experiment results show that our approach can completely check the properties associated with (i) variables, (ii) mutual exclusion, (iii) service API, and (iv) tasks execution sequences of developed applications.

An approach to making liveness model checking problems under fairness feasible is described. The proposed method divides such a problem into multiple smaller ones that can be conquered such that the former is derived from the latter. Since the proposed method does not need any specialized algorithms, it can use existing LTL model checkers such as Spin, SAL and Maude LTL model checker. The proposed method also lets (or helps) humans get better understanding of the reason why they need to use fairness assumptions.

A state machine can be specified as either an equational theory or a rewrite theory in algebraic approaches. The former is used for theorem proving, and the latter for model checking. We have proposed an approach to transform a class of equational theories into rewrite theories in order to use them in the combination of the two verification techniques. This paper shows the correctness of the transformation with respect to its preservation of invariant properties. Invariant-preservation guarantees that a counterexample found by model checking a generated rewrite theory is also a counterexample of the same invariant in the original equational theory, which provides the theoretical support to the utilization of the transformation in combination of theorem proving and model checking.

Dynamic Software Updating (DSU) is a promising software maintenance technique, which aims at updating running software systems on the fly without incurring any downtime. The systems that require dynamic updating usually require high reliability assurance. Incorrect updating may cause them to behave erratically and/or even crash, and hence results in dreadful loss. However, there are few approaches to the study of the correctness of dynamic updating. In this paper, we systematically discuss the correctness of dynamic updating from a formal perspective, and present a first algebraic approach to formal analysis of it. The basic idea is to formalize dynamic updating systems as rewrite systems, with which we can analyze dynamic updates e.g. verifying their desired properties, or detecting incorrect update points, etc. The formal analysis helps us understand the behaviors of updated systems before we apply updates to the running systems, and hence improves the reliability of the systems after being updated.

OSEK/VDX Operating System Specification is a standard in automotive industry with a long history. Dozens of mature industrial operating systems are based on this specification and widely applied in the products of major automotive manufacturers. The verification of the operating system products is always a hard nut to crack. In this paper, we propose a formal specification of OSEK/VDX Operating System based on Hoare Logic, which helps us to get rid of the confusion and ambiguities of the informal specification. In this framework, the formalization of all the Application Programming Interfaces are made. As a case study, we link our framework to the formal verification tool VCC. Some errors are detected in a market-upcoming operating system product based on our framework. We conclude that our framework is feasible in verification of operating system.

Organizational Punishment/Penalty is a pervasive phenomenon in many professional organizations. In some software development organizations, punishment measures have been adopted in an attempt to improve software developers' performance, reduce the software defects, and hence ensure software quality. It is unclear whether these measures are effective. This article presents the results of a multi-method field study that analyzes software engineers' perception towards penalty policies in relation to software quality in a software development process. The results were generated via both qualitative and quantitative methods. Through interviews, we collected the individuals' perception towards the penalty policy. By extracting data in a software configuration management system, we identified several patterns of defects change. We found that while a penalty mechanism does help to reduce software defects in daily coding activity, it fails in achieving programmers' maximum work potential. Meanwhile, experienced software programmers require less time to adapt to penalty policies and benefit from exist of less experienced developers. Some additional findings and implications are also discussed.