Protocol reverse engineering (PRE) aims to infer the specification of network protocols when the source code is not available. Specifically, field inference is one crucial step in PRE to infer the field formats and semantics. To perform field inference, binary analysis based PRE techniques are one major approach category. However, such techniques face two key challenges --- (1) the format inference is fragile when the logics of processing input messages may vary among different protocol implementations, and (2) the semantic inference is limited by inadequate and inaccurate inference rules.

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.

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.

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.

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.

Testing is an essential part of the software development of Safety-Critical Systems (SCSs). Since it can automatically generate test cases using the system requirement models, Model-Based Testing (MBT) is suitable for SCSs. However, most of the existing system modeling languages for SCSs mainly focus on representing functional requirements rather than safety, e.g., SysML. In this paper, we first propose a modeling language, Safety SysML State Machine (S2MSM), to guarantee safety during the requirement modeling stage. Second, we propose a model transformation algorithm to transform the S2MSM model into an intermediate model. Then, we design a time flow operation sequence that simulates the external real-time environment. Finally, we generate test cases from the intermediate model according to the MC/DC criterion and time flow operation sequence. We conduct a case study on a real-world SCS application to demonstrate the effectiveness and efficiency of the proposed 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.

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.

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.

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.

In requirements engineering (RE), there are three essential descriptions, i.e., requirements, specification and domain properties. Their relationship is proposed by Jackson et al, and verified in various requirements approaches. However, at present, there is no formal verification for the relationship in the Problem Frames (PF) which is a well known approach in the RE. Our previous work based on the PF explicitly captures the three descriptions. Based on that work, this paper further formalizes the three descriptions using Communicating Sequential Process (CSP), transforms the relationship into two "refines", and verifies them with Process Analysis Tool (PAT). The verification ensures that the machine which behaves as in the specification installed in a specific domain will satisfy the requirements.

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.

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.

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.

For many old buildings in the world, due to the legacy devices problem, it is hard to supply appropriate energy for them.In order to reduce the energy consumption of buildings under the premise of satisfying user requirements, we use software control systems whose core part is the scheduling strategy, to reconstruct them.It is time consuming to choose a good scheduling strategy due to many uncertain factors, among which user actions are of the most influence.In this paper, we propose an Support Vector Machine (SVM) based approach to explore the relation between user action and the best scheduling strategy of a control system.The main contributions include:(1) obtaining the sample set by collecting data at the model level using Statistical Model Checking (SMC) based method; (2) using SVM algorithm to learn the relation model between user actions and the best scheduling strategies; and (3) applying the relation model to predict a best scheduling strategy.Finally a real case study is conducted showing the efficiency of our approach.

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.

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).

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.

It is well acknowledged that environment plays an important role in requirement derivation. However, at present the time-continuous properties of the environment are of little concern. Our previous work modeled the time-continuous environment by constructing a software environment ontology. This paper further presents an approach for deriving software requirements specification with time using software environment ontology. Experiments are conducted by deriving different software requirement specifications under different situations. They are simulated with Simulink. The simulation results show that the software behaviors can be more accurately determined with respect to time-continuous environment by using time as a measurement.

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.