1.0 Participants

Carnegie Mellon University

Faculty
David Garlan Associate Professor of Computer Science
Mary Shaw Alan J. Perlis Professor of Computer Science, Associate Dean for Professional Programs
Jeannette Wing Professor of Computer Science


Graduate Students

Shawn Butler
Craig Damon
Robert DeLine
Darrell Kindred
Robert Monroe
Robert O'Callahan
John Ockerbloom
Siddhartha Puri
Bridget Spitznagel
Zhenyu Wang
Hao-Chi Wong


Visitors and Postdocs

Staff

James Ivers Project Scientist
Andrew Kompanek Research Programmer
Gregory Zelesnik Principal Research Programmer

2.0 Ongoing Research & Development

The following are the on-going research and development activities for the Composable Software Systems group.

We investigated a new approach to architectural refinement that allows us to adapt formal theories of refinement to architectural designs. We began to develop a connector calculus that should ultimately allow us to reason about (and implement) complex connectors as a composition of more primitive parts.

Research continues on the Armani software architecture design language. Armani extends the ACME architecture description language with constructs for capturing architectural design expertise and design constraints. We developed an initial version of an Armani language reference manual, and prototype tools. As part of this work, we developed a formal, set-theoretic semantics for architectural constraints that permits one to incorporate predicates into the type checking rules for architectures. This semantics is based on a PVS-style interpretation of "types as predicates over sets".

We continue to develop extensions of Wright to permit description of dynamically-reconfigurable architectures and allow automated analysis of these descriptions.

We continue to apply 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.

We continue to use Aesop to develop new styles and analyses for architectural design. We continue to find ways to integrate Aesop with evolving ACME facilities and tools.

We continue our research on the next generation of the UniCon language, UniCon 2. We are currently designing the language and the next generation of tools to edit and compile descriptions in the language. 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 continue to investigate the relationship between modules in advanced programming languages and ADLs. In particular, we envision that SML-mod-rec can be used as an "intermediate language" into which many existing ADLs can translate. SML-mod-rec has the potential to handle dynamism for ADLs too. We will build support for SML-mod-rec by extending the existing SML TIL compiler.

We continue to make progress on showing how the theory generation approach, in its full generality, can be used to specify and reason about authentication protocols and the relationship between a concrete protocol and its BAN abstract version.

We continue to make progress on formally defining the techniques used by Nitpick and the next generation tool, Ladybug (see below).

We continue to make progress on Lackwit's successor for Java: a code-level analysis tool based on type inference for finding data dependencies in large-scaled software systems.

We continue our work with analyzing security protocols.

On-going support is being provided to users and evaluators of Armani, Aesop, the ACMELib library and toolset, Lackwit, Revere, and the UniCon toolset.

The UniCon toolset has now been acquired by 227 organizations in 36 different countries.

The following represent the accomplishments and the technology transition activities accomplished by the Composable Software Systems group during the reporting period.

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. Before this quarter, we didn't know whether it was even feasible.

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.

For Nitpick, a new framework for formally describing and analyzing the underlying techniques was developed. Using this framework, the techniques have been proven sound.

A second generation tool, LadyBug, is in final pre-beta-release testing. 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 by implementing LadyBug in Java
ability to easily plug in alternative solver methods to enable effective comparisons between techniques.
internal support for additional specification language features, including numbers and inheritance, with the eventual expectation of supporting the UML constraint language OCL

The thesis proposal by Rob O'Callahan based on his successor to Lackwit (applied to Java) was presented and passed.

Wright models led to better understanding and minor revisions in the DMSO HLA specification for time management services for distributed simulation. Some of our formal architectural models are now being used (by DMSO) as a part of the new HLA specification.

In the UniCon 2 toolset, we implemented multiple inheritance of properties in extendable language definitions. We also made 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. We also implemented remote builds, meaning that the toolset can build descriptions targetted for the Unix and Windows NT platforms, even though they are hosted on Windows NT platforms themselves.

