Multi-modal salient object detection (MSOD), which integrates complementary modalities such as depth or thermal data, primarily faces two challenges: accurately preserving salient object details and effectively aligning cross-modal features. Recent advances in using Stable Diffusion to generate images with fine edge details have inspired researchers to reformulate MSOD as a conditional mask generation process guided by salient features, which has achieved excellent visual results. However, these approaches often overlook the high computational cost and large-scale architecture of Stable Diffusion, both of which render it unsuitable for real-world MSOD applications. Therefore, we propose SimpleDiffusion, the first lightweight and efficient conditional diffusion model for MSOD that does not rely on Stable Diffusion. Specifically, we propose an Adaptive Cross-Modal Fusion Conditional Network and a Latent Denoising Network to reduce the complexity of diffusion models. Furthermore, we design a Multi-modal Feature Rectification and Fusion Module to enhance the representational capacity of cross-modal salient features. Customized training and sampling strategies are also developed to improve inference efficiency and reduce erroneous object segmentations. Experiments on multiple MSOD datasets demonstrate that SimpleDiffusion reduces model size by over tenfold and improves inference speed by more than fivefold compared to other diffusion-based methods, while maintaining comparable or superior performance.

Multi-modal salient object detection (SOD) through the integration of additional data such as depth or thermal information has become a significant task in computer vision during recent years. Traditionally, the challenges of identifying salient objects in RGB, RGB-D (Depth), and RGB-T (Thermal) images are tackled separately. However, without intricate cross-modal fusion strategies, such approaches struggle to effectively integrate multi-modal information, often resulting in poorly defined object edges or overconfident inaccurate predictions. Recent studies have shown that designing a unified end-to-end framework to handle all three types of SOD tasks simultaneously is both necessary and difficult. To address this need, we propose a novel approach that treats multi-modal SOD as a conditional mask generation task utilizing diffusion models. We introduce DiMSOD, which enables the concurrent use of local (depth maps, thermal maps) and global controls (original images) within a unified model for progressive denoising and refined prediction. DiMSOD is efficient, only requiring fine-tuning of our newly introduced modules on the existing stable diffusion, which not only reduces the fine-tuning cost, making it more viable for practical use, but also enhances the integration of multi-modal conditional controls. Specifically, we have developed modules including SOD-ControlNet, Feature Adaptive Network (FAN), and Feature Injection Attention Network (FIAN) to enhance the model's performance. Extensive experiments demonstrate that DiMSOD efficiently detects salient objects across RGB, RGB-D, and RGB-T datasets, achieving superior performance compared to previous well-established methods.

Salient Object Detection (SOD) aims to identify and segment the most striking elements within an image. Salient object detection methods can be differentiated into several types according to the input data, such as RGB-D (Depth) and RGB-T (Thermal). Previous research primarily focused on saliency detection for single data types. However, forcing an RGB-D SOD model to process RGB-T data will degrade its performance significantly. In addition, current methods still face challenges in detecting fine edge details of salient objects and achieving end-to-end training. To address these issues, we introduce diffSOD, which leverages stable diffusion and cross-modal feature rectification and fusion module for saliency detection by transforming salient object detection into a denoising process from a noisy mask to an object mask. It offers a unified solution for salient object detection that seamlessly spans both RGB-D SOD and RGB-T SOD. Extensive experiments validate the effectiveness of the proposed diffSOD, demonstrating its ability to efficiently detect salient objects across both RGB-D and RGB-T data, while achieving superior performance over state-of-the-art methods.

Open-vocabulary semantic segmentation (OVSS) is a challenging computer vision task that labels each pixel within an image based on text descriptions. Recent advancements in OVSS are largely attributed to the increased model capacity. However, these models often struggle with unfamiliar images or unseen text, as their visual language understanding is limited to training data. Text-to-image (T2I) diffusion models have demonstrated strong image generation with diverse open-vocabulary descriptions. It prompted us to explore whether the comprehensive priors in T2I diffusion models could enhance the zero-shot generalization of OVSS. In this study, we define OVSS as a denoising diffusion task from noisy to object mask and introduce Seg-diffusion, a novel method based on Stable Diffusion that utilizes its extensive visual and linguistic prior knowledge. Specifically, the object mask diffuses from ground-truth to a random distribution in latent space. The model learns to reverse this noisy process to reconstruct object mask to segment objectives using text embeddings with our proposed Content Attention Module (CAM). Extensive experiments on popular OVSS benchmarks show that Seg-diffusion outperforms previous well-established methods and achieves impressive zero-shot generalization to unseen datasets.

Advanced online execution monitoring is an essential system for ensuring the safety of nuclear facilities. Formal modeling and quantitative evaluation of these systems offer a promising approach to verifying their behaviors and identifying potential vulnerabilities. However, existing modeling languages often lack the capability to represent the system’s control flow logic. Additionally, the absence of automated transformation rules hinders the verification of generated models using available verification tools. Hence, in this paper, we propose a novel synchronous modeling language, Hybrid SynLong, which integrates data flow and control flow to effectively describe the real-time dynamic behaviors of online monitoring systems. Additionally, we present a method for converting the Hybrid SynLong language model into a network of stochastic hybrid automata, enabling direct verification with existing statistical model checkers. In consequence, the performance of an online monitoring system can be quantitatively evaluated by executing well-defined queries. The experimental results illustrate the effectiveness and efficiency of the proposed modeling language and transformation algorithms, as demonstrated through their application in an online monitoring system for a nuclear plant.

Visual anomaly detection in computer vision is an essential one-class classification and segmentation problem. The student-teacher (S-T) approach has proven effective in addressing this challenge. However, previous studies based on S-T underutilize the feature representations learned by the teacher network, which restricts anomaly detection performance. In this study, we propose a novel feature-constrained and attention-conditioned distillation learning method for visual anomaly detection with localization, which fully uses the features of the teacher model and the local semantics of the critical structure to instruct the student model to detect anomalies efficiently. Specifically, we introduce the Vision Transformer (ViT) as the back-bone for anomaly detection tasks, and the central feature strategy and self-attention masking strategy are proposed to constrain the output features and impose agreement between multi-image views. It improves the ability of the student network to describe normal data features and widens the feature difference between the student and teacher networks for abnormal data. Experiments on the benchmark datasets demonstrate that the proposed method significantly improves the performance of visual anomaly detection compared with the competing methods.

Effective anomalous signal detection in time series multimedia data is imperative for safety-critical cyber-physical systems (CPS). Nevertheless, constructing a system for precise and rapid anomaly detection is challenging due to complex system dynamics, long-range dependencies, and unidentified sensor noise in modern CPS. This study proposes TranBF, an innovative time series anomalous signal detection method designed with a carefully engineered deep Transformer network and Bayesian Filtering. TranBF aims to capture the dynamics and broader temporal dependencies of CPS within a dynamic state-space and recursively track the uncertainty of system noise over time, thereby significantly improving the robustness and accuracy of anomaly detection. Extensive experiments on three real-world public datasets demonstrate that TranBF can significantly out-perform state-of-the-art baseline methods in terms of detection performance. Specifically, TranBF enhances F1 scores by a maximum of 16.5% while concurrently reducing training times by as much as 39.3% compared to the baseline models. Furthermore, the ablation study furnishes empirical evidence supporting the effectiveness of each component within TranBF.

