Publications (co-)authored by Rance Cleaveland: 2003

A. Ray and R. Cleaveland.
Architectural Interaction Diagrams: AIDs for System Design.
In International Conference on Software Engineering, pages 396-407, Portland, Oregon, May 2003. IEEE Computer Society Press.
©2003 IEEE.

This paper develops a modeling paradigm called Architectural Interaction Diagrams, or AIDs, for the high-level design of systems containing concurrent, interacting components. The novelty of AIDs is that they introduce interaction mechanisms, or buses, as first-class entities into the modeling vocabulary. Users then have the capability, in their modeling, of using buses whose behavior captures interaction at a higher level of abstraction than that afforded by modeling notations such as Message Sequence Charts or process algebra, which typically provide only one fixed interaction mechanism. This paper defines AIDs formally by giving them an operational semantics that describes how buses combine subsystem transitions into system-level transitions. This semantics enables AIDs to be simulated; to incorporate subsystems given in different modeling notations into a single system model; and to use testing, debugging and model checking early in the system design cycle in order to catch design errors before they are implemented.

B. Sengupta and R. Cleaveland.
Towards Formal But Flexible Scenarios
In S. Uchitel, editor, Proceedings of the Second International Workshop on Scenarios and State Machines: Models, Algorithms and Tools,, Portland, Oregon, May 2003. Satellite workshop of the International Conference on Software Engineering.

We argue that the evident utility of scenario-based modeling can be greatly enhanced when enriched with a mathematically precise notion of conditionality and partiality, such as that found in Triggered Message Sequence Charts (TMSCs). Unlike traditional Message Sequence Charts, the TMSC formalism allows scenarios to be conditional and partial, supports logical as well as behavioral operators for scenario composition, and is equipped with a refinement notion drawn from traditional process theory that provides a rigorous basis for stepwise development of specifications. This paper illustrates these points via the Center TRACON Automation System for flight control.

B. Sengupta and R. Cleaveland.
TRIM: A Tool for Triggered Message Sequence Charts.
In W. Hunt and F. Somenzi, editors, Computer-Aided Verification 2002, volume 2725 of Lecture Notes in Computer Science, pages 106-109, Boulder, Colorado, July 2003. Springer Verlag.
©2003 Springer Verlag.

TRIM is a tool for analyzing system requirements expressed using Triggered Message Sequence Charts (TMSCs). TMSCs enhance MSCs with capabilities for expressing conditional and partial behavior and with a refinement ordering. This paper shows how the Concurrency Workbench of the New Century may be adapted to check refinements between TMSC specifications.

B. Sengupta and R. Cleaveland.
Refinement-Based Requirements Modeling Using Triggered Message Sequence Charts
In Eleventh IEEE International Requirement Engineering Conference, pages 95-104, Monterey, California, September 2003. IEEE Computer Society Press.
©2003 ACM.

Triggered Message Sequence Charts (TMSCs) are a visual, mathematically precise notation for capturing system requirements as conditional and partial scenarios. This paper shows how TMSCs may be used to formalize two different requirements modeling methodologies. The first approach combines prescriptive (``do this'') and constraint-based (``don't do that'') requirements within a single specification; it is useful for composing localized subsystem requirements with global system ones. The second approach supports layered specifications in which partial descriptions of requirements may be elaborated on in a succession of steps; it is suitable for the incremental development of complex behavior in which ``error'' scenarios are ``layered on top of'' normative ones. Both methodologies derive their formal robustness from the notion of semantic refinement for TMSCs, which is based on DeNicola's and Hennessy's must preorder. Case studies are used to illustrate the utility of the work.

E. Stark, R. Cleaveland and S. Smolka.
A Process-Algebraic Language for Probabilistic I/O Automata.
In R. Amadio and D. Lugiez, editors, CONCUR'03, volume 2761 of Lecture Notes in Computer Science, pages 193-207, Marseille, France, September 2003. Springer-Verlag.
©2003 Springer-Verlag.

We present a process-algebraic language for Probabilistic I/O Automata (PIOA). To ensure that PIOA specifications given in our language satisfy the ``input-enabled'' property, which requires that all input actions be enabled in every state of a PIOA, we augment the language with a set of type inference rules. We also equip our language with a formal operational semantics defined by a set of transition rules. We present a number of results whose thrust is to establish that the typing and transition rules are sensible and interact properly. The central connection between types and transition systems is that if a term is well-typed, then in fact the associated transition system is input-enabled. We also consider two notions of equivalence for our language, weighted bisimulation equivalence and PIOA behavioral equivalence. We show that both equivalences are substitutive with respect to the operators of the language, and note that weighted bisimulation equivalence is a strict refinement of behavioral equivalence.

D. Zhang, R. Cleaveland and E. Stark.
The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems
In H. Garavel and J. Hatcliff, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 2619 of Lecture Notes in Computer Science, pages 431-436, Warsaw, Poland, April 2003. Springer-Verlag.
©2003 Springer-Verlag.

This paper reports on an effort to integrate two verification tools, the Concurrency Workbench of the New Century (CWB-NC) and PIOATool. Our aim is to build a single tool that combines the ``functional'' analysis capabilities of the CWB-NC with the compositional performance-analysis features of PIOATool. We discuss some of the issues involved in the integration, highlighting a particular integration paradigm in which one tool becomes a subshell of the other.

Rance Cleaveland
Last modified: Thu Oct 26 15:43:32 Eastern Daylight Time 2006