EDCS Annual Report April 1, 1997 through March 31, 1998 CMU: A Technology Investigation Supporting Software Architecture and Analysis for Evolution Cooperative Agreement F30602-97-2-0031 1.0 Accomplishments This section presents a comparison of actual accomplishments with the goals and objectives established for the period. Additionally, it lists accomplishments that go above and beyond the stated goals and objectives. The basis of comparison is the set of milestones that were generated to satisfy the request made by the Contract Monitoring Agent (Captain Mark Gerken, Rome Air Development Center) on May 15, 1997. The milestones are listed, followed by the set of accomplishments that satisfy each. Where a milestone was not satisfied, an appropriate explanation is substituted in lieue of accomplishments. The milestones are listed in chronological order by year and quarter. This section of the annual report satifies the requirements for section 1, subsections a) and b) as outlined in Part IV, Article 15, Part C of Cooperative Agreement F30602-97-2-0031. 1.1 2nd Quarter 1997 Progress Against Milestones TABLE 1. 2nd Quarter 1997 Milestones Milestone Satisfying Accomplishments Transition the Aesop and ACME toolsets to Lockheed-Martin for packaging and incorporation into their 1997 EDCS "Demo Days" demonstrations. Distributed release of version 0.2 of the ACME Web-generator tool and the automatic graph-layout tool to Lockheed Martin. Extended Aesop to support ACME version 3.0 and a new distributed message passing architectural style. Distributed this technology to Lockheed-Martin. Developed version 3.0 of the ACME Library in C++ and Java, and distributed it to Lockheed Martin. Publish a report on Architectural Mismatch. A paper is in draft. Revision of the paper has been deferred to allow Rob DeLine to pursue a research opportunity that will aid refinement of the taxonomy. Other 2nd Quarter 1997 Accomplishments We made the following languages and tools publically available over the Internet: TABLE 2. Publically available Languages and Toolsets language/tool URL UniCon http://www.cs.cmu.edu/~UniCon Nitpick http://www.cs.cmu.edu/~nitpick Aesop http://www.cs.cmu.edu/~able/aesop ACME http://www.cs.cmu.edu/~acme Revere http://www.cs.cmu.edu/~revere Lackwit http://www.cs.cmu.edu/~roc/Lackwit.html In UniCon, we implemented the capability of converting UniCon to ACME, and vice-versa. The UniCon toolset was used to support a class in Software Architectures at the University of Oregon, taught by Professor Marilynn Livingston. We delivered the Carnegie Mellon University Software Architecture course once again, and this time it was captured for on-line dissemination and CD-ROM packaging. We developed a new symmetry reduction method for our Nitpick specification checker. In the summer of 1996, we began work on a simpler proof of soundness of our existing method; while working on the proof, we found a way to improve the algorithm. The new algorithm was incorporated into the Nitpick tool during this period; it is not only cleaner but also performs significantly better. This new algorithm is described in the following paper: Daniel Jackson, Somesh Jha, Craig A. Damon. "Isomorph-free Model Enumeration: A New Method for Checking Relational Specifications." ACM Transactions on Programming Languages and Systems. We used Nitpick to verify two properties of the Mobile IPv6 protocol (adopted as an IETF standard). The properties we checked are that the cache entries of mobile hosts do not form a cycle (so packets never travel in a loop) and that authenticated messages do not form a cycle. We found an error in the Mobile IPv6 protocol specification where a cycle, involving just two hosts, could be created. We informed one of the designers of the problem, since IP does not have the same error. We also found that a feature that was originally included as a performance optimization of the protocol was necessary its correctness. We have adapted type theory, and its associated inference algorithms, to be exploited for reverse engineering of large C programs. The declared type of a function in a C program will rarely tell you as much as it might; a function might declare an argument to be a pointer, for example, even if it is never dereferenced. But by inferring, in a richer type system than C's, the most general type of a function, one can obtain detailed information about the use of data structures. Robert O'Callahan built a prototype tool called Lackwit that can show where data structures are read and written, and how values flow from one to another; it can find candidates for data abstraction and identify representation exposures (i.e., inappropriate revelations of the internal representation of an abstract data type); and it can show dependences between functions due to shared data, correctly distinguishing incidental use of shared library functions from true architectural connection. The analysis is completely modular and can accommodate missing or incomplete code, handles aliasing and higher order functions smoothly, and scales remarkably well. The prototype tool has been applied successfully to Reid Simmon's Morphin, a robotics application, and is now being used to analyze the entire source code of the Linux operating system. We made progress on developing a new formal basis for modeling dynamic software architectures; that is, architectures that can be reconfigured during run time. Analytic tractability is achieved by localizing reconfiguration information in a special "reconfiguration module" which is triggered by special reconfiguration control events in the system's components. Significant properties of a dynamic architecture can then be checked. It is possible to determine if a system reconfiguration can cause in-transit data to be lost. We developed a new algorithm, called Architectural Unification, that determines when an architectural design fragment (or pattern) can be instantiated in a given context. We developed a taxonomy of visualization techniques based on evaluation of over 70 published industrial architectural case studies. When it is complete this work will provide practical guidance for practicing software architects who want to improve their ability to use visual techniques to describe system architectures. We developed an ACME-based tool that converts Wright specifications into Rapide specifications. This tool permits the incorporation of Rapide tools (e.g., for POSET viewing, animation, and anomaly detection) into the Wright tool suite. 1.2 3rd Quarter 1997 TABLE 3. 3rd Quarter 1997 Milestones Milestone Satisfying Accomplishments Demonstrate Aesop and Unicon integration (via ACME). Performed the following tasks in support of the EDCS "Demo Days" Conference in Seattle, July 21-24, 1997: · finished UniCon-to-ACME, ACME-to-UniCon, and Aesop-to-ACME converters · added a "message queue" connector to the UniCon toolset · finished a performance analysis tool for message passing architectures · designed and implemented a message-passing application for the demonstration Developed an ACME(v3.0)-UniCon translator using the Able group's C++ ACMELib distribution. Developed a UniCon-ACME(v3.0) translator. Extended Aesop to support translation to ACME(v3.0) and to add a new distributed message passing architectural style. Produced a demonstration integrating ACME, UniCon, and Aesop for EDCS "Demo Days." Presented the "Integration" demonstration at the EDCS "Demo Days" in Seattle. This demonstration highlighted the group's success with the integration of ACME, UniCon, and Aesop. Send a report to DMSO on our initial findings from the HLA analysis. Applied formal modeling tools to the Defense Modeling and Simulation Office (DMSO) High Level Architecture (HLA) IFSpec, generating significant feedback, which was summarized in a report to DMSO. Demonstrate a prototype architectural performance analysis tool. Developed a performance analyzer for ACME-based architectural descriptions. Publish our report on a catalog of architectural styles and design elements. Published the following paper: Shaw, M., Clements, P. "A Field Guide to Boxology: Preliminary Classification of Architectural Styles for Software Systems." COMPSAC `97, August, 1997. Other 3rd Quarter 1997 Accomplishments We developed a better understanding of the role of imperative modules for expressing architectural connectors. This enhanced our ability to develop the SML-mod-rec extension of the SML modules language, in which architectural connectors can be described. 1.3 4th Quarter 1997 Progress Against Milestones TABLE 4. 4th Quarter 1997 Milestones Milestone Satisfying Accomplishments Perform case studies of application of exhaustive case enumeration (Nitpick) to architectures and architectural styles. Published the following papers: Jackson, D., Ng, Y., Wing, J. "A Nitpick Analysis of Mobile IPv6." CMU Technical Report CMU-CS-98-113, March, 1998. Jackson, D. "Automatic Analysis of Architectural Style." Jackson, D., Damon, C. "Semi-executable Specifications." CMU School of Computer Science Technical Report 95-216, Pittsburgh, PA. November, 1995. Finish the preliminary design of UniCon 2. Developed the initial prototype of the UniCon 2 graphical editor using Visio 5.0, Visual Basic for Applications (VBA), and Java. Architectural descriptions in the UniCon 2 textual syntax can be loaded into the editor, rendered graphically, and then exported as text once again. This can be accomplished for the pipe-and-filter style. Additionally, these graphical descriptions can be partially built, meaning that the glue code is generated for the connections when the system is built. Implemented credentials in the compiler prototype backend. The following paper describes credentials: Shaw, M. "Truth vs. Knowledge: The Difference Between What a Component Does and What We Know It Does." Proceedings of the 8th International Workshop on Software Specification and Design, March, 1996. Finish implementing bounded generation in Nitpick. Developed the first formal definition of bounded generation, one of Nitpick's state space reduction techniques. Implemented bounded generation in Nitpick. Finish implementing "honesty" and "feasibility" checks in Revere. Developed a better understanding of "honesty" and "responsibility" checks for authentication protocols. Implemented "honesty," "responsibility," and "feasibility" checks in Revere. Other 4th Quarter 1997 Accomplishments We helped DMSO produce the next draft of the HLA IFSpec. We applied Wright to the Defense Modeling and Simulation Office (DMSO) High Level Architecture (HLA) for distributed simulation. Specifically, we modeled the part of the architecture that concerns distributed time management. This led to new insights into the algorithms for time management, which in turn led to changes in the the most recent release of the published HLA specification. In our research on using ML for architecture descriptions we identified a key language feature not directly supported by ML but needed to support software architecture description. This is the capability of defining recursive ML structures, which permits symmetric definition of connector attachment. We made significant progress on the formalization of "theory generation," the key technique behind Revere. We identified it to be a decidable fragment of first-order logic. We investigated existing model checkers (Spin) and proof checkers (Step) in preparation for designing a hybrid checker for analyzing security protocols. We immediately discovered many limitations of both tools that would stand in the way of using them directly. We plan to look at secure auction protocols as our challenge problem. 1.4 1st Quarter 1998 Progress Against Milestones TABLE 5. 1st Quarter 1998 Milestones Milestone Satisfying Accomplishments Publish a report on Modeling Dynamic Architectures. Published the following paper: Allen, R., Douence, R., Garlan, D. "Specifying and Analyzing Dynamic Software Architectures." Proceedings of the 1998 Conference on Fundamental Approaches to Software Engineering (FASE'98), March, 1998. Demonstrate the utility of Revere on a suite of examples. In progress; this will be completed by the end of 2nd Quarter 1998. Other 1st Quarter 1998 Accomplishments We made a technical breakthrough in giving a type-theoretic semantics to an extension of the SML modules language, SML-mod-rec. We can use this extended language to encode much of the commonality in existing ADLs, in particular representing both connectors and components as modules. The technical extension to SML needed is mutually recursive structures; giving a semantics to this extension is non-trivial. For Revere, we achieved a significant technical goal by completely formalizing the theory generation approach, proving its soundness with respect to the (decidable) fragment of first-order theory it defines. Theory generation is described in detail in Darrell Kindred's thesis, as well as in the following publication: Kindred, D., Wing, J. "Fast, Automatic Checking of Security Protocols." Proceedings of the USENIX 1996 Workshop on Electronic Commerce, Rutgers, NJ, November, 1996. For Nitpick, we developed a new framework for formally describing and analyzing the underlying techniques. Using this framework, the techniques have been proven sound. We developed a successor to Nitpick called LadyBug. LadyBug offers four significant advantages over the original Nitpick: · improved reductions in the number of cases necessary to generate and test due to the implementation of several basic improvements, including bounded generation, consequence closure of the fact set, and optimized derived variable selection · portability gained through Java · ability to easily plug in alternative solver methods to enable comparisons between techniques. · internal support for additional specification language features, including numbers and inheritance, with the expectation of eventually supporting the UML constraint language OCL In UniCon 2, we implemented multiple inheritance of properties in extendable language definitions. This extension makes it possible for definitions in the language to have more than one build expert, so that multiple types of build expertise can be applied to the same component or connector abstraction in a given system build. Implemented remote builds, allowing the toolset to build descriptions targetted for Unix and Windows NT platforms, even though they are hosted on Windows NT platforms. In UniCon 2, we implemented Remote Procedure Call (RPC) and Pipe connector abstractions for systems targetted for the Unix platform, as well as PLBundler, ProcedureCall, and DataAccess connector abstractions for systems that are targetted for both the Unix and Windows NT environments. In the UniCon 2 graphical editor, we implemented the capability of saving textual descriptions after they have been manipulated graphically. This includes the saving of the positioning information associated with the graphical shapes. Enhanced the graphical ditor to load descriptions written in any architectural style: unknown component and connector abstractions are rendered with default shapes. For UniCon 2, we began implementing conversions to and from ACME. 2.0 Cost Overruns This section of the annual report satifies the requirements for section 1, subsection c) as outlined in Part IV, Article 15, Part C of Cooperative Agreement F30602-97-2-0031. This project experienced no cost overruns during the period covered by this annual report, April 1, 1997 through March 31, 1998. However, our burn rate of the funds received from the Defense Advanced Research Projects Agency (DARPA) during the recent months has exceeded our estimated burn rate. Our academic calendar results in significantly different expense profiles in academic year and in summer. We will carefully review and adjust our expenses for the summer. 3.0 Chronological List of Publications This section of the annual report satisfies the requirements for section 2, subsection d) as outlined in Part IV, Article 15, Part C of Cooperative Agreement F30602-97-2-0031. Spitznagel, B., Garlan, D. "Architecture-Based Performance Analysis." Accepted for publication in Proceedings of the 10th International Conference on Software Engineering and Knowledge Engineering (SEKE'98), June, 1998. Allen, R., Douence, R., Garlan, D. "Specifying and Analyzing Dynamic Software Architectures." Proceedings of the 1998 Conference on Fundamental Approaches to Software Engineering (FASE'98), March, 1998. Leavens, G., Wing, J. "Protective Interface Specifications." Formal Aspects of Computing, March, 1998. Jackson, D., Ng, Y., Wing, J. "A Nitpick Analysis of Mobile IPv6." CMU Technical Report CMU-CS-98-113, March, 1998. Garlan, D. "Higher-Order Connectors." Proceedings of Workshop on Compositional Software Architectures, January, 1998. Wang, Z. "Separating Application Logic from Architectural Concerns - Beyond Object Services and Frameworks." Proceedings of Workshop on Compositional Software Architectures, January, 1998. Vaziri-Farahani, M., Lynch, N., Wing, J. "Proving the Correctness of a Controller Algorithm for the RAID Level 5 System." Accepted for publication in Fault-Tolerant CS, 1998. DeLine, R. "Understanding Changes to Software Component Packaging." Submitted to the 5th International Conference on Software Reuse, December, 1997. Garlan, D., Monroe, R., Wile, D. "ACME: An Architecture Description Interchange Language." Proceedings of CASCON'97, November, 1997. Melton, R., Garlan, D. "Architectural Unification." Proceedings of CASCON'97, November 1997. Garlan, D., Tomayko, J., Gluch, D. "Agents of Change: Educating Future Leaders in Software Engineering." IEEE Computer, November, 1997. Zaremski, A., Wing, J. "Specification Matching of Software Components." ACM Transactions on Software Engineering and Methodology, October, 1997. Jackson, D., Ng, Y., Wing, J. "A Nitpick Analysis of Mobile IPv6." Submitted to Formal Aspects of Computing, September, 1997. Allen, R., Garlan, D., Ivers, J. "Formal Modeling and Analysis of Architectural Standards." Submitted for publication, September, 1997. Kindred, D., Wing, J. "Closing the Idealization Gap with Theory Generation." Proceedings of the DIMACS Workshop on Cryptogaphic Protocol Design and Verification, Rutgers, NJ, September, 1997. (extended abstract) Allen, R., Garlan, D., Douence, R. "Specifying Dynamism in Software Architectures." Proceedings of the Workshop on Foundations of Component-Based Software Engineering (FASE), Zurich, Switzerland, September, 1997. Shaw, M., Clements, P. "A Field Guide to Boxology: Preliminary Classification of Architectural Styles for Software Systems." COMPSAC `97, August, 1997. Wing, J. " Subtyping for Distributed Object Stores." Proceedings of the Second IFIP International Workshop onFormal Methods for Open Object-based Distributed Systems (FMOODS), University of Kent at Canterbury, July, 1997, pp. 305-318. (invited paper) Allen, R., Garlan, D. "A Formal Basis for Architectural Connection." ACM Transactions on Software Engineering and Methodology, July, 1997. DeLine, R., Zelesnik, G., Shaw, M. "Lessons on Converting Batch Systems to Support Interaction." Proceedings of the 19th International Conference on Software Engineering, May, 1997, pp.195-204. Allen, R. "A Formal Approach to Software Architecture." Ph.D. Thesis, Carnegie Mellon University, May, 1997. CMU Technical Report CMU-CS-97-144. Ng, Y. "A Nitpick Specification of IPv6." B.S. in Computer Science, May 1997. O'Callahan, R., Jackson, D. "Lackwit: A Program Understanding Tool Based on Type Inference." Proceedings of the 19th International Conference on Software Engineering, May, 1997, pp. 338-348. Jackson, D., Jha, S., Damon, C. "Isomorph-free Model Enumeration: A New Method for Checking Relational Specifications." ACM Transactions on Programming Languages and Systems, accepted, to appear. Garlan, D., Wang, Z. "A Case Study in Software Architecture Interchange." Submitted for publication, February, 1998. Dingel, J., Garlan, D., Jha, S., Notkin, D. "Towards a Formal Treatment of Implicit Invocation." Accepted for publication in Formal Aspects of Computing. Wing, J., Vaziri-Farahani, M. "A Case Study in Model Checking Software Systems." Science of Computer Programming, Vol. 28, 1997, pp. 273-299. 4.0 List of Professional Personnel This section of the annual report satifies the requirements for section 2, subsection e) as outlined in Part IV, Article 15, Part C of Cooperative Agreement F30602-97-2-0031. 4.1 Faculty Mary Shaw, Alan J. Perlis Professor of Computer Science, Associate Dean for Professional Programs Jeannette Wing, Professor of Computer Science (Jeannette was elected ACM Fellow this year.) David Garlan, Associate Professor of Computer Science Daniel Jackson, Assistant Professor of Computer Science (Daniel left Carnegie Mellon University to join the Massachussetts Institute of Technology (MIT) in August, 1997.) 4.2 Graduate Students Robert Allen Shawn Butler Edwin Chan Craig Damon (Craig successfully proposed his thesis in October 1997.) Robert DeLine Darrell Kindred Ralph Melton Robert Monroe Robert O'Callahan (Robert successfully proposed his thesis in March 1998.) John Ockerbloom (John successfully defended his thesis in January 1998.) Siddhartha Puri Bridget Spitznagel Zhenyu Wang Hao-Chi Wong 4.3 Visitors and Postdocs Remi Douence, Postdoc 4.4 Staff James Ivers, Project Scientist Andrew Kompanek, Research Programmer Gregory Zelesnik, Principal Research Programmer 4.5 Advanced Degrees (accomplishments) Robert O'Callahan successfully proposed his PhD thesis entitled "Scalable Program Analysis and Understanding Based on Type Inference," March 16, 1998. John Ockerbloom successfully defended his PhD thesis entitled "Mediating Among Diverse Data Types," January 20, 1998. Craig Damon successfully proposed his PhD thesis entitled "Selective Enumeration," October 27, 1997. 5.0 Interactions (related activities) This section of the annual report satisfies the requirements for section 2, subsection f) as outlined in Part IV, Article 15, Part C of Cooperative Agreement F30602-97-2-0031. 5.1 Presentations This section describes papers presented at meetings, conferences, and seminars, as well as invited talks, and other presentations. David Garlan, Bob Monroe: EDCS Meeting, Santa Fe, NM Mary Shaw: Keynote Address. Fifth International Symposium on Assessment of Software Tools and Technologies Pittsburgh PA, June 1997. David Garlan (invited lecture): Software Architecture: Practice and Potential. Oregon Graduate Institute Beaverton OR, June 1997. Mary Shaw: Architecture Description presentation Quest Technology Awareness Symposium Schaumberh IL, April 1997. Mary Shaw (distinguished lecture) York University Toronto CA, March 1997. Robert Monroe: EDCS Demo Days Aesop Demonstration, Demonstration of Integration of Aesop/ACME/UniCon Seattle, WA, July 1997 Mary Shaw and Robert DeLine: EDCS Demo Days UniCon Demonstration, Demonstration of Integration of UniCon/ACME/Aesop Seattle, WA, July 1997 Darrell Kindred: EDCS Demo Days Revere Demonstration Seattle, WA, July 1997 Craig Damon: EDCS Demo Days Nitpick Demonstration Seattle, WA, July 1997 Jeannette Wing (invited speaker): Subtyping for Distributed Object Stores Second IFIP International Workshop on Formal Methods for Open Object-based Distributed Systems (FMOODS) University of Kent at Canterbury, July, 1997 Jeannette Wing (invited panelist): Panel on Funding for Software Research COMPSAC `97 Washington, DC, August, 1997. Mary Shaw (invited panelist): Internet Interactive Learning COMPSAC `97 Washington, DC, August, 1997. David Garlan (invited panelist): Architectural Languages and Design Environments: From Research to Practice. SEI Symposium Pittsburgh, PA, August, 1997. Zhenyu Wang: A Framework for Software Architecture Debugging Environments Information Sciences Institute (ISI) University of Southern California (USC), August 1997. Darrell Kindred and Jeannette Wing (workshop): Closing the Idealization Gap with Theory Generation DIMACS Workshop on Cryptogaphic Protocol Design and Verification Rutgers, NJ, September 1997. David Garlan: Software Architecture: Practice and Potential. University of Washington Seattle WA, September 1997. David Garlan: Software Architecture: Practice and Potential. University of California at Berkeley Berkeley, CA, September 1997. David Garlan: An Overview of Architecture Description Languages. Intel Corporation Santa Clara, CA, September 1997. David Garlan: Software Architecture Research at CMU. Hewlett Packard Laboratories Palo Alto, CA, September 1997. Robert Monroe (presentation): Armani (to) Martin Griss Hewlett Packard Laboratories Palo Alto, CA, September 1997. David Garlan and Robert Allen (Tutorial): Modeling and Analysis of Software Architecture SIGSOFT `97 Foundations of Software Engineering/European Software Engineering Conference Zurich, Switzerland, September 1997 Robert Monroe (demonstration): Aesop and ACME (to) Rockwell Executives Carnegie Mellon University, Pittsburgh, PA, September 1997. Gregory Zelesnik (presentation/demonstration): Composable Software Systems and UniCon (to) Rockwell Executives Carnegie Mellon University Pittsburgh, PA, September 1997. Robert Monroe (demonstration): Aesop and ACME (to) Rhoda Novak of The Aerospace Corporation Carnegie Mellon University Pittsburgh, PA, September 1997. Gregory Zelesnik (demonstration): UniCon (to) Rhoda Novak of The Aerospace Corporation Carnegie Mellon University Pittsburgh, PA, September 1997. Jeannette Wing DARPA ITO PI Meeting Austin Texas, November 10-12, 1997 Jeannette Wing CISE Advisory Committee meeting National Science Foundation (NSF) November 29 - December 1, 1997 David Garlan (invited talk): EDCS Research at CMU Lockheed-Martin Atlanta, GA, December 1997 David Garlan (DARPA Planning Workshop): AITS/EDCS Meeting Washington, D.C., January 23, 1998. Jeannette Wing (invited talk): Formal Methods: Past, Present, and Future Distinguished Lecture Series University of Washington, February 19, 1998. Mary Shaw (invited talk): Architecture Description Languages (ADLs) and UniCon IBM Toronto, Canada, February 24, 1998. David Garlan (DARPA Planning Workshop): Demo Days Planning Meeting Melbourne, FL, February 10-11, 1998. David Garlan (DARPA Planning Workshop): ACS/EDCS Meeting Washington, D.C., March 11, 1998. David Garlan (DARPA Planning Workshop): EDCS Spring Meeting Los Angeles, CA, March 16-17, 1998. 5.2 Consultative and Advisory Functions This section describes interactions with other institutions in a collaborative, consultative, or advisory capacity. 5.2.1 Collaboration With Integrators Global Transportation Network Lockheed-Martin made significant progress on incorporating and integrating Aesop and ACME into a technology demonstration for the July EDCS meeting. Worked with Dick Creps at Lockheed Martin to continue to transition CMU EDCS technology. 5.2.2 Collaboration With Other Projects in the Architecture Cluster Lockheed-Martin (Creps) We provided our prototypes to Lockheed-Martin for integration, and worked with them to develop sample applications. We provided the language reference manual for Version 3.0 of ACME to Lockheed-Martin. Worked with Paul Kogut of Lockheed Martin to define a collaborative demonstration for the EDCS Demo Days conference in July, 1998 involving CMU technology. We began collaborative work with Carolyn Talcott and Jose Meseuger on modeling Wright in Maude. Stanford University (Luckham) CMU created an ACME-based translator from Wright to Rapide. This tool uses the Rapide analysis and display tools. SRI (Moriconi) CMU worked with the developers of SRI's SADL to make sure that ACME can handle the constraints associated with architectural style and refinement. University of Texas (Batory) CMU held discussions on how Batory's notion of architectural refinement compares with DeLine's flexible component packaging and whether Batory's generator technology is a good tool to support DeLine's thesis work. USC/ISI (Balzer) Wang worked with Bob Balzer and Dave Wile at ISI to produce a software architecture debugging environment. USC/ISI (Wile) CMU extended their ADL tools (for Wright, UniCon, and Aesop) to read and write ACME specifications. This work leverages the ACME language definition, the ACMELib infrastructure, and some of the ACME-based tools. 5.2.3 Collaboration With Projects in the High Assurance Cluster University of Massachussets (Osterweil/Clarke) CMU worked with UMASS to combine the static checking capabilities of Wright with those of Flavors/INCA. MCC MCC expressed interest in integrating Nitpick into Quest. University of Washington (Notkin) Garlan collaborated with Notkin to develop formal models for reasoning about Implicit Invocation Architectures. 5.2.4 Collaboration With Projects in the Design Management Cluster CMU (Scherlis) O'Callahan held discussions with Scherlis' student Chan about applying a Java version of Lackwit to help them do code analysis. 5.2.5 Collaboration With Projects in the Dynamic Languages Cluster CMU (Falhman) CMU held discussions with the Gwydion project on how to incorporate some form of architecture description view and/or formally derived/described properties of software systems into their hypercode system. We met with Paul Hudak (Yale) to discuss his proposals for higher-order, polymorphic extensions to ACME. 5.2.6 Other Advisory Functions Jeannette Wing is a member of the Scientific Advisory Board for the National Science Foundation's (NSF) CISE Directorate. At Advisory Committee meetings she often discusses joint projects and programs between the NSF and the Defense Advanced Research Projects Agency (DARPA) with other committee members. 6.0 New Discoveries, Inventions, and Ideas This section of the annual report satisfies the requirements for section 2, subsection g) as outlined in Part IV, Article 15, Part C of Cooperative Agreement F30602-97-2-0031. We have had a simple insight that allows type theory, and its associated algorithms, to be exploited in the following context: reverse engineering of large C programs. The declared type of a function in a C program will rarely tell you as much as it might; a function might declare an argument to be a pointer, for example, even if it is never dereferenced. But by inferring, in a richer type system than C's, the most general type of a function, one can obtain detailed information about the use of data structures. We are now applying this idea to Java. For Revere, we achieved a significant technical goal by completely formalizing the theory generation approach, proving its soundness with respect to the (decidable) fragment of first-order theory it defines. In our research on using ML for architecture descriptions we identified a key language feature not directly supported by ML but needed to support software architecture description. This is the capability of defining recursive ML structures, which permits symmetric definition of connector attachment. In addition, we made a technical breakthrough in giving a type-theoretic semantics to an extension of the SML modules language, SML-mod-rec.