To address the challenge of visual anomaly detection amidst complex background interference. First, we construct a structural causal model for anomaly detection under complex background interference and propose an intervention strategy to block background feature interference. Then, we build an anomaly feature-sensitive neural network (AFSNN) containing two feature extraction modules based on the causal intervention strategy. Given the limitations of convolutional neural networks in capturing global features associated with spatial location dependence, and the substantial data requirements of vision transformers, we opt for the enhanced Swin Transformer module and the deformable convolutional networks encoder module to extract global features and local details, respectively. We also designed the cross-attention to fuse these two scales of feature representation. Finally, we introduce a causality-sensitive learning module that differentiates the outputs of the two feature extraction modules and constructs a causality-sensitive loss function by maximizing the output differences. This approach blocks background features and enhances sensitivity to anomaly features during training. Experiments show that AFSNN can effectively attenuate the confusing interference of the background pattern.

The Traveling Salesman Problem is a combinatorial optimization problem that seeks to find the shortest path visiting a set of locations, where each location is visited exactly once, and the path returns to the starting point. Using traditional computing model to solve Traveling Salesman Problem would face the issue of state explosion. This paper proposes a solving method based on the probe machine model, greatly accelerating the solving speed. By iteratively adding probes and performing probe operations in sequence, both optimal and feasible solutions for this problem can be obtained. We developed a solver PROBE4TSP and presented its framework and execution process. Through comparative experiments, we demonstrate that this method is faster than some classical solvers for small-scale Traveling Salesman Problems, especially fewer than thirty nodes.

Multi-agent systems (MASs) have garnered significant interest across various academic fields. Although MASs are widely applicable, they continue to encounter several challenges, particularly in terms of security.. Model checking, a verification technique that examines all possible system states, is employed to address these challenges. However, the state space of many practical systems can be prohibitively large, leading to exponential growth in verification time. This study introduces a new method for verifying MASs using Strategy Computation Tree Logic (SCTL) via the connective probe machine, a model of fully parallel computing. This approach is pioneering in utilizing the probe machine to speed up MAS verification, specifically allowing for the parallel resolution of SCTL formulas. Unlike conventional model checkers, our method can uncover multiple counterexamples for specified properties, facilitating the identification of various system flaws. We have developed a model checker named MC2PM based on our approach and have validated its feasibility and efficiency through experiments.

Abstract Salient Object Detection (SOD) is a challenging task that aims to precisely identify and segment the salient objects. However, existing SOD methods still face challenges in making explicit predictions near the edges and often lack end‐to‐end training capabilities. To alleviate these problems, we propose SOD‐diffusion, a novel framework that formulates salient object detection as a denoising diffusion process from noisy masks to object masks. Specifically, object masks diffuse from ground‐truth masks to random distribution in latent space, and the model learns to reverse this noising process to reconstruct object masks. To enhance the denoising learning process, we design an attention feature interaction module (AFIM) and a specific fine‐tuning protocol to integrate conditional semantic features from the input image with diffusion noise embedding. Extensive experiments on five widely used SOD benchmark datasets demonstrate that our proposed SOD‐diffusion achieves favorable performance compared to previous well‐established methods. Furthermore, leveraging the outstanding generalization capability of SOD‐diffusion, we applied it to publicly available images, generating high‐quality masks that serve as an additional SOD benchmark testset.

Deep reinforcement learning (DRL) is widely applied in motion planning for multi-robot systems as DRL leverages the offline training process to improve the real-time computation efficiency. In DRL-based methods, the DRL models compute an action for a robot based on the states of its surrounding obstacles, including other robots in the system. They always assume that the number of obstacles is fixed and the obtained obstacles’ states are reliable. However, in the real world, a multi-robot system may suffer from various attacks, such as remote control attacks and network attacks, that cause wrong positions of the surrounding obstacles received by a robot. In this paper, we propose a robust motion planning methodDAE-Crit-LSTM, integrating a denoising autoencoder (DAE) with DRL models, to mitigate such position deception attacks in environments with a different number of obstacles.DAE-Crit-LSTMshows the following two advantages. First,DAE-Crit-LSTMcan be applied in benign and attacked scenarios and thus does not require any detector. It learns an encoder and a decoder to approximate the accurate positions of the obstacles, no matter under attack or not. Second,DAE-Crit-LSTMapplies an LSTM (Long Short-Term Memory)-based DRL model to deal with a variable number of obstacles in the environment. It is worth noting thatDAE-Crit-LSTMis method-agnostic and can be easily implemented in state-of-the-art motion planning methods. Comprehensive experiments show thatDAE-Crit-LSTMcan mitigate position deception attacks and guarantee safe motion. We also demonstrate the effectiveness and generalization ofDAE-Crit-LSTM.

Machine learning has become a promising technology for anomaly detection of cyber-physical systems (CPSs). However, the trained anomaly detection models always suffer from bias due to the scarcity of anomaly data in CPSs and the biased data collection process, which may poison the models' generalization ability. Recent debiasing methods are proposed to deal with the bias via resampling the training dataset, reweighting during the training phase, or adjusting the classification threshold. However, they may lose valuable information, need extra knowledge of the models, or lead to overfitting. Especially, they lack a causal understanding of the debiasing process, so they cannot point out the source and propagation of the bias and, thus, cannot deal with it in an explainable way. In this article, we propose a counterfactual debiasing framework to mitigate the bias in a well-trained model. First, we formalize the model's training and inference processes using causal graphs. Thus, we can understand the source and propagation of the model's bias through causal inference. Then, we use counterfactual inference to estimate the bias's detrimental causal effect on the prediction and remove it from the total causal effect. Therefore, we can conduct unbiased inferences with a biased model. The proposed method can remove the bias in an explainable way by incorporating causal graphs. Comprehensive experiments are conducted on seven real-world CPS datasets, i.e., IDA, MFP, ACS, SPF, UNS, NSL, and ICS. The results demonstrate the effectiveness, compatibility, and unbiasedness of the proposed approach.

Great achievements have improved the efficiency and effectiveness of formal verification fairly, such that it is now applicable to industrial-scale software. However, verifying a full software system is still considered too complex. In practice, industrial control software models to be verified may result in state space explosion. We propose a problem frame-based approach that takes the full software system as input and tries to decompose the full software model into some smaller modules. Our approach decomposes the whole safety requirements to sub safety requirements, and the verification problem of the whole model is projected to sub verification problem according to the decomposed safety requirements. The sub verification problems check the projected sub models against the the sub safety requirements. We carry out an extensive evaluation based on the trackside subsystems in rail transit. Verifying the decomposed model can lead to a significant performance gain, due to the fact that abstract models reduce too much state space.

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.

Anomalous signal detection aims to detect unknown abnormal signals of machines from normal signals. However, building effective and interpretable anomaly detection models for safety-critical cyber-physical systems (CPS) is rather difficult due to the unidentified system noise and extremely intricate system dynamics of CPS and the neural network black box. This work proposes a novel time series anomalous signal detection model based on neural system identification and causal inference to track the dynamics of CPS in a dynamical state-space and avoid absorbing spurious correlation caused by confounding bias generated by system noise, which improves the stability, security and interpretability in detection of anomalous signals from CPS. Experiments on three real-world CPS datasets show that the proposed method achieved considerable improvements compared favorably to the state-of-the-art methods on anomalous signal detection in CPS. Moreover, the ablation study empirically demonstrates the efficiency of each component in our method.