In UniCon 2 and the associated toolset, 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. The editor was also enhanced to load descriptions written in any architectural style: unknown component and connector abstractions are rendered with default shapes.

In the UniCon 2 tool suite, we have started implementing conversions to and from ACME. The UniCon->ACME translator is nearly complete.

COLLABORATION WITH INTEGRATORS

Global Transportation Network

Worked with Dick Creps at Lockheed Martin to continue to transition CMU EDCS technology.

COLLABORATION WITH OTHER PROJECTS IN ARCHITECTURE CLUSTER

Lockheed-Martin (Creps)

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.

COLLABORATION WITH PROJECTS IN HIGH ASSURANCE CLUSTER

No new progress to report.

COLLABORATION WITH PROJECTS IN DESIGN MANAGEMENT CLUSTER

No new progress to report.

COLLABORATION WITH PROJECTS IN DYNAMIC LANGUAGES CLUSTER

We met with Paul Hudak (Yale) to discuss his proposals for higher-order, polymorphic extensions to ACME.

5.0 Publications

The following are the papers that have been authored by the members of this contract during the reporting period. They have been organized into groups based on their status as submitted, accepted, or published. They represent transition of our research to the community at large.

Published

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.

Garlan, D.
Higher-Order Connectors.
Proceedings of the Workshop on Compositional Software Architectures, January, 1998.

Jackson, D., Ng, Y., Wing, J.M.
A Nitpick Analysis of Mobile IPv6
CMU Technical Report CMU-CS-98-113, March, 1998.

Wang, Z.
Separating Application Logic from Architectural Concerns - Beyond Object Services and Frameworks
Proceedings of Workshop on Compositional Software Architectures, January, 1998.

Accepted

Dingel, J., Garlan, D., Jha, S., Notkin, D.
Towards a Formal Treatment of Implicit Invocation
Accepted for publication in Formal Aspects of Computing.
Spitznagel, B., Garlan, D.
Architecture-Based Performance Analysis.
Accepted for publication at the 10th International Conference on Software Engineering and Knowledge Engineering (SEKE'98), June, 1998.
Leavens, G., Wing, J.M.
Protective Interface Specifications
Accepted for publication in Formal Aspects of Computing, March, 1998.
Vaziri, M., Lynch, N., Wing, J.M.
Proving the Correctness of a Controller Algorithm for the RAID Level 5 System
Accepted for publication in Fault-Tolerant CS, 1998.

Submitted

Allen, R., Garlan, D., Ivers, J.
Formal Modeling and Analysis of Architectural Standards.
Submitted for publication.
Garlan, D., Wang, Z.
A Case Study in Software Architecture Interchange.
Submitted for publication February 15, 1998.

6.0 Travel

The following are the talks, presentations, panels, lectures, workshops, and demonstrations given by the members of this contract during the reporting period. They represent transition of our research to the community at large.

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
February 24, 1998.

David Garlan (DARPA Planning Workshop):
AITS/EDCS Meeting
Washington, D.C.
January 23, 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.

7.0 Miscellaneous/Administrative/Problematic Issues

None to report.

8.0 Plans For The Next Reporting Period

We plan to continue our redesign of the UniCon 2 language and toolset. Specifically, we plan to start work on a Database connector abstraction for UniCon 2. We also plan to implement an ACME to UniCon translator. Additionally, we plan to augment the UniCon 2 graphical editor to be able to perform edit operations on graphical descriptions.

We plan to continue helping Lockheed-Martin incorporate CMU technology into the next demonstration for the EDCS "Demo Days" '98.

We plan to finish writing up our most recent results on our experience with integrating Aesop, UniCon, and ACME.

Continue to apply Wright to the HLA, develop Armani language and tools, understand architectural refinement, and higher-order connectors.

We plan to transition prototype Armani environment to Lockheed Martin for incorporation in their July Demo.

We plan to complete the thesis work on Revere.

We plan to publicly release the next generation Nitpick tool, Ladybug.

We plan to continue progress on Lackwit (and the Java version), Nitpick, and Ladybug.