Project Summary

Organization:

Carnegie Mellon University

Subcontractors:

None

Principal Investigators:

Mary Shaw	shaw+@cs.cmu.edu	(412) 268-2589 
David Garlan	garlan+@cs.cmu.edu	(412) 268-5056 
Daniel Jackson	dnj+@cs.cmu.edu		(412) 268-5143 
Jeannette Wing	wing+@cs.cmui.edu	(412) 268-3068

Title of Effort:

Software Sciences and Engineering Research: Composable Software Systems

Objective:

To provide a scientific and engineering basis for designing, building, and analyzing composable software systems. To provide languages, tools, environments, and techniques to support these activities.

Approach:

The three research lines are software architecture, formal methods, and tractable software analysis. This project will develop new models, theories, methods, languages, and tools for classifying, specifying, analyzing, and designing software systems beyond the component level. This support could lead to substantial reduction in maintenance costs, improvement in software reuse, and increase in quality of software.

1997 Accomplishments:

We delivered three new releases of UniCon this year. The toolset has now been acquired by 145 organizations in 28 different countries:

Version 3.4 (October 30, 1996)

The graphical editor is now completely integrated with the compiler of the textual language. All editing and building operations in the editor use the compiler's programming interface to manipulate internal data structures representing the graphical description. The editor no longer analyzes an architectural description by invoking the compiler in the background on equivalent textual versions of the graphical architectural description. The analysis and building is performed from the internal representation. This has significantly increased the speed of the building and analysis operations in the graphical editor.

All memory leaks have been removed from the textual compiler and the compiler's programming interface with the Purify utility from Pure Software, Inc. This means that the graphical editor can be active indefinitely without it running out of memory.

The look and feel of the graphical editor has been updated, and errors encountered in a build or analysis operation are now reflected graphically in an architectural description.

There is a new connector in the UniCon language: the DML connector. It connects database components with applications written in C that access them.

Distributed RPC connections among platforms in a heterogenous environment involving linux, solaris, and sunos systems has been made robust.

Version 4.0 (January 20, 1997)

The problems with building and running the graphical editor on Linux systems have been ironed out. The editor is now as robust in the Linux environment as it is on Solaris and SunOS platforms.

A new connector has been added to the compiler and the graphical editor: the SharedMemory connector. This connector allows the sharing of global data between processes on the same unix platform. The glue code in the connector consists of calls to the Unix shared memory API, namely the shmget, shmat, shmdt C library routines.

Version 4.1 (May 5, 1997)

The graphical editor has been tested extensively. It is as stable as the textual compiler. It is now safe to build a system of executable programs from a UniCon architectural description within the graphical editor at any arbitrary step in the specification process. Builds can be attempted on partial and incomplete specifications. The editor provides both graphical and textual feedback (the textual feedback appears in the STk interpreter window) regarding compilation and building errors.

Included in this distribution is a Rate Monotonic Analysis tool, written in C. It is invoked by the graphical editor during the build function and the textual compiler during the semantic analysis phase. It is invoked automatically to perform a rate monotonic analysis (RMA) on a UniCon architectural description involving RTScheduler connectors that have the Algorithm property set to "rate_monotonic". The output of this tool indicates whether or not the system of schedulable processes (i.e., the components of type SchedProcess) connected to a given processor resource in the real-time system is schedulable. The tool identifies the events that are found in the system, and then reports the period information and the calculated worst-case response time for each event. This tool can also be run in a stand-alone fashion.

Also included in this distribution is the UniCon-to-ACME translator. The translator is part of the UniCon textual compiler, uparse, which is included in each distribution. In this distribution a new option has been added to this compiler (i.e., the "-a" option) that, when selected, analyzes the input as if the user had selected the "-b" option (i.e., a build). However, rather than proceeding with a build, the compiler generates an ACME description and outputs it to a file with a .acme extension.

We implemented capability for converting UniCon to ACME and vice-versa. The UniCon-to-ACME converter is part of the UniCon textual compiler and was delivered with release 4.1 of the UniCon toolset. The ACME-to-UniCon translator has been completed and will be delivered with release 4.2 of the UniCon toolset.

The UniCon toolset was used to support a class in Software Architecture at the University of Oregon. This class was being taught by Professor Marilynn Livingston (mlivings@cs.uoregon.edu).

We delivered the Carnegie Mellon University (CMU) Master of Software Engineering (MSE) Software Architecture course again at CMU. The course material was captured for on-line dissemination. This includes course schedule and syllabus, lecture slides, reading assigments, project assignments, bibliography, and some of the actual readings. The course lectures were also videotaped for possible on-line dissemination as well. See http://www.cs.cmu.edu/afs/cs/project/tinker-arch/www/html/index.html.

We classified architectural styles in the following work:

Mary Shaw and Paul Clements. A Field Guide to Boxology: Preliminary Classification of Architectural Styles for Software Systems. COMPSAC '97, to appear.

We explicated the relationship between architectural packaging decisions (batch or interactive) and internal structure of a system's implementation. This can be found in the following work:

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.

We developed a novel logic-based approach, theory generation, to checking properties of protocols. It is described in the following work:

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

In this approach, we generate a finite representation of a theory given a logic and the protocol to be checked; checking a property of the protocol is a simple membership test. Darrell Kindred built a tool called Revere to embody this approach. It is fast and completely automatic. The speed in checking protocol designs is on the order of recompiling the protocol specification. We applied this approach to checking authentication protocols based on the Burrows-Abadi-Needham Logic of Authentication. We verified all the protocols in the original BAN paper (identifying the same flaws that they did by hand) and all the relevant protocols in Chapter 3 of Schneier's "Applied Cryptography" book.

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 in the fall of 1997; it is not only cleaner but also performs significantly better. This new algorithm is described in the following work:

Daniel Jackson, Somesh Jha, Craig A. 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.

We have been researching new boolean-based specification checking and bounded generation techniques for our Nitpick tool.

Nitpick checks properties of software specifications by exhaustive enumeration of states. For complex states involving many relations, functions and sets, the state space is vast. The current Nitpick tool employs a variety of mechanisms to reduce the space. The first is symmetry reduction; it avoids considering a state that is symmetrical to one already analyzed. The second is short circuiting; it avoids enumerating the values of a particular state variable when it can be determined, from the values of other variables already assigned, that the property will be satisfied however the state assignment is completed. Together, these have enabled us to check some complex specifications, but the method is still very sensitive to the number of variables.

Short circuiting essentially provides a weak form of goal-directedness. Values of variables are considered in their entirety - that is, a whole function, or a whole set. If it were possible to consider partial values, the goal-directedness could be much improved. We have started to work on a new checking engine that considers the arcs of a function or relation one at a time, so that the search has a finer granularity. Our scheme involves translating the relational specification into a boolean formula and applying satisfiability algorithms. It builds on our previous work, and exploits some of the ideas from our symmetry work.

We have also been working on a scheme that improves the explicit search method. "Bounded generation" allows only the values of a relation to be generated that are known in advance to satisfy a constraint. For example, given a constraint that p is a sub-relation of q, and given that q has already been generated, the generation of p can be limited to sub-relations of q. A prototype implementation of bounded generation has been constructed, and appears to result in considerable speedup for a variety of specifications.

We used Nitpick to verify two properties of the Mobile IPv6 protocol (adopted as an IETF standard). This is described in the following work:

Yu-Chung Ng, A Nitpick Specification of IPv6, Senior Honors Thesis, Computer Science Department, Carnegie Mellon University, May 1997.

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 IPv4 does not have the same error. We also found that a feature that was originally included as a performance optimization was necessary for the correctness of the protocol.

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. Robert O'Callahan has 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; 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 seems to scale 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. The approach and tool are described in the following work:

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.

We applied the Wright Architecture Specification Language to the DMSO High-Level Architecture for distributed simulation. We discovered a number of bugs in the published architectural specification, which have led to revisions in more recent versions of the specification.

We made progress on developing a new formal basis for modeling of 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.

We developed a new tool for architectural performance analysis. The tool applies classical queueing-theoretic results from hardware performance modeling to software architecture. Given an architecture based on asynchronous message passing, annotated with estimates of individual component processing times, the tool will calculate overall system throughputs and latencies, and identify system bottlenecks.

We developed an ACME-based tool that converts Wright specifications into Rapide specifications. This permits the incorporation of Rapide tools (e.g., for POSET viewing, animation, and anomaly detection) into the Wright tool suite.

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 upgraded the Aesop design tools to be compatible with ACME 3.0 release. This allows tools such as ACME and Wright to interact with other EDCS-supported, ACME compliant architectural design tools.

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.

FY98 Plan:

We plan to finish the design and implementation of UniCon 2. UniCon 2 improvements include improved type checking, improved support for adding connector types, evolvable specifications, support for adding component types, and improvements in multi-level definition handling.

We plan to re-target UniCon 2 to handle PCs, probably rehosting in the process.

We plan to add component and connector types in UniCon 2 for architectures commonly found on PCs, including ActiveX, CORBA, etc.

We plan to refine the credentials model in UniCon 2 for evolving specifications.

We plan to concentrate on a full suite of component/connector types in UniCon 2 to support an application area, specifically on-line education.

We plan to classify means of repairing architectural mismatch.

We plan to design and implement flexible packaging for mismatch alleviation.

We plan to continue developing tools for architectural modeling and analysis, extending our results in the domain of distributed simulation, and improving our publicly available tools (Aesop and Wright). Specifically, expect improved versions of tools for performance modelling, architectural visualization, and layout.

We plan to continue developing techniques and formalisms for specifying and analyzing dynamic architectures.

We plan to check security protocols not only for standard properties like authentication but properties heretofore never formally verified like honesty, responsibility, and feasibility. The plan is to use the same theory generation approach to do these checks.

We plan to find an automated way to provide feedback to the security protocol designer about why a property does or does not hold when checked using the "theory generation" approach.

We plan to look at using Lackwit to analyze Java programs. Many of the ideas will apply straightforwardly; subtyping is perhaps the only major challenge. We have had to address similar issues in the handling of type coercions in C, so we are fairly confident that Lackwit for Java will be a success.

We plan to develop the boolean version of Nitpick and test it on our now extensive suite of examples. We also plan to complete the version of Nitpick based on bounded generation, and test it. In both of these, we expect to see dramatic performance improvements over our current implementation, making Nitpick applicable to a wide range of realistic problems.

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 http://www.cs.cmu.edu/~UniCon)
Point of Contact	Gregory Zelesnik (UniCon-Distribution@cs.cmu.edu)
URL	http://www.cs.cmu.edu/~UniCon

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 (cdamon@cs.cmu.edu)
URL	http://www.cs.cmu.edu/~nitpick

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 (garlan@cs.cmu.edu)
URL	http://www.cs.cmu.edu/~able/aesop

4. ACME

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 (garlan@cs.cmu.edu)
URL	http://www.cs.cmu.edu/~able/acme-web/v3.0/alpha-dist/alpha-dist.html

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 (dkindred@cmu.edu)
URL	http://www.cs.cmu.edu/~UniCon

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 (roc@cs.cmu.edu)
URL	http://www.cs.cmu.edu/~roc/Lackwit.html

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.