Some examples of systems and their organizations that have ignored or violated human values have caused very devastating and widespread damage. To prevent these incidents, operationalizing human values in systems transforms the values into concrete concepts such that they can be validated. There are several challenges such as a lack of techniques to integrate values, mechanisms to trace values, formalized perspective of values. To address these challenges, we propose Ont4Sys, an ontology-based tool of semantic representation and verification for traceability models with human value. Our research uses the formal theory Ontology to integrate value into the model and traces value under traceability’s guidance. The verification and labeling algorithm is provided to verify values and help with inspections. Two subject systems are selected for feasibility and accuracy evaluation. The experimental results show that our approach can effectively verify human values; moreover, based on traceability, there is at least a 50% reduction rate in model size to help with inspections. The labeling algorithm ensures high recall while minimizing the "noise" that is detrimental to the user’s understanding of the system.

The decision-making process in autonomous driving systems encounters large uncertainties with environmental changes and needs to face the complex spatio-temporal evolution of multiple objectives.Formal analysis and verification are crucial to establishing reliable and safe standards.In this paper, we propose an extension of the clock constraint language CCSL to construct spatio-temporal constraint and autonomous driving safety specifications, leveraging various autonomous driving scenarios.Additionally, we introduce probabilistic spatio-temporal events and devise extensions for driving specifications that incorporate stochasticity.This specification is converted to the UPPAAL-SMC model for facilitating formal modeling and verification.Specific schemes and verification are given in conjunction with a typical autonomous driving scenario.

With the applications of deep learning in safety-critical domains such as autonomous driving systems gaining ground, it demands rigorous verification to guarantee the safety and reliability of corresponding systems. As the intelligent component in such systems, neural networks (NNs) must be robust in that their outputs are not affected by minor perturbation to inputs. Many research studies have shown that formal methods are effective ways to the robustness verification of NNs. However, most of the existing approaches are focused on NNs that contain monotonic activation functions, such as ReLU, Tanh, and Sigmoid. In this work, we propose an approach to verify the robustness of NNs with the nonmonotonic activation function called Swish. Such networks have been proved to have a better performance on image classification than other NNs. In our approach, we turn the robustness verification problem into a constraint-solving problem using the linear approximation technique. We first model the affine function of an NN into a linear constraint model. Then, for nonlinear activation functions, we leverage an efficient approximation strategy to linearly approximate them. Finally, we utilize the constraint solver gurobi to solve the model, which reveals that the model satisfies the robustness property. We develop a prototype tool and evaluate it with open-sourced NNs. Experimental results showed the effectiveness and efficiency of our approach.

Avionics embedded systems are subjected to stringent timing requirements to be verified. Evaluating if messages meet their timing requirements, such as the latency constraint, is of the highest importance from the design stage of avionics systems. End-to-end latency of messages is an important design parameter that needs to be within specified bounds for the correct functioning of avionics systems. In this paper, we define the “SysML Flow Model” for the first time. Subsequently, we propose an approach to transfer the SysML Flow Model to a timed automaton, to perform schedulability and end-to-end latency verification. This fills an important gap in the method toolbox of the safety-critical domain engineer. The definition has a profound potential to broaden the use of Model-Driven Architecture and its well-known advantages in safety-critical avionics applications. Finally, we apply this technique to an industrial case of a flight management system.

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.

Automatic flight control systems (AFCS) are safety-critical systems tightly integrating computation, networking and physical processes. However, the uncertainty resulting from evolving dynamics in cyberspace and the physical world can affect the reliability of decision-making in the controller, threatening the system’s safety. How to accurately capture the uncertainty, effectively control the aircraft and improve safety has become an unavoidable challenge for the software industry. To this end, we define an uncertainty-aware modeling language (UAML), which supports modeling the AFCS’s dynamic behavior and environmental uncertainty using formal specifications. We use a machine learning-based method to predict the risk levels in operating environments as the representation of uncertainty from the physical world. The prediction result is transferred to UAML as the parameters. On this basis, we present a framework for quantitative safety evaluation using statistical model checking based on UPPAAL-SMC to help AFCS make reliable decisions at runtime. We illustrate our approach by modeling and analyzing a realistic example, and the experimental result demonstrates the effectiveness of our approach.

Establishing formal modeling and verification methods for requirements has become the key to enhancing avionics software’s safety and development efficiency. As the mainstream modeling language used in Model-Based Software Engineering (MBSE), SysML is often applied to software requirements specifications. However, due to the lack of systematic and rigorous semantic definitions, SysML can cause problems in terms of accuracy and consistency in system development, threatening the correctness of safety-critical avionics software. To address the problem, this paper defines Safety SysML State Machine, an extended SysML state machine for safety control functions. Stepwise, the authors illustrate the formal specification and the refinement rules of the Safety SysML State Machine to construct the avionics integration model. Furthermore, a tool is implemented integrating the modeling and verification of the Safety SysML State Machine. Our contribution has a profound potential to broaden the use of MBSE and its well-known advantages in safety-critical applications. A specific case study on the aircraft roll angle control system demonstrates the effectiveness of our approach and the tool.

Bounded Model Checking (BMC) has been found promising in finding deep vulnerabilities in industry designs and scaling well with design sizes. However, the parallelisation of BMC is challenging, due to the propositional satisfiability (SAT) problem and satisfiability modulo theories problem solving being hard to parallelise. In this paper, we propose a novel approach to perform BMC based on the mathematical model of probe machine, which is the first approach to employ probe machine to accelerate BMC, particularly it can solve SAT formulas in full parallel. We introduce the workflow of the algorithm and explain in detail the process of mapping BMC to the probe machine. A method is provided to prove the correctness of the algorithm and to analyze its time complexity. We develop a model checker called BMC2PROBE based on our approach and explain the framework and memory management of the tool. The experiment results are discussed, which prove the feasibility and effectiveness of our approach.

One of the major challenges confronting System Modeling Language(SysML) is that it cannot always provide verifiable guarantees of formalization and rigorousness.To verify model designs, the research of transformation from SysML to ontology emerges because of ontology's formal standards and verifiability obtained by ontology reasoners.However, existing transformation approaches are mostly limited to a single view without traceability or lack a clear process so that it can't be automated.In this paper, we propose a novel approach to maintain precious traceability between requirements and model multi-views design based on ontology.In addition, our approach contains a normative process of ontology building in support of an automated implementation.We use this approach to obtain the ontology of a safety-critical system and carry out the ontology evaluation experiment, whose results demonstrate the feasibility and efficiency 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.

Cyber-physical System (CPS) represents a system that tightly integrates computation, communication, and physical processes. As an effective modeling language, AADL is often applied for real-time and embedded systems. However, AADL has limitations in modeling stochastic events because the interaction between the system and an uncertain external environment is often complex and unpredictable. In this paper, we propose a stochastic hybrid modeling language based on AADL, called SHML. SHML supports both continuous behavior analysis and probabilistic modeling of CPSs. To achieve the verification objective, we present a set of mapping rules to transform the SHML design into networks of stochastic hybrid automata (NSHA). By using statistical model-checking techniques, the obtained NSHA model and performance queries are jointly applied to evaluate the quantitative performance of SHML designs. Experiments on traffic collision avoidance systems are conducted, and the results demonstrate the usability and effectiveness of our approach.

