Federated Learning (FL) enables multiple clients to collaboratively train models without sharing raw data, making it well-suited for privacy-preserving applications in heterogeneous IoT environments. However, disparities in client model architectures and computational resources often lead to accuracy degradation and the straggler problem, undermining training efficiency. To address these challenges, we propose HAPFL, a novel Heterogeneity-aware Personalized Federated Learning framework based on multi-level Reinforcement Learning (RL). HAPFL integrates three key components: 1) An RL-based model allocation mechanism that employs a PPO agent to assign appropriately sized models to clients based on their computing capabilities; 2) An RL-based training intensity adjustment scheme that dynamically controls local training epochs per client to reduce straggling latency; 3) A mutual learning scheme using knowledge distillation between each client's local model and a homogeneous lightweight model (LiteModel), which also serves as the global aggregation model to tackle model heterogeneity. Experiments on MNIST, CIFAR-10, and ImageNet-10 demonstrate that HAPFL achieves superior accuracy while reducing overall training time by$20.9 \%-40.4 \%$and straggling latency by$\mathbf{1 9. 0 \% - 4 8. 0 \%}$compared to existing approaches.

Ensuring the safety of complex industrial control systems (ICS) cannot be fully achieved during the design and development phases. Many uncertainties and unknowns only become apparent during real-world operation, especially in the context of Industry 4.0, where ICS integrate increasing characteristics of cyber-physical systems (CPS), such as openness and connectivity. Runtime verification (RV) is extensively employed to guarantee the runtime safety of systems. However, current RV methods face substantial challenges in ICS, particularly due to extensive device heterogeneity, intricate real-time constraints, and the need for coordinating multiple controllers. In this article, we propose a novel framework that incorporates stream-based RV to ensure the runtime safety of ICS. By leveraging a communication bridge based on the open platform communications unified architecture (OPC UA) standard, our framework achieves platform compatibility. This framework, coupled with its nonintrusive verification feature, is well-suited for scenarios involving heterogeneous devices and collaborative controllers. Additionally, stream-based formal specification captures complex time-sensitive constraints, such as real-time synchronizations involving various signals, including triggering, duration, and timeout. To further enhance safety, the framework offers online correction strategies for addressing runtime violations, aiming to preserve or restore system safety. Experimental results from general case studies demonstrate that our approach surpasses existing methods in managing device heterogeneity, complex real-time constraints, and multicontroller cooperation scenarios.

Monotone learning describes learning processes in which expected error consistently decreases as the amount of training data increases. However, recent studies challenge this conventional wisdom, revealing significant gaps in the understanding of generalization in machine learning. Addressing these gaps is crucial for advancing the theoretical foundations of the field. In this work, we utilize Probably Approximately Correct (PAC) learning theory to construct a theoretical error distribution that approximates a learning algorithm’s actual performance. We rigorously prove that this theoretical distribution exhibits monotonicity as sample sizes increase. We identify two scenarios under which deterministic algorithms based on Empirical Risk Minimization (ERM) are monotone: (1) the hypothesis space is finite, or (2) the hypothesis space has finite VC-dimension. Experiments on three classical learning problems validate our findings by demonstrating that the monotonicity of the algorithms’ generalization error is guaranteed, as its theoretical error upper bound monotonically converges to the minimum generalization error.

Source-free domain adaptation (SFDA) aims to address the challenge of adapting to a target domain without accessing the source domain directly. However, due to the inaccessibility of source domain data, deterministic invariable features cannot be obtained. Current mainstream methods primarily focus on evaluating invariant features in the target domain that closely resemble those in the source domain, subsequently aligning the target domain with the source domain. However, these methods are susceptible to hard samples and influenced by domain bias. In this paper, we propose a Consistent Assistant Domains Transformer for SFDA, abbreviated as CADTrans, which solves the issue by constructing invariable feature representations of domain consistency. Concretely, we develop an assistant domain module for CADTrans to obtain diversified representations from the intermediate aggregated global attentions, which addresses the limitation of existing methods in adequately representing diversity. Based on assistant and target domains, invariable feature representations are obtained by multiple consistent strategies, which can be used to distinguish easy and hard samples. Finally, to align the hard samples to the corresponding easy samples, we construct a conditional multi-kernel max mean discrepancy (CMK-MMD) strategy to distinguish between samples of the same category and those of different categories. Extensive experiments are conducted on various benchmarks such as Office-31, Office-Home, VISDA-C, and DomainNet-126, proving the significant performance improvements achieved by our proposed approaches. Code is available at https://github.com/RoryShao/CADTrans.git.

