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.

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.

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.

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.

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.