Mixed-type decision-making is ubiquitously required in robotic systems and has attracted significant research interests. Examples include, but not limited to, the integrated task and motion planning and optimal control of hybrid systems involving both continuous and discrete dynamic behaviors. For decision-making of robotic systems to improve operational efficiency, safety, and/or mission success rate, they involve both discrete variables representing task allocation or transitions between discrete modes and continuous variables representing trajectories of the planned motion or states governed by differential equations. This paper formulates a class of mixed-type decision-making problems with polynomial objective and constraints as quadratically constrained quadratic programming (QCQP) problems and a nonconvex optimization method based on alternating direction method of multipliers is proposed to solve the QCQP. The proposed optimization method consists of three sequential subproblems, all of which admit closed-form solutions. Moreover, convergence proof of the optimization algorithm is provided. Two representative problems, traveling salesman with obstacle avoidance and rendezvous and docking of a charging station with distinct phase constraints, are described and solved via the proposed method. Numerical simulations as well as experimental verification of both problems are presented and compared with a state-of-art method to validate the effectiveness, efficacy and robustness of the nonconvex optimization method.
The Speci cation and Analysis of Requirements (SpeAR) tool is a requirements prototyping and analysis tool based on the formal semantics of the Lustre language. It features a domain speci c language that formally captures functional requirements of systems or software. Once formalized, requirements can be analyzed to demonstrate correct- ness, consistency, and traceability using in nite-state model checking tools, such as JKind. The formal notation and analyses that SpeAR supports can be used to automate activities related to certi cation of safety critical software as suggested by DO-178C: Software Considera- tions in Airborne Systems and Equipment Certi cation. This standard de nes a rigorous software development process that ensures that soft- ware development activities produce object code that implement sys- tem requirements correctly, while introducing no additional functional- ity. Recent updates to the guidance allow for the use of formal methods to satisfy DO-178C certi cation objectives as outlined in DO-333: For- mal Methods Supplement to DO-178C and DO-278A. This paper walks through an e ort in which SpeAR is used to automate certi cation ac- tivities for production avionics software. It focuses on the use of SpeAR to address veri cation objectives related to the software design artifacts of DO-178C, replacing manual peer review activities with more rigorous formal-methods based analyses.
Avionics-related systems and the procedures for interacting with them appear to be growing in complexity. This trend places a larger burden on pilots to manage increasing amounts of information and to understand system interactions. The result is an increase in the likelihood of loss of airplane state awareness (ASA). One way to gain more insight into this issue is through experimentation using objective measures of visual behavior. This study summarizes an analysis of oculometer data obtained during a high-fidelity flight simulation study that included a variety of complex pilot-system interactions that occur in current flight decks, as well as several planned for the next generation air transportation system. The study was comprised of various scenarios designed to induce low and high energy aircraft states coupled with other emulated causal factors in recent accidents. Three different display technologies were evaluated in this recent pilot-in-the-loop study conducted at NASA Langley Research Center. These technologies include a stall recovery guidance algorithm and display concept, an enhanced airspeed control indication of when the automation is no longer actively controlling airspeed, and enhanced synoptic diagrams with corresponding simplified electronic interactive checklists. Multiple data analyses were performed to understand how the 26 participating airline pilots were observing ASA-related information provided during different stages of flights and in response to specific events within these stages.
We investigate the challenging problem of integrating detection, signal processing, target tracking, and adaptive waveform scheduling with lookahead in urban terrain. We propose a closed-loop active sensing system to address this problem by exploiting three distinct levels of diversity: (1) spatial diversity through the use of coordinated multistatic radars; (2) waveform diversity by adaptively scheduling the transmitted waveform; and (3) motion model diversity by using a bank of parallel filters matched to different motion models. Specifically, at every radar scan, the waveform that yields the minimum trace of the one-step-ahead error covariance matrix is transmitted; the received signal goes through a matched-filter, and curve fitting is used to extract range and range-rate measurements that feed the LMIPDA-VSIMM algorithm for data association and filtering. Monte Carlo simulations demonstrate the effectiveness of the proposed system in an urban scenario contaminated by dense and uneven clutter, strong multipath, and limited line-of-sight.
JKIND is an open-source industrial model checker developed by Rockwell Collins and the University of Minnesota. JKIND uses multiple parallel engines to prove or falsify safety properties of infinite state models. It is portable, easy to install, performance competitive with other state-of-the-art model checkers, and has features designed to improve the results presented to users: inductive validity cores for proofs and counterexample smoothing for test-case generation. It serves as the back-end for various industrial applications.
