Technology Transition

Technology Transition

We transitioned the UniCon toolset to the University of Oregon. It was used in a Masters course on Software Architecture to teach the students about architectural abstractions and how to describe systems using them.

We transitioned the Aesop toolset to Lockheed-Martin for packaging and incorporation in the EDCS demonstrations for "Demo Days."

David Garlan prepared a tutorial entitled "Architectural Description and Analysis," which will be given at the European Software Engineering Conference in September.

We applied formal modeling tools to DMSO HLA, generating significant feedback, which has had an impact on their published architectural specification.

We made the following systems and prototypes publicly available. Some can be obtained over the WWW, and for these we have included the URL.

1. UniCon
System UniCon ToolSet
Purpose Toolset for creating, manipulating, analyzing, and compiling software architecture descriptions written in the UniCon architecture description language (ADL)
Environment Linux, SunOS 4.1.3, Solaris 5.4, 5.5 platforms; Also requires installation of Odin (make-like system construction utility, available in the public domain - see
Point of Contact Gregory Zelesnik (

2. Nitpick
System Nitpick
Purpose Tool for analyzing designs which are described in a Z-like specification language called NP
Environment any Macintosh computer
Point of Contact Craig A. Damon (

3. Aesop
System Aesop
Purpose Toolkit and framework that allows software architects to quickly and easily generate customized, "style-specific" software architecture design environments
Environment SunOS 4.1.3 (Has been ported to Solaris by Aesop users, but not yet included with the CMU Aesop distribution).
Point of Contact David Garlan (

System ACME
Purpose Software architecture interchange language that supports the interchange of architectural descriptions among a wide variety of architecture description languages (ADLs) and their associated toolsets
Environment The ACME Tool Developer's Library (AcmeLib), which includes extensible ACME parsers and unparsers, is written in C++ and available for Unix and PC platforms. The primary environment requirement is a modern C++ compiler
Point of Contact David Garlan (

5. Revere
System Revere
Purpose Analysis tool for cryptographic protocols
Environment Requires Standard ML of New Jersey, version 109.29 or higher (available for Windows 95/NT and most Unix variants)
Point of Contact Darrell Kindred (

6. Lackwit
System Lackwit
Purpose Tool for reverse-engineering programs to recover information about the flow and use of data
Environment SunOS, Linux, Alpha OSF 3.2, or Ultrix
Point of Contact Robert O'Callahan (


The following are the papers authored by this group during fiscal year 1997. All have been submitted, accepted for publication, or published. They represent transition of (or an attempt to transition) our research to the community at large.

Jeannette Wing. Subtyping for Distributed Object Stores. To appear in Proceedings of the Second IFIP International Workshop on Formal Methods for Open Object-based Distributed Systems (FMOODS), July 1997. Extended abstract of invited talk.

Yu-Chung Ng, A Nitpick Specificatoin of IPv6. B.S. in Computer Science, May 1997.

Amy Zaremski, Jeanette Wing. Specification Matching of Software Components. To appear in ACM Transactions on Software Engineering and Methodology, accepted May 1997.

Jeannette Wing, Mondonna Vaziri-Farahani. A Case Study in Model Checking Software Systems. Science of Computer Programming, Vol. 28, 1997, pp. 273-299.

Edmund Clarke, Jeannette Wing. Formal Methods: State of the Art and Future Directions. ACM Computing Surveys, Vol. 28, No. 4, December 1996, pp. 626-643.

Gary Leavens, Jeannette Wing. Protective Interface Specifications. Proceedings of TAPSOFT '97 Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, Lecture Notes in Computer Science 1214, April 1997, pp. 520-534.

Darrell Kindred, Jeannette Wing. Fast, Automatic Checking of Security Protocols. Proceedeings of the USENIX 1996 Workshop on Electronic Commerce, Oakland, CA, November 1996, pp. 41-52.

N. Heintze, Doug Tygar, Jeannette Wing, Hao-Chi Wong. Model Checking Electronic Commerce Protocols. Proceedings of the USENIX 1996 Workshop on Electronic Commerce, Oakland, CA, November 1996, pp. 147-164.

Craig Damon, Daniel Jackson, Somesh Jha. Checking Relational Specifications with Binary Decision Diagrams. Proceedings of the 4th ACM SIGSOFT Conference on Foundations of Software Engineering, San Francisco, CA, October 1996, pp.70-80.

Daniel Jackson, Craig Damon, Somesh Jha. Faster Checking of Software Specifications. Proceedings of the ACM Conference on Principles of Programming Languages, St. Petersburg Beach, FL, January 1996, pp. 79-90.

Daniel Jackson, Somesh Jha, Craig Damon. Isomorph-free Model Enumeration: A New Method for Checking Relational Specifications. Accepted for publication pending minor revision, ACM Transactions on Programming Languages and Systems.

Robert O'Callahan, Daniel Jackson. Lackwit: A Program Understanding Tool Based on Type Inference. Proceedings of the International Conference on Software Engineering, Boston, MA, May 1997.

Heather Richter. A Taxonomy of Visualizations in Software Architecture. CMU Technical Report, to appear.

Robert Allen. A Formal Approach to Software Architecture. Ph.D. Thesis, Carnegie Mellon University, May, 1997. CMU Technical Report CMU-CS-97-144.

Robert Allen, David Garlan. A Formal Basis for Architectural Connection. Accepted, Transactions on Software Engineering and Methodology To appear, July 1997.

Robert Monroe, Andrew Kompanek, Ralph Melton, David Garlan. Architectural Styles, Design Patterns, and Objects. IEEE Software, January 1997.

David Garlan, Robert Monroe, David Wile. ACME: An Architecture Description Interchange Language. Submitted for publication.

Robert Allen, David Garlan. Formal Modeling and Analysis of the HLA RTI. Proceedings of the 1997 Spring Simulation Interoperability Workshop, March, 1997.

David Garlan. Style-Based Refinement for Software Architecture. Proceedings of the Second International Software Architecture Workshop (ISAW2), October, 1996.

Ralph Melton, David Garlan. Architectural Unification. Submitted for publication, January, 1997.

Mary Shaw, Paul Clements. A Field Guide to Boxology: Preliminary Classification of Architectural Styles for Software Systems. To appear, COMPSAC '97. Preliminary version, Toward Boxology: Preliminary Classification of Architectural Styles, Proceedings of the Second International Software Architecture Workshop, October, 1996.

Robert DeLine, Gregory Zelesnik, Mary Shaw. Lessons on Converting Batch Systems to Support Interaction. Proceedings of the 18th International Conference on Software Engineering, May 1997, pp.195-204.


The following are the talks given by the principle investigators of this contract during fiscal year 1997. These talks represent transition of our research to the community at large.

Jeannette Wing

"A Story in the Practice of Formal Methods."
Brown University, April 11, 1997.

"Formal Methods: Past, Present, and Future."
Programming Systems Cultural Exchange Series, CMU, February 17, 1997.

"Formal Methods: Past, Present, and Future."
University of Pennsylvania, Distinguished Lecture Series, January 28, 1997.

"Mathematics for Software Engineers."
Harvard University, November 26, 1996.

Mary Shaw

Keynote Address,
Fifth International Symposium on Assessment of Software Tools and Technologies.
Pittsburgh PA, June 1997.

"Software Architecture: Perspectives on an Emerging Discipline."
Quest Technology Awareness Symposium, Schaumberg IL April 1997.

"Architectures for Software Systems."
Distinguished Lecture, York University, Toronto Canada, March 1997.

Keynote address, Nortel Design Forum
Nortel Teleconference from Ottawa Canada, December 1996.

"Software Architecture: Perspectives on an Emerging Discipline."
International Software Architecture Workshop, FASE-4,
San Francisco CA, October 1996.

David Garlan

Invited lecture, "Software Architecture: Practice and Potential."
Oregon Graduate Institute, Beaverton OR, June 1997.

Panel participant, "Future directions in Distributed Simulation."
1997 Spring Simulation Interoperability Workshop, Orlando FL, March 1997.

Invited lecture, "Software Architecture."
Texas Instruments, Fort Worth TX, December 1996.

Distinguished Lecture, "An Engineering Discipline for Software Architecture."
University of British Columbia, Vancouver BC, Canada, December 1996.

Daniel Jackson

"Using Relations and Symmetry to Find Bugs in Software Specifications."
Department of Computer Science, Columbia University, N.Y., February 20, 1997.
Department of Computer Science, Technion, Haifa, Israel, February 27, 1997.
Institute of Computer Science, Hebrew University, Jerusalem, Israel, March 3, 1997.
Department of Computer Science, Princeton University, Princeton, NJ, March 11, 1997.
Department of Electrical Engineering and Computer Science,
Massachusetts Institute of Technology, Cambridge, MA, March 19, 1997.
Department of Computer Science, Stanford University, Stanford, CA, April 2, 1997.

"A Trick For Finding Models of Relational Formulae."
IFIP Working Group 2.3 on Programming Methodology,
Napa Valley, CA, January 29, 1997.

"Construction and Analysis of Object Models".
Department of Computing,
Imperial College of Science, Technology and Medicine, January 17, 1997.

"Model Checking and Requirements".
3rd IEEE International Symposium on Requirements Engineering (RE'97),
Annapolis, MD, January 8, 1997.

Mail the current maintainer of this page.

Last modified: July 1997