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.
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.
Architectures: Recommendations for Industrial Practice
David Garlan and Joćo Pedro Sousa
Available as technical report CMU-CS-00-169.