NASA logo

+ Contact NASA



  • + HOME
  • + WELCOME
  • + QUICK PAGE
  • + PHILOSOPHY
  • + TEAM
  • + RESEARCH
  • + LINKS

  • Alwyn E. Goodloe

    I am a computer scientist working in Formal Methods group of the safety Critical  Avionics Systems Branch at NASA's Langley Research Center.

    Research

      My primary research focus is in the area of  formal methods applied to safety critical systems. In particular, my recent research has been in the areas of

    My doctoral research was conducted under the direction of Carl A. Gunter [ext] and primarily focused  in the area of network security and I still have a strong interest in network security, configuration, and analytics.  I also conducted some work  in embedded systems. My masters  thesis in math was in computer algebra.

    Education:

    Ph.D. Computer and Information Science,[ext] University of Pennsylvania[ext], 2008

    MSE Computer and Information Science[ext], University of Pennsylvania[ext], 2000

    MSc Mathematics[ext], George Mason University[ext], 1992

    European Summer Schools

    NATO Summer School on Models, Algebras, and Logics, Marktoberdorf, Germany, July 2002.

    European Education Forum Summer School on Specification, Refinement, and Verification, Turku, Finland, August 2002.

    Selected Papers:

    L. Pike, N.Wegmann, S. Niller, and A. Goodloe.   Copilot: Monitoring Embedded Systems, in Innovations in Systems and Software Engineering, Volume 9, Issue 4, 2013.

    A. Goodloe, C. Munoz, F.Kirchner, and L. Correson.   Verification of Numerical Programs: From Real Numbers to Floating Point Numbers, in Proceedings of 5th NASA Formal Methods Symposium (NFM 2013), Lecture Notes in Computer Science, Vol. 7871, pp. 441-446, May 2013.

    L. Pike, N.Wegmann, S. Niller, and A. Goodloe.   Experience Report: A Do-It-Yourself High-Assurance Compiler, International Conference on Functional Programming (ICFP), 2012.

    A. Goodloe and C. Munoz.  Compositional Verification of a Communication Protocol for a Remotely Operated Aircraft, Science of Computer Programming, Volume 78, Issue 7, pp. 813-827, 2013*. This paper is an extended version of the conference publication in Lecture Notes in Computer Science, Volume 5825, November 2009.

    L. Pike and A. Goodloe.   Copilot: A Hard Real-Time Runtime Monitor. To appear in Proceedings of 1st International Conference on Runtime Verification. 2010.

    A. Goodloe and L. Pike.   Toward Monitoring Fault-Tolerant Embedded Systems. In Proceedings of 1st International Workshop on Software Health Management. 2009.

    A. Goodloe and C. Pasareanu and D. Bushnell and P. Miner.   Test Generation Framework for Distributed Fault-Tolerant Algorithms. In Proceedings of Automated Formal Methods. 2009.

    A. Goodloe and C. A. Gunter.   Completeness of Discovery Protocols. In Proceedings of ACM Workshop on Assurable and Usable Security Configuration. 2009.

    A. Goodloe and C. Munoz.   Compositional Verification of a Communication Protocol for a Remotely Operated Vehicle. In Proceedings of Formal Methods and Industrial and Critical Systems. Lecture Notes on Computer Science 5825,Springer-Verlag. 86--101. 2009.

        A. Goodloe and C.A. Gunter. Reasoning about Concurrency for Security Tunnels.In 20th IEEE Computer Security Foundations Symposium. July 2007.

     A. Goodloe, M. Jacobs, G. Shah, and C.A. Gunter.  L3A: A Protocol for Layer Three Accounting.   In Proceedings of the First Workshop on Secure Network Protocols (NPSEC), 2005.

    A. Goodloe, C. A. Gunter, and M.-O. Stehr. Formal Prototyping in Early Stages of Protocol Design. In Proceedings of the Workshop on Issues in the Theory of Security (WITS'05).  The ACM Digital Library, 2005.

    A. Goodloe, M. McDougall, C.A. Gunter, and R. Alur. Predictable Programs in Barcodes. In Proceedings of International Conference on  Compilers, Architecture and Synthesis of Embedded Systems (CASES), 298-303, 2002.

    A. Goodloe, M. McDougall, C.A. Gunter, and R. Alur. Predictable Programs in Barcodes. In Proceedings of International Conference on  Compilers, Architecture and Synthesis of Embedded Systems (CASES), 298-303, 2002.

    A. Goodloe and P. Loustaunau. An Abstract Data Type Development  of Graded Rings, In Proceedings of the International Symposium on  the Design and Implementation of Symbolic Computation Systems (DISCO),  Lecture Notes in Computer Science 721, 192-202, 1992.


    Technical Reports

    A. Goodloe and L. Pike. Monitoring Distributed Real-Time Systems: A Survey and Future Directions. NASA Technical Report. 2010.

    C. Munoz and A. Goodloe. Design and Verification of a Distributed Communication Protocol. NASA Technical Report. 2008.

     A. Goodloe, M. McDougall, C. A. Gunter, and M.-O. Stehr. Designand Analysis of Sectrace: A Protocol to Set Up Security Associations
      in IPsec.  CIS Department Technical Report, University of Pennsylvania, 2004.

    A. Goodloe, M. McDougall, C. A. Gunter, T. Hiller, and  P. McCann.  Authenticated Traversal. CIS Department Technical Report, University of Pennsylvania, 2002.

    My dissertation and  research papers in network security can be found on the tunnel calculus [ext] page at the Illinois Security Lab[ext]

    Note: The [ext] tag identifies links that are outside of the NASA domain.

    Contact

    Safety Critical Avionics Systems Branch
    NASA Langley Research Center
    Mail Stop 130
    Hampton, VA 23681-2199, USA


    a.goodloe@nasa.gov
    Phone: +1 (757) 864 5064
    Fax: +1 (757) 864 4234