The three-axis active attitude control method with a momentum wheel and magnetic coils for a pico-satellite is considered. The designed satellite is a 2.5 kg class satellite stabilized to nadir pointing. The momentum ...The three-axis active attitude control method with a momentum wheel and magnetic coils for a pico-satellite is considered. The designed satellite is a 2.5 kg class satellite stabilized to nadir pointing. The momentum wheel performs a pitch-axis momentum bias, nominally spinning at a particular rate. Three magnetic coils are mounted perpendicularly along the body axis for precise attitude control through the switch control mechanism. Momentum wheel start up control, damping control and attitude acquisition control are considered. Simulation results show that the proposed combined control laws for the pico-satellite is reliable and has an appropriate accuracy under different separation conditions. The proposed strategy to start up the wheel after separation from the launch vehicle shows that its pitch momentum wheel can start up successfully to its nominal speed from rest, and the attitude convergence can be completed within several orbits, depending on separation conditions.展开更多
Checking whether a given formula is an invariant at a given program location(especially,inside a loop) can be quite nontrivial even for simple loop programs,given that it is in general an undecidable property.This is ...Checking whether a given formula is an invariant at a given program location(especially,inside a loop) can be quite nontrivial even for simple loop programs,given that it is in general an undecidable property.This is especially the case if the given formula is not an inductive loop invariant,as most automated techniques can only check or generate inductive loop invariants.In this paper,conditions are identified on simple loops and formulas when this check can be performed automatically.A general theorem is proved which gives a necessary and sufficient condition for a formula to be an invariant under certain restrictions on a loop.As a byproduct of this analysis,a new kind of loop invariant inside the loop body,called inside-loop invariant,is proposed.Such an invariant is more general than an inductive loop invariant typically used in the Floyd-Hoare axiomatic approach to program verification.The use of such invariants for program debugging is explored;it is shown that such invariants can be more useful than traditional inductive loop invariants especially when one is interested in checking extreme/side conditions such as underflow,accessing array/collection data structures outside the range,divide by zero,etc.展开更多
基金supported by the Program for New Century Excellent Talents in University (No. NCET-06-0514), Chinathe Postdoctoral Science Foundation of China (Nos. 20081458 and 20080431306)
文摘The three-axis active attitude control method with a momentum wheel and magnetic coils for a pico-satellite is considered. The designed satellite is a 2.5 kg class satellite stabilized to nadir pointing. The momentum wheel performs a pitch-axis momentum bias, nominally spinning at a particular rate. Three magnetic coils are mounted perpendicularly along the body axis for precise attitude control through the switch control mechanism. Momentum wheel start up control, damping control and attitude acquisition control are considered. Simulation results show that the proposed combined control laws for the pico-satellite is reliable and has an appropriate accuracy under different separation conditions. The proposed strategy to start up the wheel after separation from the launch vehicle shows that its pitch momentum wheel can start up successfully to its nominal speed from rest, and the attitude convergence can be completed within several orbits, depending on separation conditions.
基金supported by NSFC-90718041NKBRPC-2005C B321902+1 种基金China Scholarship Council in Chinasupported by the National Science Foundation award CCF-0729097
文摘Checking whether a given formula is an invariant at a given program location(especially,inside a loop) can be quite nontrivial even for simple loop programs,given that it is in general an undecidable property.This is especially the case if the given formula is not an inductive loop invariant,as most automated techniques can only check or generate inductive loop invariants.In this paper,conditions are identified on simple loops and formulas when this check can be performed automatically.A general theorem is proved which gives a necessary and sufficient condition for a formula to be an invariant under certain restrictions on a loop.As a byproduct of this analysis,a new kind of loop invariant inside the loop body,called inside-loop invariant,is proposed.Such an invariant is more general than an inductive loop invariant typically used in the Floyd-Hoare axiomatic approach to program verification.The use of such invariants for program debugging is explored;it is shown that such invariants can be more useful than traditional inductive loop invariants especially when one is interested in checking extreme/side conditions such as underflow,accessing array/collection data structures outside the range,divide by zero,etc.
