|
|
|
home
> team > civil servants > {aeg}
Alwyn E. Goodloe 
 a.goodloe@nasa.gov
 +1 757 864 5064
MS 130, NASA Langley Research Center, Hampton VA 23681,
USA
I am a computer scientist working in Formal Methods group of
the safety Critical Avionics Systems Branch at NASA's Langley
Research Center.
!!!!!!NEWS!!!!!!
I am a co-chair of NASA Formal Methods 2012
please submit a paper or attend!
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
- Interactive theorem proving with PVS
![[ext]](../../../images/exlink.gif)
- Test generation from formal specifications
- Protocol verification
- Runtime verification
- Generating Java code from PVS specifications
- Fault-tolerant computing
- Verification of algorithms for air space
management
My doctoral research was
conducted under the direction of Carl A. Gunter 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:
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:
A. Goodloe and C. Munoz, Compositional Verification of
a Communication Protocol for a Remotely Operated Aircraft. To appear in
the Science of Computer Programming. 2012.
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. 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 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 page at the Illinois Security Lab
Note: The ![[ext]](/images/exlink.gif) tag identifies links that are
outside of the NASA domain.
|