Programmable Logic Controllers (PLCs) are specialized computers extensively utilized in industrial control fields. Since they control industrial equipment, software faults in PLCs can result in significant losses. However, current testing for PLC programs is mainly manual, and there are very few automatic testing tools. Structured Text (ST) is one of the five PLC programming languages stipulated by the IEC 61131-3 standard, suitable for writing complex control logic. This paper proposes an automatic unit test case generation framework for ST programs based on Dynamic Symbolic Execution and PLC states, as well as a supporting algorithm, and implements the PLCAutoTester tool. PLCAutoTester supports the automatic generation of ST program unit test cases that comply with statement coverage, branch coverage, and MC/DC coverage criterion. We evaluated the PLCAutoTester using 20 PLC programs and compared it with S${}_{YM}$PLC. The experimental results show that PLCAutoTester can generate unit test cases with high coverage in a short time. And in 11 common programs, PLCAutoTester is able to generate test cases with almost the same statement coverage as S${}_{YM}$PLC while reducing the number of test cases by 95%.

With the ever-increasing demand for computing power in deep learning, distributed training techniques have proven to be effective in meeting these demands. However, current existing state-of-the-art distributed training frameworks, such as Parameter Server (PS), Ring-All-Reduce, and their varieties, still face significant challenges. In particular, the existence of communication bottlenecks can severely limit the efficiency and scalability of distributed training frameworks, making it difficult to fully and effectively exert the computing power of large-scale clusters, especially in the presence of dynamic and ever-changing network environments. To address these issues and further maximize the utilization of the computing power of clusters, in this paper we propose an efficient and dynamic distributed training framework, named GreedW. GreedW can greatly improve the training efficiency of workers by dynamically constructing an adaptive customized communication network and adaptively scheduling the workload. Specifically, GreedW employs a greedy strategy to dynamically construct the communication network tree in each iteration for gradient transmission with minimum communication cost and applies a heterogeneity-aware workload allocation scheme to adaptively balance the heavy traffic across heterogeneous workers in the cluster taking into account the available computing capabilities of each node, which effectively alleviates the network bottleneck. It is worth noting that GreedW is enabled to dynamically adjust the assigned job on each worker node based on their completion time during each round of model aggregation to ensure that each worker node completes its assignments around the same time, thus mitigating the intractable straggler issue and minimizing their idle waiting time. Comprehensive experimental evaluations on three different-scaled training models (i.e., Mnist-2NN, Mnist-CNN, and TextCNN) for image recognition and natural language processing tasks demonstrate that GreedW outperforms the existing state-of-the-art frameworks in terms of training efficiency, system flexibility, and robustness.

Taint analysis is concerned about whether a value in a program can be influenced, or tainted, by user input.Existing works on taint analysis focus on tracking the propagation of taint flows between variables in a program, and a security risk is reported whenever a taint source (user input) flows to a taint sink (resource that requires protection).However, a reported bug may have its taint source and taint sink located in different software components, which complicates the bug tracking and bug confirmation for developers.In this paper, we propose Taint Trace Analysis (TTA), which extends P/Taint, a context-sensitive Java taint analysis project, by making the taint information flow explicit.Thanks to the underlying Datalog semantics, we describe a way to extract traces of taint flows across program contexts and field accesses in the Doop framework.Different from existing works that produce only source-sink pairs, the output of TTA can be visualized as a set of traces which illustrate the inter-procedural taint propagation from taint sources to their corresponding sinks.As a consequence, TTA provides more useful information for developers and users after a vulnerability is reported.Our implementation is also efficient, and as shown in our experiment, it adds only a small run-time overhead on top of P/Taint for a range of analyses with different types of context-sensitivities applied.

Software requirements are the criteria for the correctness of the software behaviors. How to verify the correctness of the requirements is a big challenge in requirements engineering. Among various requirements approaches, the environment modeling based requirements engineering(EBRE) gains great popularity due to its explicit environment model. However, it still lacks of a formal approach to verify the correctness of the requirements models proposed in EBRE. Event-B is a popular formal method employing step-wise refinement to construct system models and verify their correctness according to the system requirements. This paper combines EBRE with Event-B to merge the advantages of the two methods. On the one hand, we transform the EBRE models to the initial Event-B model to guide the further design and development of the system. On the other hand, the transformed Event-B model can provide formal proof on the consistency of the requirements model. We also implement a plug-in tool on the Rodin platform to realize the automatic transformation from EBRE models to Event-B model and to commit a formal verification on the correctness of the transformed requirements model.

