Autonomous systems will soon be ubiquitous in our society, saving us time, performing tasks we do not want to do, caring for us and keeping us safe. Autonomous robots in homes and businesses are already cleaning floors, mowing lawns, delivering meals and packages, and the technology is now driving cars and trucks. Though they will soon be common occurrences in everyday life, assuring their safety, privacy and security is still a huge challenge. A number of autonomous car accidents have occurred after millions of miles of testing, and injuries regularly occur from other types of autonomous systems. Assuring the proper behavior and safety of autonomous systems is an important endeavor to reduce risks in using them. This monograph discusses assurance for autonomous systems, the different approaches to assuring autonomy, formal analysis, cybersecurity, certification and research challenges. The monograph starts with a brief introduction to assured autonomy, providing definitions and key terms. Thereafter, an overview of assured autonomy and different aspects of system and software assurances are provided, and Section 3 discusses governance, trust, ethics and privacy of autonomous systems. Section 4 covers assuring the correct operation of autonomous systems, which can be done through techniques such as formal verification, testing and monitoring. The monograph then describes certification of current systems and proposals for certifying autonomous systems, providing an example of the certification of aircraft software and multiple proposals for how autonomous systems could be certified. Lastly, areas of research in assuring autonomous systems are covered.
The security of computer networks is critical to our nation's civil and military infrastructure. Eliminating vulnerabilities in network software will significantly improve security of our computer and military systems. The Automatic Generation of Network Element Software (AGNES) code generator will generate network element software that is free from known weaknesses which in turn will reduce vulnerabilities. AGNES uses an ontology of coding solutions based on network element standards and the Common Weakness Enumeration (CWE) database to avoid common weaknesses. The generated software will be put through rigorous static analysis to validate the absence of known weaknesses. The generated code will be compared to open source software for comparison of code quality, functionality and performance.
This paper represents a new contribution to the growing literature on memes. While most memetic thought has been focused on its implications on humans, this paper speculates on the role that memetics can have on robotic communities. Though speculative, the concepts are based on proven advanced multi agent technology work done at NASA - Goddard Space Flight Center and Lockheed Martin. The paper is composed of the following sections : 1) An introductory section which gently leads the reader into the realm of memes. 2) A section on memetic engineering which addresses some of the central issues with robotic learning via memes. 3) A section on related work which very concisely identifies three other areas of memetic applications, i.e., news, psychology, and the study of human behaviors. 4) A section which discusses the proposed approach for realizing memetic behaviors in robots and robotic communities. 5) A section which presents an exploration scenario for a community of robots working on Mars. 6) A final section which discusses future research which will be required to realize a comprehensive science of robotic memetics.
Adaptive systems are critical for future space and other unmanned and intelligent systems. Verification of these systems is also critical for their use in systems with potential harm to human life or with large financial investments. Due to their nondeterministic nature and extremely large state space, current methods for verification of software systems are not adequate to provide a high level of assurance for them. The combination of stabilization science, high performance computing simulations, compositional verification and traditional verification techniques, plus operational monitors, provides a complete approach to verification and deployment of adaptive systems that has not been used before. This paper gives an overview of this approach.
The use of swarm technologies has become prevalent in a variety of application domains: medical, bioinformatics, military/defense, surveillance, even internet television broadcasting. Future NASA missions will exploit such technologies to enable spacecraft to be sent where heretofore it was impossible, to ensure greater protection of space assets, and to increase the likelihood of mission success. We describe some of the basic concepts of swarms, and discuss the requirements of a formal method suitable for use with swarm-based systems. We also present some findings of our FAST (Formal Approaches to Swarm Technologies) project, which is attempting to identify a suitable integrated formal method for this task.
Adaptive systems are critical for future space and other unmanned and intelligent systems. Verification of these systems is also critical for their use in systems with potential harm to human life or with large financial investments. Due to their nondeterministic nature and extremely large state space, current methods for verification of software systems are not adequate to provide a high level of assurance. The combination of stabilization science, high performance computing simulations, compositional verification and traditional verification techniques, plus operational monitors, provides a complete approach to verification and deployment of adaptive systems that has not been used before. This paper gives an overview of this approach.
The need to collect new data and perform new science is causing the complexity of NASA missions to continually increase. This complexity needs to be controlled via new technological advancements and balanced with a reduction in mission and operation costs. Planned and hypothesized missions involve self-management, biological-inspiration based on swarms, and autonomous operation as a means of achieving these goals. We consider a tailored software engineering approach to developing such systems based on agent-oriented software engineering and formal methods. We report on advances in modeling, implementing, and testing NASA swarm-based concept missions.
As social networks expand and interconnect with other social networks, their combined behavior can become more complex than each individual network in isolation and can result in unexpected self-organizing or emergent behaviors. This emergent behavior results from the combined knowledge or skills of the participants, and it enables the group to do things that it could not otherwise accomplish. Examples of such social network emergence can be found in startup companies, charitable organizations, groups of researchers and terrorist cells. This paper discusses a mathematical modeling technique for prediction and detection of emergent behavior in social networks using Semi-Boolean Algebra. This paper discusses emergent behavior, the use of Semi-Boolean Algebra for detecting it, and gives examples of its use on emergence in an example social network.
NASA is developing increasingly complex missions to conduct new science and exploration. Missions are increasingly turning to multi-spacecraft to provide multiple simultaneous views of phenomena, and to search more of the solar system in less time. Swarms of intelligent autonomous spacecraft, involving complex behaviors and interactions, are being proposed to accomplish the goals of these new missions. The emergent properties of swarms make these missions powerful, but simultaneously far more difficult to design, and to verify that the proper behaviors will emerge. In verifying the desired behavior of swarms of intelligent interacting agents, the two significant sources of difficulty are the exponential growth of interactions and the emergent behaviors of the swarm. NASA Goddard Space Flight Center (GSFC) is currently involved in two projects that aim to address these sources of difficulty. We describe the work being conducted by NASA GSFC to develop a formal method specifically for swarm technologies. We also describe the use of requirements-based programming in the development of these missions, which, it is believed, will greatly reduce development lead-times and avoid many of the problems associated with such complex systems.
The explosion of capabilities and new products within the sphere of information technology (IT) has fostered widespread, overly optimistic opinions regarding the industry, based on common but unjustified assumptions of quality and correctness of software. NASA faces this dilemma as it envisages advanced mission concepts that involve large swarms of small spacecraft that will engage cooperatively to achieve science goals. Such missions involve levels of complexity that beg for new methods for system development far beyond today's methods, which are inadequate for ensuring correct behavior of large numbers of interacting intelligent mission elements. New system development techniques recently devised through NASA-led research will offer innovative approaches to achieving correctness in complex system development, including autonomous swarm missions that exhibit emergent behavior, as well as general software products created by the software Industry.
THE Urban Challenge is the third in a series of robotic grand challenges put on by the Defense Advanced Research Agency (DARPA). The grand challenges have the goal of developing robotic technologies that will reduce the number of warfighters operating in hazardous conditions and is in support of the government mandate that one-third of the military’s vehicles be autonomous by 2015. The first Grand Challenge was in March 2004 and was over a 142 mile course in the desert between Barstow, CA and Primm, NV. Fifteen vehicles made the final round, but none finished. The second Grand Challenge was in October 2005 and was over a similar 132 mile course. In this race four vehicles successfully completed the course with “Stanley” from Stanford University coming in first and winning the $2 million prize. The Urban Challenge will test the ability of robots to operate safely and effectively in populated, busy areas. It will feature autonomous ground vehicles maneuvering in a mock city environment, simulating military supply missions and must negotiate the course along with approximately 50 human-driven vehicles. The robotic vehicles will have to complete a 60-mile course in less than six hours and must obey California traffic laws while merging into moving traffic, navigating traffic circles, negotiating busy intersections and avoiding obstacles. The final event will take place on November 3, 2007 at the urban military training facility located on the former George Air Force Base in Victorville, Calif. The location has a network of urban roads and simulates the type of environment the military operates in when deployed overseas. The awards will be for $2 million, $1 million and $500,000 and will go to the top three finishers that complete the course within the six hour time limit. More information about the event is available at the DARPA web site at www.darpa.mil/grandchallenge. This special issue has nine papers from entrants to the urban challenge. The first paper by Wooden et al. describes the Sting Racing Team’s modular control architecture based on nested hybrid automata. The second paper by Crane et al. describe Team Gator Nation’s solution to the challenge to the determination of pose, appropriate behavior mode, and the smooth transition of vehicle control between behavior modes. The third paper by Upcroft et al. of the Sydney-Berkeley Driving Team discusses their solution to denied GPS and their use of vision for localization. The fourth paper by Effertz describes the Team CarOLO approach for multi-target, multi-sensor data fusion based on an extended Kalman filter algorithm. The fifth paper by Yang et al. of TeamUCF discusses their real-time trajectory planning for their vehicle. The sixth paper by Herpin et al. discusses the steering controller of their CajunBot II. The seventh paper from Henrie and Wilde describe their approach to generating clothoid-based trajectories using constructive polylines. The eighth paper from Basarke et al. discusses their system and software engineering process for developing the intelligent autonomous software for Team CarOLO. The ninth paper from Johnson discusses the TeamNOVA approach for navigating in GPS denied areas using modified orienteering techniques.
Roy Sterritt合作论文数School of Computing, University of Ulster9
Denis Gračanin合作论文数Department of Computer Science
Virginia Polytechnic Institute & State University1