Abstract
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. These assumptions are encouraged by software producers and vendors, who at this late date have not succeeded in finding a way to overcome the lack of an automated, mathematically sound way to develop correct systems from requirements. 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 entail 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 some 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 computing industry.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Since this paper was originally published, a number of patents have been awarded, including U.S. Patents 7,668,796, 7,739,671, 7,752,608, 7,765,171, 7,886,273, and 7,979,848.
- 2.
“Deep” in the sense that the embedding is semantic rather than merely syntactic.
References
Bakam, I., Kordon, F., Page, C.L., Bousquet, F.: Formalization of a spatialized multiagent model using Coloured Petri Nets for the study of an hunting management system. In: Proc. First International Workshop on Formal Approaches to Agent-Based Systems (FAABS I). LNAI, vol. 1871. Springer, Greenbelt (2000)
Bauer, F.L.: A trend for the next ten years of software engineering. In: Freeman, H., Lewis, P.M. (eds.) Software Engineering, pp. 1–23. Academic Press, New York (1980)
Beni, G., Want, J.: Swarm intelligence. In: Seventh Annual Meeting of the Robotics Society of Japan, Tokyo, Japan, pp. 425–428. RSJ Press, Germering (1989)
Bonabeau, E., Théraulaz, G., Deneubourg, J.-L., Aron, S., Camazine, S.: Self-organization in social insects. Trends Ecol. Evol. 12, 188–193 (1997)
Bonnet, L., Florin, G., Duchien, L., Seinturier, L.: A method for specifying and proving distributed cooperative algorithms. In: Proc. DIMAS-95 (1995)
Bowen, J.P., Hinchey, M.G.: High-integrity System Specification and Design. FACIT Series. Springer, London (1999)
Brooks, Jr., F.P.: No silver bullet: essence and accidents of software engineering. IEEE Comput. 20(4), 10–19 (1987)
Büssow, R., Geisler, R., Klar, M.: Specifying safety-critical embedded systems with statecharts and Z: a case study. In: Astesiano, E. (ed.) Proc. International Conference on Fundamental Approaches to Software Engineering. LNCS, vol. 1382, pp. 71–87. Springer, Berlin (1998)
Butler, M.J.: Csp2b: a practical approach to combining Csp and B. Declarative Systems and Software Engineering Group, Department of Electronics and Computer Science, University of Southampton (1999)
Fellenstein, C.: On Demand Computing. IBM Press Series on Information Management. Prentice Hall, Upper Saddle River (2005)
Fischer, C.: Combination and implementation of processes and data: from CSP-OZ to Java. Ph.D. thesis, Universität Oldenburg, Germany (2000)
Formal Systems (Europe), Ltd.: Failures-Divergences Refinement: User Manual and Tutorial. (1999)
Gala, A.K., Baker, A.D.: Multi-agent communication in JAFMAS. In: Proc. Workshop on Specifying and Implementing Conversation Policies, Third International Conference on Autonomous Agents (Agents ’99), Seattle, Washington (1999)
Galloway, A.J., Stoddart, W.J.: An operational semantics for ZCCS. In: Hinchey, M., Liu, S. (eds.) Proc. IEEE International Conference on Formal Engineering Methods (ICFEM-97), pp. 272–282. IEEE Comput. Soc., Los Alamitos (1997)
Ganek, A.G., Corbi, T.A.: The dawning of the autonomic computing era. IBM Syst. J. 42(1), 5–18 (2003)
Gray, J.N.: What next? A few remaining problems in information technology. Turing Award Lecture (ACM FCRC) (1999)
Gray, J.N.: Dependability in the Internet era. In: Proc. High Dependability Computing Consortium Workshop, Santa Cruz, California (2001)
Harel, D.: On visual formalisms. Commun. ACM 31(5), 514–530 (1988)
Harel, D.: Biting the silver bullet: toward a brighter future for system development. IEEE Comput. 25(1), 8–20 (1992)
Harel, D.: Comments made during presentation at “Formal Approaches to Complex Software Systems” panel session. ISoLA-04 First International Conference on Leveraging Applications of Formal Methods (2004)
Hinchey, M.G., Jarvis, S.A.: Concurrent Systems: Formal Development in Csp. International Series in Software Engineering. McGraw-Hill International, London (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.: Towards an automated development methodology for dependable systems with application to sensor networks. In: Proc. IEEE Workshop on Information Assurance in Wireless Sensor Networks (WSNIA 2005). IEEE Comput. Soc., Los Alamitos (2005). Proc. International Performance Computing and Communications Conference (IPCCC-05) (Reprinted in Proc. Real Time in Sweden 2005 (RTiS2005), the 8th Biennial SNART Conference on Real-time Systems, 2005)
Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall International Series in Computer Science. Prentice Hall, Englewood Cliffs (1985)
Horn, P.: Autonomic computing: IBM’s perspective on the state of information technology. Presented at agenda 2001, Scotsdale, Arizona, 2001, IBM T. J. Watson Laboratory (October 15, 2001)
Horn, P.M.: Meeting the needs, realizing the opportunities. In: Wessner, C.W. (ed.) Capitalizing on New Needs and New Opportunities: Government—Industry Partnerships in Biotechnology and Information Technologies (2001) Board on Science, Technology, and Economic Policy (STEP), pp. 149–152. The National Academies Press, Washington (2001)
IFAD: The VDM++ toolbox user manual. Technical report, IFAD (2000)
JPL Special Review Board: Report on the Loss of the Mars Polar Lander and Deep Space 2 missions, Pasadena, California, USA (2000)
Kaufmann, M., Manolios, P., Moore, J.: Computer-Aided Reasoning: An Approach. Advances in Formal Methods Series. Kluwer Academic, Boston (2000)
Lano, K., Haughton, H.: Specification in B: An Introduction Using the B-toolkit. Imperial College Press, London (1996)
Lawson, H.W.: Rebirth of the computer industry. Commun. ACM 45(6), 25–29 (2002)
Leveson, N.G.: Medical devices: the Therac-25 story. In: Safeware: System Safety and Computers, pp. 515–553. Addison-Wesley, Reading (1995)
Lions, J.L.: ARIANE 5: Flight 501 failure, report by the inquiry board (1996)
The MathWorks, Inc., Natick, Massachusettes: Getting Started with MATLAB (2000)
Parnas, D.L.: Software aspects for strategic defense systems. American Scientist (1985)
Parnas, D.L.: Using mathematical models in the inspection of critical software. In: Applications of Formal Methods. International Series in Computer Science, pp. 17–31. Prentice Hall, Englewood Cliffs (1995)
Patterson, D., Brown, A.: Recovery-oriented computing (Keynote talk). In: Proc. High Performance Transaction Systems Workshop (HPTS) (2001)
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. IEEE Computer Society Press, Shanghai (2005)
Rash, J.L., Hinchey, M.G., Rouff, C.A., Gračanin, D., Erickson, J.D.: A tool for requirements-based programming. In: Proc. International Conference on Integrated Design and Process Technology (IDPT 2005). The Society for Design and Process Science, Beijing (2005)
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)
Rushby, J.: Remarks, panel session on the future of formal methods in industry. In: Bowen, J.P., Hinchey, M.G. (eds.) Proc. 9th International Conference of Z Users. LNCS, vol. 967, pp. 239–241. Springer, Limerick (1995)
Sterritt, R.: Towards autonomic computing: effective event management. In: 27th Ann. IEEE/NASA Software Engineering Workshop (SEW), MD, USA, pp. 40–47. IEEE Comput. Soc., Los Alamitos (2002)
Sterritt, R.: Autonomic computing. Innovations in Systems and Software Engineering: a NASA Journal 1(1) (2005)
Sterritt, R., Bustard, D.W.: Autonomic computing: a means of achieving dependability? In: IEEE Int. Conf. Engineering of Computer Based Systems (ECBS’03), Huntsville, AL, USA, pp. 247–251 (2003)
Sterritt, R., Hinchey, M.G.: Why computer based systems Should be autonomic. In: Proc. 12th IEEE International Conference on Engineering of Computer Based Systems (ECBS 2005), Greenbelt, MD, pp. 406–414 (2005)
Truszkowski, W., Hinchey, M., Rash, J., Rouff, C.: NASA’s swarm missions: the challenge of building autonomous software. IT Prof. 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 Trans. Syst. Man Cybern., Part C, Appl. Rev. 36(3), 279–291 (2006)
Truszkowski, W.F., Rash, J.L., Rouff, C.A., Hinchey, M.G.: Some autonomic properties of two legacy multi-agent systems—LOGOS and ACT. In: Proc. 11th IEEE International Conference on Engineering Computer-Based Systems (ECBS), Workshop on Engineering Autonomic Systems (EASe), pp. 490–498. IEEE Comput. Soc., Los Alamitos (2004)
Acknowledgements
This paper was previously published in Proc. Eighth International Conference on Integrated Design and Process Technology (IDPT), 2005. Reprinted with permission.
This work is funded in part by Science Foundation Ireland grant 03/CE2/I303_1 to Lero—the Irish Software Engineering Research Centre (www.lero.ie); by the NASA Office of Safety and Mission Assurance, under its Software Assurance Research Program project Formal Approaches to Swarm Technologies (FAST), administered by the NASA IV&V Facility; by the Office of Technology Transfer, NASA Goddard Space Flight Center; by the NASA Software Engineering Laboratory, NASA Goddard Space Flight Center; and by the University of Ulster Computer Science Research Institute and the Centre for Software Process Technologies (CSPT), funded by Invest NI through the Centres of Excellence Programme under the European Union Peace II initiative.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag London Limited
About this chapter
Cite this chapter
Hinchey, M., Rash, J.L., Truszkowski, W.F., Rouff, C.A., Sterritt, R. (2012). You Can’t Get There from Here! Large Problems and Potential Solutions in Developing New Classes of Complex Computer Systems. In: Hinchey, M., Coyle, L. (eds) Conquering Complexity. Springer, London. https://doi.org/10.1007/978-1-4471-2297-5_7
Download citation
DOI: https://doi.org/10.1007/978-1-4471-2297-5_7
Publisher Name: Springer, London
Print ISBN: 978-1-4471-2296-8
Online ISBN: 978-1-4471-2297-5
eBook Packages: Computer ScienceComputer Science (R0)