Supervised learning technologies represented by neural networks have made great progress in many fields. In particular applications such as image recognition and natural language processing, the entire computing process is completely handed over to the machine learning algorithm to directly learn the mapping from the feature space to the expected output, without considering much of the semantical information and domain knowledge of the data. In this paper, we propose a generic data refinement approach called divideup, which incorporates finer semantical information into the dataset to obtain a prediction model capturing more detailed information in the training data. By providing the information theory, we have high confidence that the learned model trained with the refined dataset has better prediction accuracy than the original one. We conduct extensive experiments on different datasets with the state-of-the-art neural network architectures such as ResNet and DenseNet. The experimental results show that divideup improves the prediction accuracy of all these deep learning architectures on the original test set. The divideup approach is also applied to other machine learning models such as random forest, XGboost and SVM. The results supports the conclusion that the refined training data obtained by divideup produces better prediction accuracy of the learned model.

In this article, we present a novel model checking approach to finite-time safety verification of black-box continuous-time dynamical systems within the framework of probably approximately correct (PAC) learning. The black-box dynamical systems are the ones, for which no model is given but whose states changing continuously through time within a finite-time interval can be observed at some discrete-time instants for a given input. The new model checking approach is termed as the PAC model checking due to the incorporation of learned models with correctness guarantees expressed using the terms error probability and confidence. Based on the error probability and confidence level, our approach provides statistically formal guarantees that the time-evolving trajectories of the black-box dynamical system over finite-time horizons fall within the range of the learned model plus a bounded interval, contributing to insights on the reachability of the black-box system and thus on the satisfiability of its safety requirements. The learned model together with the bounded interval is obtained by scenario optimization, which boils down to a linear programming problem. Three examples demonstrate the performance of our approach.

Autonomous driving is a safety critical system whose performance mainly depends on the recognition of the environment through a large amount of spatio-temporal data and driving policy based on the complex traffic conditions. Thus, it is important and necessary to build the abstract model of environment data and set the safety assessment method for autonomous driving policy. To address the problem, we propose a quantitative safety verification approach for the abstract decision-making model of autonomous driving. We extract the essential spatio-temporal features from both observation and estimation, and preserve them in the abstract model of decision-making. In the estimation, we adopt the explicit description of the uncertain driving decisions of vehicles by means of probability distributions. Based on these time-dependent spatial features, specification, reasoning, and verification of safety property are enabled. To evaluate the safety of the driving policy, we propose an operational verification approach based on Stochastic Hybrid Automata (SHA). Given the environmental information and the corresponding driving decisions according to the planned route on the basis of certain traffic laws, the single-lane roundabout scenario is introduced to illustrate how to verify quantitative safety property in our verification approach by using UPPAAL SMC which can validate the stochastic real-time model.

As a variant of Ant Colony Optimization, the EigenAnt algorithm finds the shortest path between a source node and a destination node based on negative feedback in the form of selective pheromone removal that occurs only on the path which is actually chosen for each trip. EigenAnt algorithm also could change quickly to reflect to the dynamic variety of initial pheromone concentrations and path length etc. However, in general, the solution of EigenAnt algorithm is not always convergent. In this paper, we propose an improved EigenAnt (iEigenAnt) algorithm in terms of both negative and positive feedback; that is, selective pheromone updates are decided by smart ants or stupid ones, which depends whether the amount of the pheromone at the selected path increases or not. The system modelled by our algorithm has a unique equilibrium as the shortest path. Besides, using mathematical analysis, we demonstrate that the equilibrium is global asymptotically stable, i.e., stable and convergent. Finally, we also implement the iEigenAnt algorithm under four different cases and apply it on travelling salesman problem problem, the simulation result shows that our iEigenAnt algorithm is faster convergent and more effective compared to the original EigenAnt algorithm, and some combinatorial optimisation problems can be effectively solved based on our iEigenAnt algorithm.

In a mobile system, mobility refers to a change in position of a mobile object with respect to time and its reference point, whereas isolation means the isolation relationship between mobile objects under some scheduling policies. Inspired by event-based formal models and the ambient calculus, we first propose the two types of special events, entering and exiting an ambient, as movement events to model and analyze mobility. Based on mobility, we then introduce the notion of the isolation of mobile objects for ambients. To ensure the isolation, a priority policy needs to be used to schedule the movement of mobile objects. However, traditional scheduling policies focus on task scheduling and depend on the strong hypothesis: The scheduled tasks are independent—that is, the scheduled tasks do not affect each other. In a practical mobile system, mobile objects and ambients interact with each other. It is difficult to separate a mobile system into independent tasks. We finally present an automatic approach for generating a priority scheduling policy without considering the preceding assumption. The approach can guarantee the isolation of the mobile objects for ambients in a mobile system. Experiments demonstrate these results.