Reinforcement learning (RL) can be defined as the process of learning policies that maximize the expectation of the rewards. It has shown success in solving complex decision-making tasks. However, reinforcement learning-based controllers do not provide guarantees of safety of physical models in Cyber-physical systems (CPSs). In this paper, we propose a framework, which allows implementing RL to the safe control system by transforming formal analysis to learned policy. For satisfaction verification and quantitative analysis, we propose an uncertainty modeling language CSML to describe behaviors of the system, and transform CSML design into networks of probabilistic timed automata (NPTA). For safe learning, we present an algorithm called Safe Control with Formal Methods (SCFM). SCFM constructs a state set that obeys the constraint described by probabilistic computation tree logic (PCTL) via exploring state space before the learning process. The monitor monitors the system, determines whether the chosen action is safe and corrects unsafe decisions. We validate our method through experiments of lane-change control for autonomous cars.

Reinforcement learning algorithms discover policies that are lauded for their high efficiency, but don't necessarily guarantee safety. We introduce a new approach that provides the best of both worlds: learning optimal policies while enforcing the system to comply with certain model to keep the learning dependable. To this end, we propose Timed Differential Dynamic Logic to express the system properties. Our main insight is to convert the properties to runtime monitors, and use them to monitor whether the system is correctly modeled. We choose the optimal polices only if the reality matches the model, or we will abandon efficiency and instead to choose a policy that guides the agent to a modeled portion of the state space. We also propose Dependable Mixed Control (DMC) algorithm to implement a framework for application. Finally, the effectiveness of our approach is validated through a case study on Communication-Based Autonomous Control (CBAC).

Model checking has established as an effective method for automatic system analysis and verification.It is making its way into many domains and methodologies.However, the state space may be extremely large for many practical systems, and this is a major limitation for state-space search algorithms in model checking.We have proposed a novel computing model called probe machine in 2016, which is a fully parallel computing model.In comparison to the Turing machine, it can solve the graph search problems efficiently, which can overcome the existing model checking limitations.In this paper, we propose a novel approach to perform Computation Tree Logic (CTL) model checking based on the mathematical model of probe machine, which can verify all CTL properties.It can greatly reduce the verification time for systems with large state space.We develop a model checker called CTL2PROBE based on our approach and the experimental results show that our approach is better than NuSMV.

Safety is critical for the new technology of the communication-based train control (CBTC) system, the train-to-train CBTC (T2T-CBTC) system, which establishes direct communication between trains. In this paper, we define a parametric spatio-temporal hybrid modeling language (StHML(p)), focusing on the extension of spatio-temporal elements and probability parameters, to model the T2T-CBTC system. The parameters are risk states which come from the uncertain environment. To this end, we present a safety-risk prediction method based on a deep recurrent neural network for the T2T-CBTC system, which takes into account highly imbalanced data of the system, to predict the risk states through environment data. To verify StHML(p) model, we propose a mapping algorithm to transform StHML(p) into NSHA (Networks of Stochastic Hybrid Automaton) and employe the statistical model checker UPPAAL-SMC for verifying quantitative properties. Finally, we implement our approach in an T2T-CBTC system.

Deep Neural Networks (DNN) has gained great success in solving several challenging problems in recent years. It is well known that training a DNN model from scratch requires a lot of data and computational resources. However, using a pre-trained model directly or using it to initialize weights cost less time and often gets better results. Therefore, well pre-trained DNN models are valuable intellectual property that we should protect. In this work, we propose DeepTrace, a framework for model owners to secretly fingerprinting the target DNN model using a special trigger set and verifying from outputs. An embedded fingerprint can be extracted to uniquely identify the information of model owner and authorized users. Our framework benefits from both white-box and black-box verification, which makes it useful whether we know the model details or not. We evaluate the performance of DeepTrace on two different datasets, with different DNN architectures. Our experiment shows that, with the advantages of combining white-box and black-box verification, our framework has very little effect on model accuracy, and is robust against different model modifications. It also consumes very little computing resources when extracting fingerprint.

Model checking is a verification technique that explores all possible system states in a brute-force manner. However, the state space can be extremely large for many practical systems and the verification time grows exponentially with the size of systems. It is a major limitation for state-space search algorithms of model checking. This paper presents a novel approach to perform Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) model checking by using the connective probe machine, which is a fully parallel computing model. Our state-space search algorithm is based on the semantics of CTL properties and we design transformation algorithms to transform the model of a system into the structure that can run on the existing probe machine. We propose another approach to find multiple accepting cycles in linear time, which greatly shortens the verification time of LTL model checking. Compared to the traditional model checker, our approach can find multiple counterexamples according to the given property, which can trace as many system defects as possible. Simultaneously, it can greatly reduce the verification time for systems with large state spaces. We develop a model checker called MC2PROBE based on our approach and prove the feasibility and efficiency of our checker by experiments.

Analysis of spatial behaviors of safety-critical systems attracts more and more attention in the filed of cyber physical systems and image processing. The major problem is expressiveness and verifiability for modeling and analysis of spatial behaviors. In order to verify the satisfiability problem of spatial properties, in this paper, we propose a novel topometric model through inducing a topological space with metric distance. For the spatial logic, we specify spatial properties with S4u in continuous regions, which are encoded S4u formula to RCC-8 relations, and discrete spatial regions, whose evolution is achieved through extending S4u with spatial near and until, named S4ue. We present a spatial model checking algorithm to verify if an S4u spatial term or formula satisfies the topometric model. We exemplify the applicability of the approach on obstacle avoidance-based path planning of robots.

We study the use of Multiform Logical Time, as embodied in Esterel/SyncCharts and Clock Constraint Specification Language (CCSL), for the specification of assume-guarantee constraints providing safe driving rules related to time and space, in the context of Automated Driving Assistance Systems (ADAS). The main novelty lies in the use of logical clocks to represent the epochs of specific area encounters (when particular area trajectories just start overlapping for instance), thereby combining time and space constraints by CCSL to build safe driving rules specification. We propose the safe specification pattern at high-level that provide the required expressiveness for safe driving rules specification. In the pattern, multiform logical time provides the power of parameterization to express safe driving rules, before instantiation in further simulation contexts. We present an efficient way to irregularly update the constraints in the specification due to the context changes, where elements (other cars, road sections, traffic signs) may dynamically enter and exit the scene. In this way, we add constraints for the new elements and remove the constraints related to the disappearing elements rather than rebuild everything. The multi-lane highway scenario is used to illustrate how to irregularly and efficiently update the constraints in the specification while receiving a fresh scene.

Due to the mobility of autonomous vehicles and changing context through time, the constraints in safe driving rules specification need to be irregularly updated for monitoring the trajectory plan. This is not assumed in the Spatial-Temporal Logic. This paper proposes a novel approach to build the specification of assume-guarantee constraints providing safe driving rules related to time and space, in the context of Automated Driving Assistance Systems (ADAS). The novelty lies in that the specification adopts Multiform Logical Time to express the time constraints and provides spatial events generated by interactions on area trajectory for expressing space constraints. We propose the safe specification patterns at a high-level that provide the required expressiveness for safe driving rules. In these patterns, logical time provides the power of parameterization to express rules, before instantiation in low-level simulation contexts. The specification finally could be used to generate monitors that are executed on lower-level simulation engines with physical and topological features.

