Abstract
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.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Failures-Divergences Refinement: User Manual and Tutorial. Formal Systems (Europe), Ltd. (1999)
Bowen, J.P., Hinchey, M.G.: Ten commandments revisited: A ten year perspective on the industrial application of formal methods. In: Proc. FMICS 2005, 10th International Workshop on Formal Methods for Indutrial Critical Systems, Lisbon, Portugal, September 5 – 6, 2005, ACM Press, New York (2005)
Butler, M.J.: csp2B: A Practical Approach To Combining CSP and B. In: Declarative Systems and Software Engineering Group, University of Southampton (February 1999)
Harel, D.: From play-in scenarios to code: An achievable dream. IEEE Computer 34(1), 53–60 (2001)
Harel, D.: Comments made during presentation at “Formal Approaches to Complex Software Systems” panel session. In: ISoLA 2004 First International Conference on Leveraging Applications of Formal Methods, Paphos, Cyprus, October 31 (2004)
Hinchey, M.G., Jarvis, S.A.: Concurrent Systems: Formal Development in CSP. In: International Series in Software Engineering, McGraw-Hill International, London, UK (1995)
Hinchey, M.G., Rash, J.L., Rouff, C.A.: Requirements to design to code: Towards a fully formal approach to automatic code generation. Technical Report TM-2005-212774, NASA Goddard Space Flight Center, Greenbelt, MD, USA (2004)
Hinchey, M.G., Rash, J.L., Rouff, C.A.: A formal approach to requirements-based programming. In: Proc. IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2005), April 3–8, 2005, IEEE Computer Society Press, Los Alamitos, Calif (2005)
Hinchey, M.G., Rash, J.L., Rouff, C.A., Gračanin, D.: Achieving dependability in sensor networks through automated requirements-based programming. Journal of Computer Communications, Special Issue on“Dependable Wireless Sensor Network” 29(2), 246–256 (2006)
Hinchey, M.G., Rash, J.L., Rouff, C.A., Truszkowski, W.F.: Requirements of an integrated formal method for intelligent swarms. In: Proc. FMICS 2005, 10th International Workshop on Formal Methods for Industrial Critical Systems, Lisbon, Portugal, September 5–6, 2005, ACM Press, New York (2005)
Hinchey, M.G., Rash, J.L., Truszkowski, W.F., Rouff, C.A., Sterrit, R.: Autonomous and autonomic swarms. In: Proc. The 2005 International Conference on Software Engineering Research and Practice (SERP 2005), Las Vegas, Nevada, USA, June 27, pp. 36–42. CSREA Press (2005)
Hinchey, M.G., Rash, J.L., Truszkowski, W.F., Rouff, C.A., Sterritt, R.: You can’t get there from here! Problems and potential solutions in developing new classes of complex systems. In: Proc. Eighth International Conference on Integrated Design and Process Technology (IDPT), Beijing, China, June 13–17, The Society for Design and Process Science (2005)
Hoare, C.A.R.: Communicating sequential processes. Communications of the ACM 21(8), 666–677 (1978)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall International Series in Computer Science. Prentice Hall International, Englewood Cliffs, NJ (1985)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Advances in Formal Methods Series. Kluwer Academic Publishers, Boston (2000)
Rash, J.L., Hinchey, M.G., Rouff, C.A., Gračanin, D.: Formal requirements-based programming for complex systems. In: Proc. International Conference on Engineering of Complex Computer Systems, Shanghai, China, June 16–20, 2005, IEEE Computer Society Press, Los Alamitos, Calif (2005)
Rash, J.L., Hinchey, M.G., Rouff, C.A., Gračanin, D., Erickson, J.D.: Experiences with a requirements-based programming approach to the development of a NASA autonomous ground control system. In: Proc. IEEE Workshop on Engineering of Autonomic Systems (EASe 2005) held at the IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2005), April 3–8, 2005, IEEE Computer Society Press, Los Alamitos, Calif (2005)
Rouff, C., Vanderbilt, A., Hinchey, M., Truszkowski, W., Rash, J.: Formal methods for swarm and autonomic systems. In: Proc. 1st International Symposium on Leveraging Applications of Formal Methods (ISoLA), Cyprus, October 30–November 2 (2004)
Rouff, C., Vanderbilt, A., Hinchey, M., Truszkowski, W., Rash, J.: Properties of a formal method for prediction of emergent behaviors in swarm-based systems. In: Proc. 2nd IEEE International Conference on Software Engineering and Formal Methods, Beijing, China (September 2004)
Rouff, C.A., Truszkowski, W.F., Rash, J.L., Hinchey, M.G.: A survey of formal methods for intelligent swarms. Technical Report TM-2005-212779, NASA Goddard Space Flight Center, Greenbelt, Maryland (2005)
Sterritt, R., Rouff, C.A., Rash, J.L., Truszkowski, W.F., Hinchey, M.G.: Self-* properties in NASA missions. In: 4th International Workshop on System/Software Architectures (IWSSA 2005) in Proc. 2005 International Conference on Software Engineering Research and Practice (SERP 2005), Las Vegas, Nevada, USA, June 27, pp. 66–72. CSREA Press (2005)
Truszkowski, W., Hinchey, M., Rash, J., Rouff, C.: NASA’s swarm missions: The challenge of building autonomous software. IEEE IT Professional 6(5), 47–52 (2004)
Truszkowski, W.F., Hinchey, M.G., Rash, J.L., Rouff, C.A.: Autonomous and autonomic systems: A paradigm for future space exploration missions. IEEE Transactions on Systems, Man and Cybernetics, Part C: Applications and Reviews 36(3), 279–291 (2006)
van Zuylen, H.J.: The REDO Compendium: Reverse Engineering for Software Maintenance. John Wiley and Sons, London, UK (1993)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Hinchey, M.G., Rash, J.L., Rouff, C.A. (2008). Some Verification Issues at NASA Goddard Space Flight Center. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_43
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_43
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)