Formal specification and refinement of a safe train control function

Motivated by the design and development challenges of the BART case study, an approach for developing and analyzing a formal model for reactive systems is presented. The approach makes use of a domain specific language for specifying control algorithms able to satisfy competing properties such as safety and optimality. The domain language, called SPC, offers several key abstractions such as the state, the profile, and the constraint to facilitate problem specification. Using a high-level program transformation system such as HATS being developed at the University of Nebraska at Omaha, specifications in this modelling language can be transformed to ML code. The resulting executable specification can be further refined by applying generic transformations to the abstractions provided by the domain language. Problem dependent transformations utilizing the domain specific knowledge and properties may also be applied. The result is a significantly more efficient implementation which can be used for simulation and gaining deeper insight into design decisions and various control policies. The correctness of transformations can be established using a rewrite-rule based induction theorem prover Rewrite Rule Laboratory developed at the University of New Mexico.

Adaptive fading Kalman filter with an application

A new adaptive state estimation algorithm, namely adaptive fading Kalman filter (AFKF), is proposed to solve the divergence problem of Kalman filter. A criterion function is constructed to measure the optimality of Kalman filter. The forgetting factor in AFKF is adaptively adjusted by minimizing the defined criterion function using measured outputs. The algorithm remains convergent and tends to be optimal in the presence of model errors. It has been successfully applied to the headbox of a paper-making machine for state estimation.

多移动机器人实时最优运动规划

研究多移动机器人的实时运动规划问题，提出了运动规划问题的体系结构，并将最优控制与智能决策相结合，建立实时专家系统，在其支持下，使机器人在时间—能量最优情况下完成规划策略。仿真结果表明该方法具有很强的实时性。