Low energy consumption and high reliability are widely identified as increasingly relevant issues in real-time systems on heterogeneous platforms. In this paper, we propose a multi-criteria optimization strategy to minimize the expected energy consumption while enforcing the reliability threshold and meeting all task deadlines. The tasks are replicated to ensure a prescribed reliability threshold. The platforms are composed of processors with different (and possibly unrelated) characteristics, including speed profile, energy cost and failure rate. We provide several mapping and scheduling heuristics towards this challenging optimization problem. Specifically, a novel approach is designed to control (i) how many replicas to use for each task, (ii) on which processor to map each replica and (iii) when to schedule each replica on its assigned processor. Different mappings achieve different levels of reliability and consume different amounts of energy. Scheduling matters because once a task replica is successful, the other replicas of that task are cancelled, which calls for minimizing the amount of temporal overlap between any replica pair. The experiments are conducted for a comprehensive set of execution scenarios, with a wide range of processor speed profiles and failure rates. The comparison results reveal that our strategies perform better than the random baseline, with a gain of 40% in energy consumption, for nearly all cases. The absolute performance of the heuristics is assessed by a comparison with a lower bound; the best heuristics achieve an excellent performance, with an average value only 4% higher than the lower bound.

In recent years, Deep Neural Networks (DNNs) have been experiencing rapid development and have been widely used in various fields. However, while DNNs have shown strong capabilities, their security problems have gradually been exposed. Therefore, the formal guarantee of neural network output is needed. Prior to the appearance of the Reluplex algorithm, the verification of DNNs was always a difficult problem. Reluplex algorithm is specially used to verify DNNs with ReLU activation function. This is an excellent and effective algorithm, but it cannot verify more activation functions. ReLU activation function will bring about "Dead Neuron" problem, and Leaky ReLU activation function can solve this problem, so it is necessary to verify DNNs based on Leaky ReLU activation function. Therefore, we propose the Leaky-Reluplex algorithm, which is based on the Reluplex algorithm. Leaky-Reluplex algorithm can verify DNNs based on Leaky ReLU activation function.

Combining spatial and temporal primitives together is quite useful to specify dynamic behaviors of cyber-physical systems. The ability to represent spatio-temporal properties by means of formulas in spatio-temporal logics has recently found important applications in various fields, such as runtime verification, parameter synthesis, contract-Based design. In this paper, we present a spatio-temporal specification language, STSL, by combining Signal Temporal Logic (STL) with a spatial logic S4u, to characterize spatio-temporal dynamic behaviors of cyberphysical systems. This language is highly expressive: it allows the description of quantitative signals, by expressing spatiotemporal traces over real valued signals in dense time, and Boolean signals, by constraining values of spatial objects across threshold predicates. STSL combines the power of temporal modalities and spatial operators, and enjoys important properties such as safety and liveness. We provide the falsification problem through extending Lemire's algorithm and a parameter synthesis procedure by calling the simulated annealing algorithm. We demonstrate the proposed approaches on adaptive cruise control system and path planning of quadrotors.

Describing spatio-temporal behaviors of cyber-physical systems attracts more and more attention in the filed of intelligent transportation systems and biological systems. The major problem is expressiveness and verifiability for modeling and analysis of spatio-temporal behaviors. In order to verify spatial and spatio-temporal behaviors, in this paper, we propose a methodology to model the evolution of spatial scene snapshots and verify the spatio-temporal models. Firstly, we define a novel Topograph through inducing Bigraph in topological space to characterize cyber-physical systems and verify the model against patterns specified with S4uformulas. Secondly, for spatio-temporal verification, we extend Topograph in dense time, named Temporal Topograph, to describe the evolution of spatial objects, which are verified against spatio-temporal specification language. We evaluate the applicability of the approach on CBTC-based intelligent transportation systems.

Although there has been substantial research in system analytics for risk assessment in traditional methods, little work has been done for safety risk prediction in communication-based train control (CBTC) system, especially intelligently predicting risk caused by the uncertainty in the system operation. Risk prediction and assessment of hazards in train control systems are vital for the safety and efficiency of urban rail transit. In this paper, we propose an intelligent hazard-risk prediction model based on a deep recurrent neural network for a new communication-mode CBTC system. First, a train-to-train communication-based train control (T2T-CBTC) system is proposed to improve the drawback of CBTC in information-exchanging mode. Then we design a risk prediction feature selection and generation method and estimate a critical function feature in the T2T-CBTC system by statistical model checking. Finally, we construct our intelligent hazard-risk prediction model based on a deep recurrent neural network using a long-short-term memory (LSTM) network. The model had excellent risk prediction classification results and performance in our experiment, even for unbalanced data set. This model consistently outperforms the deep belief network trained in Accuracy, Precision, Recall and F1-score for the hazard-risk prediction problem. Specifically, the mean accuracy is 97.2% and mean F1-score is 93.9% in overall performance of model. The improvements of our model against DBN model are 8.2% for Precision, 7% for Recall and 8% for F1-score.

As a widely used modeling language, AADL (Architecture Analysis and Design Language) plays an important role in designing safety-critical systems. It provides abundant components for describing system architecture and supports the early prediction and repetitive analysis of performance-critical attributes. However, the approach used by AADL to describe the system behavior is based mainly on automata theory; thus, encountering the state space explosion problem when modeling and verifying large and complex systems is inevitable. Furthermore, due to the lack of means to describe the behavior details, it is also difficult for AADL to support the accurate analysis and verification of functional and non-functional requirements. In this paper, we propose a language called RBML that supports refined behavior modeling to compensate for the behavior modeling and verification deficiencies of AADL. This new language is based on AADL but extends the ability to detail various behaviors and allows SMT (Satisfiability Modulo Theories) solvers to verify the constructed refined behavior model, thus alleviating the state space explosion problem to some extent. Experiments on Baidu Apollo are presented to demonstrate the feasibility of our proposed approach.

Neural network is one of the key technologies for deep learning. Experiments on some standard test datasets show that their recognition ability has reached the level of human beings. However, they are extremely vulnerable to adversarial examples, that is, adding some subtle perturbations to the input example can cause the model to give a wrong output with high confidence. In this paper, we propose a non-contact approach based on neural network and adversarial training to recognize the high-speed rail operating environment. We first built the environment dataset and trained neural network models to do the recognition. We found that our model had high prediction accuracy, but with poor security since it was easy to attack our model using Basic Iterative Methods (BIM). To improve its security, we performed adversarial training based on the adversarial training dataset we built. The evaluation experiments indicated that this approach could improve the security of our model at the same time ensuring the prediction accuracy on the original test dataset.

