Analysis and verification of pointer programs are still difficult problems so far. This paper uses a shape graph logic and a shape system to solve these problems in two stages. First, shape graphs at every program poi...Analysis and verification of pointer programs are still difficult problems so far. This paper uses a shape graph logic and a shape system to solve these problems in two stages. First, shape graphs at every program point are constructed using an analysis tool. Then, they are used to support the verification of other properties （e.g., orderedness）. Our prototype supports automatic verification of programs manipulating complex data structures such as splay trees, treaps, AVL trees and AA trees, etc. The proposed shape graph logic, as an extension to Hoare logic, uses shape graphs directly as assertions. It can be used in the analysis and verification of programs manipulating mutable data structures. The benefit using shape graphs as assertions is that it is convenient for acquiring the relations between pointers in the verification stage. The proposed shape system requires programmers to provide lightweight shape declarations in recursive structure type declarations. It can help rule out programs that construct shapes deviating from what programmers expect （reflected in shape declarations） in the analysis stage. As a benefit, programmers need not provide specifications （e.g., pre-/post-conditions, loop invariants） about pointers. Moreover, we present a method doing verification in the second stage using traditional Hoare logic rules directly by eliminating aliasing with the aid of shape graphs. Thus, verification conditions could be discharged by general theorem provers.展开更多
This paper derives a distance-based formation control method to maintain the desired formation shape for spacecraft in a gravitational potential field. The method is an analogy of a virtual spring-damper mesh. Spacecr...This paper derives a distance-based formation control method to maintain the desired formation shape for spacecraft in a gravitational potential field. The method is an analogy of a virtual spring-damper mesh. Spacecraft are connected virtually by spring-damper pairs. Convergence analysis is performed using the energy method. Approximate expressions for the distance errors and control accelerations at steady state are derived by using algebraic graph representations and results of graph rigidity. Analytical results indicate that if the underlying graph of the mesh is rigid, the convergence to a static shape is assured, and higher formation control precision can be achieved by increasing the elastic coefficient without increasing the control accelerations. A numerical example of spacecraft formation in low Earth orbit confirms the theoretical analysis and shows that the desired formation shape can be well achieved using the presented method, whereas the orientation of the formation can be kept pointing to the center of the Earth by the gravity gradient. The method is decentralized, and uses only relative measurement information. Constructing a distributed virtual structure in space can be the general application area. The proposed method can serve as an active shape control law for the spacecraft formations using propellantless internal forces.展开更多
A graph G is said to be determined by its spectrum if any graph having the same spectrum as G is isomorphic to G. An H-shape is a tree with exactly two of its vertices having maximal degree 3. In this paper, a formula...A graph G is said to be determined by its spectrum if any graph having the same spectrum as G is isomorphic to G. An H-shape is a tree with exactly two of its vertices having maximal degree 3. In this paper, a formula of counting the number of closed 6-walks is given on a graph, and some necessary conditions of a graph Γ cospectral to an H-shape are given.展开更多
传统的交变磁场测量(Alternating current field measurement,ACFM)技术具有缺陷定量准确、无需接触等优点,但是不能检测深层缺陷;脉冲涡流检测技术(Pulsed eddy current testing,PECT)具有较好的深层缺陷检测能力,但由于采用瞬态响应...传统的交变磁场测量(Alternating current field measurement,ACFM)技术具有缺陷定量准确、无需接触等优点,但是不能检测深层缺陷;脉冲涡流检测技术(Pulsed eddy current testing,PECT)具有较好的深层缺陷检测能力,但由于采用瞬态响应信号分析方法,容易受到提离效应干扰,工程实际应用较为困难,并且定量能力弱于ACFM技术。结合ACFM和PECT的优势,提出了脉冲交变磁场测量技术(Pulsed alternating current field measurement,PACFM)。该技术采用脉冲周期信号作为激励信号源,基于瞬态脉冲响应信号,采用三维场量测量和瞬态信号分析相结合的方法实现缺陷识别与定量评估。对瞬态响应信号中能够表征磁场变化规律的特征量进行提取,通过研究发现PACFM不仅具有与ACFM等同的表面缺陷检测能力,而且具有优异的深层缺陷识别与定量评估能力,抗干扰能力强,具有较高的应用价值和前景。展开更多
基金supported by the National Natural Science Foundation of China under Grant Nos.61003043,61170018the National High Technology Research and Development 863 Program of China under Grant No.2012AA010901-2the Postdoctoral Science Foundation of China under Grant No.2012M521250
文摘Analysis and verification of pointer programs are still difficult problems so far. This paper uses a shape graph logic and a shape system to solve these problems in two stages. First, shape graphs at every program point are constructed using an analysis tool. Then, they are used to support the verification of other properties （e.g., orderedness）. Our prototype supports automatic verification of programs manipulating complex data structures such as splay trees, treaps, AVL trees and AA trees, etc. The proposed shape graph logic, as an extension to Hoare logic, uses shape graphs directly as assertions. It can be used in the analysis and verification of programs manipulating mutable data structures. The benefit using shape graphs as assertions is that it is convenient for acquiring the relations between pointers in the verification stage. The proposed shape system requires programmers to provide lightweight shape declarations in recursive structure type declarations. It can help rule out programs that construct shapes deviating from what programmers expect （reflected in shape declarations） in the analysis stage. As a benefit, programmers need not provide specifications （e.g., pre-/post-conditions, loop invariants） about pointers. Moreover, we present a method doing verification in the second stage using traditional Hoare logic rules directly by eliminating aliasing with the aid of shape graphs. Thus, verification conditions could be discharged by general theorem provers.
基金supported by the National Natural Science Foundation of China (Nos. 61273351 and 61673390)
文摘This paper derives a distance-based formation control method to maintain the desired formation shape for spacecraft in a gravitational potential field. The method is an analogy of a virtual spring-damper mesh. Spacecraft are connected virtually by spring-damper pairs. Convergence analysis is performed using the energy method. Approximate expressions for the distance errors and control accelerations at steady state are derived by using algebraic graph representations and results of graph rigidity. Analytical results indicate that if the underlying graph of the mesh is rigid, the convergence to a static shape is assured, and higher formation control precision can be achieved by increasing the elastic coefficient without increasing the control accelerations. A numerical example of spacecraft formation in low Earth orbit confirms the theoretical analysis and shows that the desired formation shape can be well achieved using the presented method, whereas the orientation of the formation can be kept pointing to the center of the Earth by the gravity gradient. The method is decentralized, and uses only relative measurement information. Constructing a distributed virtual structure in space can be the general application area. The proposed method can serve as an active shape control law for the spacecraft formations using propellantless internal forces.
文摘A graph G is said to be determined by its spectrum if any graph having the same spectrum as G is isomorphic to G. An H-shape is a tree with exactly two of its vertices having maximal degree 3. In this paper, a formula of counting the number of closed 6-walks is given on a graph, and some necessary conditions of a graph Γ cospectral to an H-shape are given.
文摘传统的交变磁场测量(Alternating current field measurement,ACFM)技术具有缺陷定量准确、无需接触等优点,但是不能检测深层缺陷;脉冲涡流检测技术(Pulsed eddy current testing,PECT)具有较好的深层缺陷检测能力,但由于采用瞬态响应信号分析方法,容易受到提离效应干扰,工程实际应用较为困难,并且定量能力弱于ACFM技术。结合ACFM和PECT的优势,提出了脉冲交变磁场测量技术(Pulsed alternating current field measurement,PACFM)。该技术采用脉冲周期信号作为激励信号源,基于瞬态脉冲响应信号,采用三维场量测量和瞬态信号分析相结合的方法实现缺陷识别与定量评估。对瞬态响应信号中能够表征磁场变化规律的特征量进行提取,通过研究发现PACFM不仅具有与ACFM等同的表面缺陷检测能力,而且具有优异的深层缺陷识别与定量评估能力,抗干扰能力强,具有较高的应用价值和前景。
