Abstract:With the rapid development of aviation models, the degree of digitalization of avionics systems becomes higher and higher, and the proportion of the software in those systems becomes larger and larger. In this paper, software architecture and formal modeling of avionics systems are discussed. Further, a system level integrated testing method based on formalization for avionics system from static and dynamic aspects is proposed. At last, the effectiveness of the proposed approach is evaluated through an integrated testing system designed and implemented in this research.

Abstract:This paper presents a formal verification method for AADL (architecture analysis and design language) models by TASM (timed abstract state machine) translation. The abstract syntax of the chosen subset of AADL and of TASM are given. The translation rules are defined clearly by the semantic functions expressed in a ML-like language. Furthermore, the translation is implemented in the model transformation tool AADL2TASM, which provides model checking and simulation for AADL models. Finally, a case study of space GNC (guidance, navigation and control) system is provided.

Abstract:State transition matrix (STM), designed for modeling software system, is a table-based modeling language in which the front-end is expressed in the table form and the back-end has strict formalized definition. At present, however, STM has no time semantics, which greatly limits the application of this method in real-time embedded software modeling. In order to solve this problem, this paper proposes a time STM (TSTM) modeling method attained by adding time semantics and constraint for each cell in STM, making it suitable for describing real-time system behavior. In addition, a time computation tree logic (TCTL) model checking method is presented based on bounded model checking (BMC) technology for verification of time and logic properties of TSTM model. At last, the effectiveness of the proposed method is validated by modeling and verifying certain type train control software.

Abstract:With the rapid development of computer technology, computer systems have been widely used in the safety-critical field where software systems are important enabling components. In computer systems, device drivers act as the bridge between software and devices. Due to the complexity resulted from the fact that device drivers are associated with platforms, operating systems and devices all together, the development of device drivers is very difficult and costly. Errors and faults in device drivers often lead to system failures, causing irreparable damage to the safety-critical applications. Aiming at the assurance of reliability and correctness, the paper presents a survey of related methods and techniques from three aspects: failure isolation and recovery, correctness analysis and verification, model based design and complexity control. The mainstream methods and techniques are evaluated with their pros and cons, which lays the foundation for the further research.

Abstract:Data flow related faults are very common in program and difficult to locate. This paper proposes a data chain model that takes account of variable change and dependencies information, and puts forward a fault location approach based on the data chain model. The main research of this paper is verified by experiments. The experimental results show that the proposed approach achieves better results comparing with other fault location approaches such as DU-pair, program slice, PPDG, and statement coverage.

Abstract:The train control system is a safety-critical system. To assure its safety, it requires the testing process to cover all possible runs in its safety-critical scenarios. Existing methods of scenario modeling and test case generation cannot completely satisfy the requirement. The paper focuses on the methods of modeling safety-critical scenarios in train control system and the tools for automatically generating test cases for the system. UML activity diagram is extended with event-driven and time characteristic description mechanism to satisfy the requirement of modeling safety-critical scenarios. A simple path coverage criterion is also proposed to define the coverage of all possible runs in a scenario and a method is provided for automatic test case generation. The experiment on ground train control system shows the effectiveness and limitation of the proposed method.

Abstract:As multiprocessor real-time systems are increasingly applied in safety critical systems, it's important to ensure the correctness of such systems. One key attribute of the correctness of real-time system is the schedulability that guarantees to satisfy the timing requirements. The traditional methods for determining the schedulability are either pessimistic or unsafe. To tackle the drawbacks of those methods, this paper proposes a scheme to achieve the schedulability analysis using model checking. It provides a schedulability analysis framework for multiprocessor real-time system. All the components involved in the schedulability of the system, including the tasks, the execution infrastructure and the dispatching management unit, are modeled as timed automata and implemented in UPPAAL. Further, UPPAAL is employed to verify whether the schedulability property is always satisfied. Symbolic model checking is applied to determine schedulability. However, because of the over-approximation for stopwatches, symbolic model checking cannot be used to disprove schedulability. As a supplement, statistical model checking is used to estimate the probability of non-schedulability and generate concrete counterexamples going along with non-schedulability. Statistical model checking is also used to obtain some performance information when system is schedulable.

Abstract:Termination of multipath loop programs with one variable is analyzed in this paper. It demonstrates that under proper conditions, this kind of loops is non-terminate if and only if there exist fixed points. Especially, if the class of programs are polynomial, then under proper conditions, the termination of the programs is decidable over the reals.

Abstract:In open environment, the stochastic behavior of safety-critical system may lead to occurrence of rare-event, which is critical to the system's reliability. It is very important to estimate the probability of rare-event occurrence. Statistical model checking (SMC) is a simulation-based model checking technology, which integrates the simulation and statistical analysis technique to improve the efficiency of traditional model checking. SMC is used to verify and estimate the reliability of complex safety-critical system. However, the most challenging problem is that it is impossible to estimate and predict the probability of rare-event based on SMC with the acceptable sample size. To solve this problem, this study proposes an improved statistical model checking framework, designs and develops a statistical model checker based on machine learning to estimate and predict the probability of rare-event with fewer sample size. To demonstrate the presented approach, a case study on collision avoidance system in CBTC is discussed. The analysis results show that the proposed approach is feasible and efficient.