Ensure the correctness of safety critical systems play a key role in the worldwide software engineering. Over the past years we have been helping CASCO Signal Ltd which is the Chinese biggest high speed railway company to develop high speed railway safety critical software. We have also contributed specific methods for developing better safety critical software, including a search-based model-driven software development approach which uses SysML diagram refinement method to construct SysML model and SAT solver to check the model. This talk aims at sharing the challenge of developing high speed railway safety critical system, what we learn from develop a safety critical software with a Chinese high speed railway company, and we use ZC subsystem as a case study to show the systematic model-driven safety critical software development method.

This paper revisits the real-time scheduling problem recently introduced by Haque, Aydin and Zhu (2017). In this challenging problem, task redundancy ensures a given level of reliability while incurring a significant energy cost. By carefully setting processing frequencies, allocating tasks to processors and ordering task executions, we improve on the previous state-of-the-art approach with an average gain in energy of 20%. Furthermore, we establish the first complexity results for specific instances of the problem.

Specifying spatio-temporal aspects is one of the important areas in cyber-physical systems.Spatio-temporal logic with changes of truth value in discrete time and dense time has been researched, but a combination of spatial and temporal components with changes of spatial entities in dense time hasn't been well-done.The major problem is dense time and real-valued variables of the spatio-temporal properties of cyber-physical systems.In this paper, we propose a spatio-temporal specification language, named STSL, which integrates Signal Temporal Logic (STL) with a spatial logic S4u to deal with the changes of realvalues spatial entities in dense time.The combined language is divided into two formalisms, ST SLP C and ST SLOC , which is applied to interpret the Boolean semantics and quantitative semantics, respectively.The syntax of the two formalism and the corresponding semantics are provided.Besides, we present a Hilbert-style axiomatization for the proposed STSL and provide the soundness and completeness result by the spatio-temporal extension of maximal consistent set and canonical model.

Human-centric design is based on the psychological and physical needs of the human users. Model-driven engineering provides formal model to be analyzed. How to combine formal model with human-centric design methodology is a crucial issue and yet it has not been settled. In fact, the difficulty of this problem is lacking of formal representations of the human-centric property. The intention of our research is to provide some new approaches to effectively model and analyze the human-centric system. So we proposed model-based methodologies for modeling and analyzing the human-centric system, which aim to use hierarchical model framework to effectively build systems. This paper mainly addresses two issues. The first one is the modeling of human-centric system by the hierarchical model framework. Then we selected the automatic train control braking system as the application to build hierarchical model based on five corresponding sub-models and provide the new braking modes and new braking strategies.

Formal methods have been applied widely to verifying the safety requirements of communication-based train control (CBTC) systems, while the problem situations could be much simplified. In industrial practices of CBTC systems, however, huge complexity arises, which renders those methods nearly impossible to apply. In this paper, we aim to reduce the state space of formal verification problems in zone controller, a sub-system of a typical CBTC. We achieve the simplification goal by reducing the total number of device variables. To do this, two projection methods are proposed based on problem frames and constraints, respectively. The problem frame-based method decomposes the system according to sub-properties through functional decomposition, while the constraint-based projection method removes redundant variables. Our industrial case study demonstrates the feasibility through an evaluation, confirming that these two methods are effective in reducing the state spaces of complex verification problems in this application domain.

The MapReduce framework and its open source implementation Hadoop have established themselves as one of the most polular large data sets analyzers. They are widely used by many cloud service providers such as Amazon EC2 Cloud. However, while latency-sensitive applications becoming more and more important, Hadoop system shows its shortcoming in ensuring jobs completed on time. And currently, user has to provide a metric to evaluate the performance of different clients. Motivated by this, we proposed an algorithm CP-Scheduler (CPS) which uses a optimizer to analyze the best schedule in order to minimize the number of delayed jobs. Otherwise, as Hadoop System is not good at heterogeneous computing, our algorithm can also adapt different remote machines. These two features make it having better efficiency than the scheduler in Hadoop. The proposed algorithm is initially evaluated by a simulator which is designed for Hadoop. Experimental results show that the number of missing deadline jobs decrease by 60 percent on average in different sizes of situations.

The safety prediction of rail transit system is a fundamental problem in rail transit modeling and management. In this paper, we propose a safety prediction model based on deep learning for rail transit safety, which has been implemented as a deep belief network (DBN). It can learn effective features for rail transit prediction in an unsupervised fashion, which has been examined and found to be effective for many areas such as image and audio classification. To increase the accuracy of prediction, we introduce user satisfaction and rare-event probability, the new input prediction factors, into safety prediction. The former takes account of human and the latter is computed by statistic model checking. To show proof of the model, a real-world subway data sets based on the Beijing Metro in China is presented to demonstrate the feasibility of the model. Experiments on data sets show good performance of our prediction. These positive results demonstrate that deep learning and new factors are promising in rail transit research.

Interlocking system is an important module to ensure traffic safety. However it is still very difficult to apply automatic testing in industrial application. In this paper, we propose an approach to generate test case automatically with the help of SMT Solver. First, we extract the yard specification written by boolean expressions from interlocking rules and configuration specification. And then a process to generate test cases based on the specification is given. Finally, We apply our approach to the interlocking system at LongXiLu station in China.

For modelling hybrid systems, we have extended Event B based on its framework with the differential event. The differential event describes continuous behaviors of hybrid systems by differential equations and evolution constraint, whose proof obligations provide dynamical properties of a model. In order to ensure the safety and reliability of a model, proof obligations should be proved. It is difficult to prove proof obligation in state space, because there is no a complete method to solve differential equations in the field of mathematics. Thus we proposed an approach to proving proof obligation based on differential invariants. It is to avoid uncontrollable computation on solving differential equation. The main result is that we prove some theorems for proving proof obligations involving differential events within the framework of refinement calculus. Lastly, through the case of the Train Control System, we further show that the approach is well suited.

The integration of formal methods and requirements analysis increases the dependability of safety-critical systems. However it is still very difficult to obtain all of the safety requirements in practice, and formally construct the safety requirements model as well. In this paper, we propose an approach to capture safety requirements and formally describe them by classifying and developing safety requirements specification patterns. Our classification is a result of extracting safety properties from a variety of sources, such as interlocking tables and existing safety relevant functional requirements of railway interlocking system. They contain safety properties at analysis level and design level respectively. Furthermore, safety specification patterns based on the classification are used to formally describe and organize the safety requirements for formal verification. Finally, a tool called SRSV has been developed to enhance the process from deriving safety requirements to verifying. We applied it to the interlocking system at Mohe station in China, and the generated safety properties were then checked to hold by the verification tool.

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.

The safety properties of Cyber-Physical Systems have characteristics of both time and spatial attributes. Although various hybrid logic languages have been proposed to represent and reason both time and spatial attribute, most of them are not concerned on the quantitative problem which is important for mission-critical CPSs to specify and verify safety properties. In this paper, we propose a language named metric temporal-spatial logic (MTSL) to solve the problem. MTSL is the combination result of the metric temporal logic (MTL) and the spatial logic S4u. It can represent and reason CPS safety properties with both temporal and spatial attributes in a time quantitative manner. Based on different expressivity requirements, we define two kinds of MTSL languages named MTSLtPC and MTSLtOC. Their computational complexity of satisfiability problem are analysed. Moreover, in order to construct a decidable metric temporalspatial logic which can be used to define safety properties, we also point out that one may use safety metric temporal logic (SMTL) as the temporal language. The application of MTSLs are illustrated by case studies coming from transportation domain.

