I applied formal methods to the problem of verifying properties of software.  Specifically I used the Wright architecture description language to model Sun’s Enterprise JavaBeans component integration framework.  Usually, such frameworks define three things: (a) the overall structure of an application; (b) a set of interface standards; and (c) an infrastructure that supports the integration of application components.  Precise documentation of the framework is critical to both manufacturers of infrastructures supporting the standards, and to developers of applications.  My work illustrates a number of ambiguities and inconsistencies in the informal specification of such standards.

Selected Publications

Formal Modeling of the Enterprise JavaBeansTM Component Integration Framework
Joćo Pedro Sousa and David Garlan
Information and Software Technology Journal, n. 43, pp 171-188, Elsevier Print, United Kingdom, 2001.
This is an extended version of the work that appeared in the Proceedings of FM 99,  World Congress on Formal Methods in the Development of Software Systems.  Lecture Notes in Computer Science, vol. 1709, pp 1281-1300. Springer Verlag Wing, Woodcock and Davies (Editors), 1999.

Documenting Software Architectures: Recommendations for Industrial Practice
David Garlan and Joćo Pedro Sousa
Available as technical report CMU-CS-00-169.