The decision-making module on an autonomous car is usually a periodic program. In every cycle, the program makes a decision such as acceleration, brake, initiating a lane change process or a turn process based on the current traffic information gathered from car sensors. In urban traffic with mixed type of vehicles, the real-time performance requirement is critical for the decision-making program while acquiring global knowledge of the traffic is less practical. In such an environment, communications between vehicles are unreliable and time-consuming, so it is often difficult to know the exact driving decisions of other cars in the next cycle. In order to guarantee safety, a feasible solution requires the reasonable estimation on the driving decisions of other cars in the near future. In this paper, we propose a BMML (Bounded Multi-dimensional Modal Logic) to specify the traffic situations with spatio-temproral properties taking account of the estimated evolvement on them in the near future. The logic contains a primitive spatial logic with navigation operators and estimation operators as modal operators. The satisfaction of a BMML formula depends on a snapshot of the current traffic condition and an estimation structure capturing the believed information on the driving decisions of other cars. Given a snapshot and an estimation structure, the satisfaction of a BMML formula can be determined with simple and deterministic reasoning, so it is feasible for taking a BMML formula as the guard condition of the decision-making program of an autonomous car. The usage of BMML is illustrated with a series of small examples.

Abstract An autonomous agent is one that is not only directed by its environment, but is also driven by internal motivation to achieve certain goals based on beliefs about the environmental behaviour. Design paradigms for autonomous agents such as belief-desire-intention take into account the agent’s “mental” features when presenting its patterns of behaviour. In this paper we present an approach to modelling autonomous agents by introducing mental features to conventional transition system specifications. Mental features such as belief and desire are represented by declarative linear temporal logic formulas. Refinement is then proposed to define the correctness of the agent design and development. It turns out, however, that the introduction of these mental features is not monotonic with respect to refinement. We therefore introduce additional refinement proof obligations to enable the use of simulation rules when checking refinement.

Mobility is a critical issue that must be considered during the modeling and analyzing of a mobile system. At a high abstract level, event-based models can directly specify a mobile system without the introduction of additional mechanisms. In this article, we first propose two types of special events, entering and exiting an ambient, as movement events. Next, based on the movement events, we introduce the notion of a movement path and propose a feasible movement criterion (deciding whether a given movement path of a mobile object (agent) is feasible or not in terms of spatiotemporal topological relationships of ambients). Then, we investigate how a message movement--based communication model represents synchronous communication, asynchronous communication, and broadcast communication in a unified way. Finally, we use movement event sequences to discuss the exclusivity of ambients (an ambient only allows one mobile object to occupy (enter) it at any moment) and show that a priority scheduling control policy can guarantee exclusivity. Accordingly, we propose a correct movement criterion—that is, a correct movement path is feasible and satisfies the exclusivity of ambients. Case studies demonstrate these results.

Swarm robotic system is a complex system comprising a large number of distributed robots. Although a single robot has limited ability of computation and communication, their microscopic behaviors can finally lead to a macroscopic system behavior. Such phenomenon is called emergent behavior which is significantly useful but difficult to engineering due to its indecompositionality over time and scale. In this paper, we propose a formal framework to specify and verify the causality between the macroscopic emergent property and microscopic behaviors of robots. The framework supports hybrid specification of both continuous dynamics of robots and their discrete control programs. A refinement notion is defined in this framework which provides a formal development and verification approach to guide the design of a swarm robotic system satisfying expected emergent properties. We demonstrate the framework on a simple robot swarm consensus scenario.

The traditional research on scheduling focuses on task scheduling and schedulability analysis in concurrent reactive systems. In this article, we dedicate ourselves to event-based scheduling. We first formally define an event-based scheduling policy and propose the notion of the correctness of a scheduling policy in terms of weak termination. Then we investigate the correctness of the decomposition of scheduling controls and finally obtain a decentralized scheduling method. The method can automatically decompose the scheduling policies of a concurrent reactive system into atomic scheduling policies. Every atomic scheduling policy corresponds to one subsystem. Each of the subsystems is a completely independent system, which may be developed and deployed independently. An experiment demonstrates these results that may help engineers to design correct and efficient schedule policies for a concurrent reactive system.