MARTE (Modeling and Analysis of Real-Time and Embedded Systems) is a profile of UML (United Modeling Language). MARTE provides support for specification, design and verification of real-time and embedded systems. Even though MARTE time model offers a support to describe multiform clocks, it lacks the ability to model both discrete and continuous behaviors of a hybrid system. To address the problem of hybrid systems modeling, we propose Hybrid MARTE which is an extension to MARTE for hybrid system modeling and analysis. Compare to MARTE, in Hybrid MARTE, we can construct the logical time and chronometric time in a unified way. Besides, a systemic framework for the modeling the requirements and design of a hybrid system is provided. Hybrid MARTE also provides multiple views modeling, something like UML. Hybrid MARTE Class Diagram can be used for description in static view, Hybrid MARTE Sequence Diagram in interactive view and Hybrid MARTE Statechart in dynamic behavioral view. HybridMARTE is successfully used in modeling and analysis of the Train Position Determination of railway control systems.

Energy consumption evaluation is one of the most important steps in Cyber-Physical Energy System (CPES) development. However, due to the lack of accurate and effective modeling and evaluation approaches considering the uncertainty of environment, it is hard to conduct the quantitative analysis for the energy consumption of CPESs. To address the above issue, this paper proposes an environment-aware energy consumption evaluation framework based on the Statistical Model Checking (SMC). In our framework, the environment uncertainty of CPESs is modeled using the Stochastic Hybrid Automata (SHA). In order to describe various environment modeling patterns, we create a collection of parameterized SHA models and save them to a domain specific environment ontology. Based on the domain environment ontology and user designs in the form of UML sequence diagrams and activity diagrams, our framework can automatically guide the construction of CPES models using networks of SHA and conduct the corresponding energy consumption evaluation. A case study based on an energy-aware building design demonstrates that our approach can not only support the accurate environment modeling with various uncertain factors, but also can be used to reason the relations between the energy consumption and environment uncertainties of CPES designs.

Modeling and Analysis of Real-Time and Embedded systems (MARTE) is a profile of United Modeling Language (UML), which provides support for specification, design and verification for Real-Time Embedded Systems (RTES). MARTE sequence diagram can deal with both discrete and dense time in which a clock can be either chronometric or logical. However it lacks the ability to describe the continuous behavior of a hybrid system. We propose a new method named Hybrid MARTE Sequence Diagram (HSD) to describe the communication between participants and the continuous evolution within the execution occurrence of a hybrid system. HSD combines the time model from MARTE and specification of the time-continuous behavior aspects from hybrid automata with MARTE sequence diagram. It improves the MARTE sequence diagram in that: the logical time and the chronometric time are unified. Besides, the description of continuous evolution of a hybrid system is provided. We firstly extend the basic MARTE elements to support both discrete and continuous aspects. Then we define the formal syntax and semantics of HSD based on hybrid transition system. Using this new method, we model an industrial application named Train Position Determination (TPD).

iCMTC is an advanced Communication Based Train Control system developed by CASCO Signal Ltd. For China's mass transit transportation. Some subsystems of iCMTC has been applied in Shanghai Metro Line 10. Zone Controller (ZC) is one of the subsystems of iCMTC. Modeling and verifying ZC is challenging due to the complexity of the block system and the behavior itself. We propose a formal approach to gradually specify the block system and lower complexity of the verification of ZC behavior. In recent years, there are many researches on railway systems. However, these studies use simple track networks, which makes them inadequate in industrial practice. To address this problem, we define specific block layouts (i.e., Double slip connection) as relations on sets. We also define mathematical properties of the relations so that the block system can be precisely described. For the purpose of reducing the complexity of verification, we propose an improved refinement mechanism based on the Event-B notation. Based on this refinement mechanism, we develop a Rodin plug-in to help us refine the system. We use this mechanism in modeling the ZC behavior, and achieve good results in automated proof. Several safety properties are considered and verified to ensure the safety and correctness of ZC.

Automation and high coverage are two essential industrial technical requirements of qualified testing method for safety-critical systems. The ioco-testing method is a sound and well-defined formal automation testing technique for labelled transition system. However, when we apply this method to a train control system developed by our industrial partner, we find that some testing requirements are not covered for certain testing objects. Further analysis has shown that the ioco-testing method only generates test cases based on explicit specified system behaviors which may result in low coverage when the implementation under test includes code branches used to deal with faults which can't be defined thoroughly in the specification in practices. Therefore, we propose a labelled transition system testing method based on specification mutation to improve safety-critical system testing coverage. We firstly define the mutation operators for the Input output symbolic transition system (IOSTS) modeling language, then we construct the corresponding test generation algorithm and translate the derived test cases into xml files which can be directly applied to the implementation under test in a simulation and test platform developed by our partner. Preliminary experiments on a safety-critical function named train position determination have shown about 28.5% improvement on the testing coverage.

The Problem Frames (PF) approach is a well-known approach for describing, analyzing and structuring problems in requirements engineering. It defines certain patterns of problems to be problem frames which have solutions. The real world problems are solved by decomposing to sub-problems which could be matched against problem frames. However, whether existing problem frames is enough for covering all problems is undecided. In this paper, we propose to recognize problem frames in a specific application domain by using feature models. As feature models could link to solution space, our approach bridges the gap between problem frames and solution space. The newly constructed problem frames could be used to analyse problems. We illustrate their usage by presenting a problem frames based problem analysis which include problem descriptions and matches. Because our new problem frames are high level, the real world problems do not need to be decomposed before matched.

The Clock Constraint Specification Language (CCSL) is a formal polychronous language based on the notion of logical clock. It defines a set of kernel constraints that can represent both asynchronous and synchronous relations. It was originally developed as part of the UML Profile for MARTE to express causal and temporal constraints of Real-time and Embedded Systems. In this paper, we explore the use of CCSL for modeling scheduling requirements and to conduct schedulability analysis. For this purpose, a dedicated scheduling library of CCSL has been built. This library is endowed with a state-based operational semantics, and is applied to solve issues related to schedulability analysis and latency-insensitive design. We establish schedulability categories and latency-insensitiveness property in the context of the semantics, and solve those issues by using model checking techniques.

Cyber-Physical Systems (CPSs) integrate computing, communication and control processes. Close interactions between the cyber and physical worlds occur in time and space frequently. Therefore, both temporal and spatial information should be taken into consideration when specifying properties of CPS systems for verification. However, how to formulate properties specifying spatial together with temporal features is still an unsolved problem in the CPS. In this paper, we propose an approach to analyze the spatio-temproal properties of CPS. A spatio-temporal logic is developed, including the syntax and semantics of the logic. With that logic, properties of both states, transitions and global systems could be specified, paving the way for further verification. To show the efficiency of the approach, a Train Control System is introduced as a case study. Meanwhile, more details about how to specifying properties of CPS systems with our method are elaborated.

AADL (Architecture Analysis and Design Language) is widely used in the area of modeling and analysis. However, it is not so convenient to describe a hybrid system with AADL. In this paper, we propose an approach to construct an annex of AADL, thus to facilitate the modeling and analysis of hybrid system. The syntax and semantics of hybrid AADL are provided. Additionally, we developed a hybrid system modeling plug-in to OSATE, which is an AADL supporting tool. Our approach, as well as our tool, is successfully used in the development of a lunar rover control system for the institute of China Aerospace Science and Technology.

