Status Report: A Technology Investigation Supporting Software Architecture and Analysis for Evolution

Agreement/Contract Number: F30602-97-2-0031

For the period: April 1997 through June 1997

Principal Investigators: David Garlan and Mary Shaw

Carnegie Mellon University

5000 Forbes Avenue

Pittsburgh, PA 15213-3891

E-mail: garlan@cs.cmu.edu, mary.shaw@cs.cmu.edu

WWW Homepage: http://www.cs.cmu.edu/~Compose/

Voice: 412-268-5056 (Garlan); 412-268-2589 (Shaw)

FAX: 412-268-5576


1.0 Participants

Carnegie Mellon University

2.0 Ongoing Research & Development

We delivered a new release of UniCon this period. The toolset has now been acquired by 145 organizations in 28 different countries:

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 Architectures for Software Systems.

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 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 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 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.

3.0 Notable Accomplishments & Technology Transition

Notable Accomplishments

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

We performed the following tasks in support of the EDCS "Demo Days" Conference to be held in Seattle, July 21-24, 1997:

Technology Transition

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

We transitioned the UniCon toolset to the University of Oregon for inclusion into their course on Software Architectures.

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/~revere

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

4.0 Progress on Inter/Intra Cluster Collaborations

COLLABORATION WITH INTEGRATORS

Global Transportation Network

Lockheed-Martin made significant progress on incorporating and integrating the following CMU technology:

  • Aesop
  • ACME

COLLABORATION WITH OTHER PROJECTS IN ARCHITECTURE CLUSTER

Lockheed-Martin (Creps)

We provided our prototypes to Lockheed-Martin for integration.

Stanford University (Luckham)

CMU made progress on an ACME-based translator from Wright to Rapide. This tool uses the Rapide analysis and display tools.

SRI (Moriconi)

CMU started working 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 began discussion 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 began working with Bob Balzer and Dave Wile at ISI to produce a software architecture debugging environment.

USC/ISI (Wile)

CMU has begun extending our 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

COLLABORATION WITH PROJECTS IN HIGH ASSURANCE CLUSTER

University of Massachussets (Osterweil/Clarke)
CMU began working 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 has been collaborating with Notkin to develop formal models for reasoning about Implicit Invocation Architectures.

COLLABORATION WITH PROJECTS IN DESIGN MANAGEMENT CLUSTER

CMU (Scherlis)

O'Callahan talked with Scherlis' student Chan about applying a Java version of Lackwit to help them do code analysis.

COLLABORATION WITH PROJECTS IN DYNAMIC LANGUAGES CLUSTER

CMU (Falhman)

CMU has discussed with the Gwydion project how to incorporate some form of architecture description view and/or formally derived/ described properties of software systems into our hypercode system.

5.0 Publications

The following are the papers authored by this group during the reporting period. 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.

6.0 Travel

The following meetings were attended by contract personnel:

EDCS Meeting, Santa Fe, NM

David Garlan
Bob Monroe

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

7.0 Miscellaneous/Administrative/Problematic Issues

None to report this period.

8.0 Plans For The Next Reporting Period

We plan to make progress on the preliminary design of UniCon 2. UniCon 2 improvements will 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 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 work to begin on improved versions of tools for performance modelling, architectural visualization, and layout.

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

We plan to begin checking 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 begin research on finding 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 start looking 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.