1.0 Participants
Carnegie Mellon University
Graduate Students
Visitors and Postdocs
Staff
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:
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.
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:
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:
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:
We used Nitpick to verify two properties of the Mobile IPv6 protocol (adopted as an IETF standard). This is described in the following work:
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:
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.
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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
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.
Yu-Chung Ng, A Nitpick Specification 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.
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.
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.
David Garlan, Robert Monroe, David Wile. ACME: An Architecture
Description Interchange Language.
Submitted for publication.
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.
6.0 Travel
The following meetings were attended by contract personnel:
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.
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.
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.