In component-based architecture, a component is a unit of computation or a data store. Connectors are architectural building blocks used to model interactions among components. However, in some particular complex real-time systems, it is non-determinate and confused to distinguish some modules functioning as components as well as connectors. Therefore, a unified model method is demanded to describe those modules. In this paper, we propose a method to divide components into reactive and active component based on providing or requiring services when they interact with each other. A reactive component provides services and could call services of other reactive components. Active components call reactive components and are used to coordinate reactive components. Active and reactive timed automata are unified defined by extending timed automata to denote them. Then, we redefine the component composition language and present the semantics of composition of timed automata. A case study of Train Integrity Detection System illustrates the usage of our unified models for active and reactive components.

In the paper, we propose a method that can be applied to verify implementation in real-time reactive system. Different from other software model checking approaches, our method is based on testing. This approach allows the verification of safety property to be conducted directly on real code instead of models extracted from final implementation. Verifying that kind of models is a hard work and can only be applied to parts of the implementation. The method is done by establishing a connection between safety verification and conformance testing in real-time system. We first prove a theorem that in real-time system, under the input enabled precondition, if an implementation conforms to its specification and the specification satisfies the safety properties, the implementation satisfies it either. Then, based on contropositivity of the former conclusion, we present a test case generation framework which forms basis for generating test cases that can be used to detect violations of safety properties in the implementation. In addition, this test generation framework can also detect more nonconformance defects when compared with other real time test generation methods. The method is illustrated with a train gate control system.

Precisely describing complicate interaction process is still an open problem in MARTE(Modeling and Analysis of Realtime Embedded System). In this paper, we propose an approach to modeling interaction behaviors to enhance MARTE modeling ability. MARTE is published by OMG(Object Management Group) in Aug, 2010 as a standard modeling language for modeling real time and embedded system. Our approach is based on timed CSP(Communicating Sequential Processes). To describe the multiform time structure in MARTE, we make an extension to timed CSP. The syntax and semantics of the communicating process specification are given and also the laws, the trace model and the failures model are defined. One of the main advantages of our method is to help people to modeling the complicate interaction process with process algebra, thus to simplify the modeling and verification of the interaction and concurrent behaviors in real-time and embedded systems between different processes. The approach is applied to model and analyze a Train Over Speed Protection System for Shanghai Bell Company.

The specification of Modeling and Analysis of Real-time and Embedded Systems (MARTE) is an extension of UML in the domain of real-time and embedded Systems. However, unified modeling of continuous and discrete variables in MARTE is still an unsolved problem for hybrid real-time system development. In this paper we propose an extended statechart, Hybrid MARTE statechart, for modeling and analyzing of hybrid real-time and embedded systems. In Hybrid MARTE Statecharts, we unify the logical time and the chronometric time variables. The improvement of MARTE statechart is based on hybrid automata. Formal syntax and semantics of Hybrid MARTE statecharts are given based on labeled transition systems. At the end of this paper, a case study is given to show how to model the behavior of a Train Control System with Hybrid MARTE statecharts.

As the embedded systems are becoming more and more complex, requirements engineering approaches are needed for modeling requirements, especially the timing requirements. Among various requirements engineering approaches, the Problem Frames(PF) approach is particularly useful in requirements modeling for the embedded systems due to the characteristic that the PF pays special attention to the environment entities that will interact with the to-be software. However, no concern is given on timing requirements of the PF at present. This paper studies how to add timing constraints on problem domains in the PF. Our approach is to integrate the problem representation frame in the PF with the timing representation mechanism of MARTE(Modeling and Analysis of Real Time and Embedded systems). A unified problem frame modeling process integrated with timing constraints is provided, and problem frame requirements with timing constraints expressed by MARTE/CCSL(Clock Constraint Specification Language) and clock construction operators are obtained.

The Clock Constraint Specification Language (CCSL) provides expressions and relations to specify the time requirements and causal dependencies of systems. It was initially proposed, in the context of MARTE: the UML profile for Modeling and Analysis of Real-Time and Embedded Systems. In this paper, we propose a method to verify CCSL specifications. We give a formal state-based interpretation of a fundamental subset of CCSL clock constraints. Based on it, we translate a CCSL specification into a Promela model and feed the result into the model checker SPIN. Then we show some patterns for expressing the properties of the model and do the verification. A digital filter application is used as an example to illustrate the approach.

We have seen growing interest in validation of a business process model before it is implemented due to the complexity to model business process. In this paper, we propose a method for analyzing and validating the functional correctness of a business process model. Based on our previous work, we model a business process in UML activity diagrams with OCL constraints, then we give a formal semantics of the business process model, finally we validate the model by prototyping. We have developed a tool - AutoPA to support our method. When applying the tool, a business process model specified by UML activity diagrams with OCL constraints is transformed into an executable prototype in Java. Both the control flow dimension and the dataflow dimension of the model are considered. With the prototype, users can validate the functional properties of the business process model in an interactive way. We use a real-world example as a case study: the business process of the first delivery of mortgage archive in a risk mitigation system of a bank.

In this paper we propose an approach to check the compatibility of two services. The models of the services are built in finite state machine (FSM) and the behavior of services is described with the process of communicating sequential processes (CSP). An operator named corresponding position concurrency is defined to facilitate the calculation of composability of the paths which are obtained from processes, thus we can determine whether the two services are compatible or not. Simple examples are introduced to illustrate how to use this approach.

Assuring the consistency between collaborative services is a challenge problem in service oriented architecture. In this paper, we propose an approach to verifying the consistency of collaborative services based upon model checking. We first introduce an Extended UML Sequence Diagram for modeling dynamic behavior of collaborative service combining with UML State Chart Diagram. And then we define Collaboration-Contracts and obtain the verification model from the dynamic behavior models. Finally, wean automatically verify the consistency of collaborative services in behavior models by using an integrated SPIN-binding modeling tool Trustable MDA we developed to, In addition, a user-friendly service simulator is provided to locate the position of inconsistency.

In this paper, we present a method to measure the survivability of an object-oriented software in design phase. Each component is responsible for this measuring and the relations between components are based on the communication type. Each component can be characterized by a composite Petri net which combines the features of statechart and object diagram. A fuzzy number is introduced to this net to represent uncertain elements that might affect the survivability. Survival possibility theory has been used to produce survivability measure function for each component. A survivability measure index is defined for the system, and we proved that this index is monotonic.

This paper presents an approach to validation and verification of the WSCDL specification. In order to validate whether the CDL document is well defined or not, we introduce OCL to precisely describe the constraints which was expressed by natural language, and design a simple validator to check the static properties of the CDL document. The validator is created based on a Java model and the Java model is generated according to the UML diagrams with OCL constraints which is used to describe CDL specification. To verify the dynamic properties of CDL document, we model the behavior of CDL document with Java, so that Java Pathfinder model checker can be applied to check the desired properties. The assert activity is introduced to the CDL specification for describing the logic properties, to facilitate the verification process. A case study is given and it shows that our approach is both effective and practical. Moreover, this approach can check almost every kinds of CDL document, even the documents including exception block or finalize block.