Virtualization is fundamental to cloud computing. It allows abstraction centred on services and isolation of lower level functionalities and underlying hardware. Modeling, analyzing and verifying cloud systems necessarily involve virtualization and services. However, there exist few efforts to effectively formalizing virtualization in cloud computing. In this paper, based on services we present an approach for defining virtualization. We discuss some properties of service virtualization under some operations and the correctness of virtual services (virtual services without abnormal behavioral problems). Moreover, we investigate automatic configuration of a service based on virtualization, that is, given a virtualized service, how can we automatically obtain all possible correct virtual services of such a service? The configuration process is to first separate a virtualized service into atomic and correct virtual services and then merge these atomic virtual services into all possible correct virtual services of such a virtualized service. The obtained theoretical results help to formally analyze, verify and configure cloud systems.

Self-organising systems are distributed systems which achieve an ordered global state without centralised control. They include adaptive sensor networks, swarm robotic systems and mobile ad-hoc networks. Designing such systems is difficult and often based on a trial-and-error approach. In this paper, we provide an approach which is both systematic and formal. Our approach builds on the formalism of Object-Z and the refinement approach of action systems. It follows an intuitive approach to development which breaks a refinement proof into three steps which the designer may iterate through on the way to the final design.

Asynchronous multi-agent systems (AMAS) are multi-agent systems with asynchronous updates and communications. They are often designed from the point of view of local computations and the interactions of autonomous agents. However, often some functionality of the system is proposed from the global point of view. It is not always possible to verify such global functionality under total, random, asynchrony and such asynchrony is unrealistic in most cases. Several non-functional factors such as the variance of local clocks of the agents and the message delays play essential roles in implementing ordered asynchrony in practice and should be taken into account in the specification and verification. In this paper, we present a specification framework for AMAS using Object-Z and bounded fairness constraints. The bounded fairness constraints are used to specify required non-functional factors. We demonstrate that under these constraints the system's functionality can be guaranteed by the local behaviour of the agents.

As an automotive industry standard of operating system specification, OSEK/VDX is widely applied in the process of designing and implementing the static operating system and the corresponding interfaces for automotive electronics. It is challenging to explore an effective method to support large-scale correctness verification of OSEK/VDX specification. In this paper, we employ process algebra CSP to describe and reason about a real code-level OSEK/VDX operating system. Thus the whole system is formally modeled as a CSP process which is encoded and implemented in process analysis toolkit (PAT). Furthermore, the expected properties are described and expressed in terms of the first-order logic. The properties are also established and verified in our framework. The result indicates that the whole system is deadlock-free and the scheduling scheme is sound with respect to the specification.

In this paper we present a probabilistic calculus for formally modeling and reasoning about Mobile Ad Hoc Networks (MANETs) with unreliable connections and mobility of nodes. In our calculus, a MANET node can locally broadcast messages to a group of nodes within its physical transmission range. The group probability is also introduced since two distinct nodes within different groups should receive messages from the same sender with different possibilities. Our calculus naturally captures essential features of MANETs, i.e., local broadcast, mobility and probability. Moreover, we give a formal operational semantics of the calculus in terms of the labeled transition system and define the notion of open bisimulation. Finally, we illustrate our calculus with a toy example.

The web environment creates risks together with benefits for web services. Web services often engage attacks from hackers or anyone having hostile intensions. The behavior of services is often effected by the environment changes which should be included in its specifications. In addition, services usually have some mechanisms provided by the developers to deal with the environment changes, especially attacks. However, common specifications of services seldom contain such information. This paper provides a formal behavioral model based on the service behaviors related to its environments and environment changes. A refinement relation is also provided in the behavior model. This model can form a view to analyze the environment influence to the service and compare them according to their defending mechanisms.

Competitions of shared Web resources have been widely concerned today. Under the circumstances of networks, no central supervisor can be implemented, which makes it more complicated to avoid deadlock problems. This paper describes the interactions of Web services and shared web resources using CSP method. Deadlocks can be analyzed based on the formal model.

As a programming model, MapReduce is implied for easier processing and generating large cluster of distributed data sets. We use CSP framework to model MapReduce system through which the parallelization of the computation and the distribution of data across multiple machines can be reflected. Some properties of MapReduce can be verified based on the achieved model.

Nowadays the B/S (browser/server) architecture has become one of the most popular approaches to implement the Web service. Because of the instability of the Web environment, keeping the consistency of the data is of essential importance. Consequently we turn to formal methods intending to avoid inconsistencies in the B/S architecture. This paper describes a service-oriented system with the B/S architecture using the CSP (communicating sequential processes) method. We define the processes in the system and the behaviors of them. After the definition, we analyze the causes of inconsistencies and demonstrate that the formal definition and mechanism we made can implement an inconsistency free system, which means the inconsistency can be avoided or fixed.