Abstract:The success of aerospace depends on the correctness of aerospace embedded software. Such embedded software are usually period-driven and can be decomposed into different modes with each mode representing a system state observed from outside. Such software may also involve intensive computing in their modes. Currently, there is lack of domain-specific formal modeling languages for such software in the relevant industry. To address this problem, this article proposes a formal visual modeling approach called SPARDL as a concise and precise way to specify such software. To capture the temporal properties of aerospace embedded software, a property specification language is provided based on interval logic. To support application in industry, code generation methodology is also discussed. This modeling approach is applied in some real-life cases in aerospace industry.

Abstract:Lustre is a synchronous dataflow language widely used in safety critical industrial control system. Formal verification is efficient to improve the reliability of the compiler which translates Lustre to C. Based on this approach, this paper conducts a research on the trustworthy compiler for translating Lustre*(a Lustre-like language) to Clight (a subset language of C). The entire compiling process is divided into different stages to tackle the large difference between Lustre* and Clight. Each stage performs a specific translation task. This paper describes a translation algorithm which eliminates high-order operations. The implementation of translation process is assisted by theorem proving tool Coq, and a strict proof of correctness of the process is also provided.

Abstract:This article proposes a clone detection method based on a program characteristic metrics. Though analyzing the syntax and semantic characteristics of vulnerabilities, this detection method abstracts certain key nodes which describe different forms of vulnerability type from syntax parser tree, and expands four basic types of code clone to auxiliary classes. The characteristic metrics of the code then is finalized by obtaining the number of key nodes which are calculated via scanning corresponding code segment in the syntax parser tree. The clone detection based on a characteristic metrics creates basic knowledge base by extracting partial instances of open vulnerability database, and precisely locates the vulnerability codes by performing cluster calculation on the same codes responding to multiple types of code clone. Comparing with the detection method based on single characteristic vector, the proposed method produces more precise description about vulnerability. This detection method also offers a remedy to the drawbacks of formal detection method on its vulnerability type covering ability. Nine vulnerabilities are detected in an android-kernel system test. Testing on software of different code sizes shows that the performance of this method is linear with the size of the code.

Abstract:This paper introduces Micro-Dalvik, a formalized Dalvik-like VM model to exhibit core features of the register-based architecture. This formal specification describes the instruction set and runtime state, and the runtime behaviors of the instructions as state transitions based on big-step operational semantics. The Micro-Dalvik VM instruction set is more abstract than comparable Dalvik VM to attain clarity of its semantics, but bears no further simplification of the meaning of instructions. Some properties of Micro-Dalvik VM semantics are stated based on this formal specification and sketch of the proofs is provided. This formalization is implemented in the theorem proof assistant Isabelle/HOL.

Abstract:Cyber physical systems (CPS) typically employ real-time multitasking systems as their control software. This paper proposes an approach to formally analyzing such control software using statistical model checking of UPPAAL. The main contribution of this study is a model in timed automata which modularly describes the major components of a multitasking system. The model supports the analysis of timing-related functional properties as well as schedulability analysis, and can easily be adapted and extended for verifying different properties of various multitasking systems. A case study on an early version of the Chinese Lunar Rover control software shows that the proposed method is able to track down undesired behavior in real-world industrial CPS.

Abstract:Program spectrum based dynamic fault localization is an active research topic in the domain of software automatic debugging. It aims to localize pontential faults in a faulty program based on a specific model which is constructed on execution behaviors and results of test cases. This survey offers a systematic overview of existing research achievements of the domestic and foreign researchers in recent years. First, some preliminary knowledge and basic assumptions are presented. Next, a research framework is proposed and important influencing factors which can affect the effectiveness of fault localization are identified. These factors include program spectrum construction, test suite maintenance and composition, number of faults, test case oracle, user feedback, and fault removal cost. In addition, the evaluation metrics and subject objects used in previous empirical studies are analyzed. Furthermore, classical applications of fault localization in some specific application domains are summarized. Finally a perspective of the future work in this research area is discussed.

Abstract:In C/C+ language, limited rages represented by integer types and castings between different signs or widths cause integer-based weakness, including integer overflow, integer underflow, signedness error and truncation error. Attackers usually exploit them indirectly to commit damaging acts such as arbitrary code execution and denial of service. This paper presents a survey on integer-based vulnerabilities. A novel security model is proposed in view of behaviors resulting from the weakness occurrence, and the sufficient conditions in determining integer-based vulnerabilities are also presented. A thorough comparison among detecting methods is further conducted in consideration of covering sufficient conditions. Through an empirical study on real-world integer bug cases, the characteristics and distributions are discussed. Finally, the challenges and research directions of integer-based vulnerabilities are explored.

Abstract:State/Event fault tree (SEFT) is a modeling technique for describing the causal chains which lead to failure in component-based embedded systems, and the top event of SEFT describes the result of the failure. One important way for capturing the mean time parameter of system failure is to quantitatively analyze the mean time of the top event occurrence, which provides support for system safety evaluation. However, it is necessary to formally describe SEFT semantics in order to quantitatively analyze the time property. In this paper, a time property analysis method for SEFT based on interactive Markov chain (IMC) is presented. Firstly, interface interactive Markov chain (Interface-IMC) is proposed based on refining the interactive action of IMC. Secondly, semantics of components and logic gates in SEFT are formally described by Interface-IMC. Thirdly, the semantics of SEFT is obtained by composing all the Interface-IMCs generated in the above steps. During this process, weak bisimilarity technique is applied to reduce state space. Then, a quantitative time analysis method is presented based on the formal semantic model of SEFT. Finally, the time analysis processes for the SEFT of aircraft radar landing control system and sprinkler system are illustrated by the proposed method. The method provides a new solution for analyzing time properties of component-based system failure.