Publications (co-) authored by Rance Cleaveland: 2000

M. Bernardo and R. Cleaveland.
A Theory of Testing for Markovian Processes
In C. Palamidessi, editor, CONCUR 2000, volume 1877 of Lecture Notes in Computer Science, pages 305-319, State College, Pennsylvania, August 2000. Springer-Verlag.
(C)2000 Springer-Verlag.

We present a testing theory for Markovian processes in order to formalize a notion of efficiency which may be useful for the analysis of soft real-time systems. Our Markovian testing theory is shown to enjoy close connections with the classical testing theory of DeNicola-Hennessy and the probabilistic testing theory of Cleaveland-Smolka et al. The Markovian testing equivalence is also shown to be coarser than the Markovian bisimulation equivalence. A fully abstract characterization is developed to ease the task of establishing testing-related relationships between Markovian processes. It is then demonstrated that our Markovian testing equivalence, which is based on the (easier to work with) probability of executing a successful computation whose average duration is not greater than a given amount of time, coincides with the Markovian testing equivalence based on the (more intuitive) probability of reaching success within a given amount of time. Finally, it is shown that it is not possible to define a Markovian preorder which is consistent with reward-based performance measures, thus justifying why a generic notion of efficiency has been considered.

R. Cleaveland, X. Du and S. Smolka.
GCCS: A Graphical Coordination Language for System Specification
In A. Porto and G.-C. Roman, editors, COORDINATION 2000, volume 1906 of Lecture Notes in Computer Science, pages 284-298, Limassol, Cyprus, September 2000. Springer-Verlag.
(C)2000 Springer-Verlag.

We present GCCS, a graphical coordination language for hierarchical concurrent systems. GCCS, which is implemented in the Concurrency Factory design environment, represents a coordination model based on process algebra. Its coordination laws, given as a structural operational semantics, allow one to infer atomic system transitions on the basis of transitions taken by system components. We illustrate the language's utility by exhibiting a GCCS-coordinated specification of the Rether real-time ethernet protocol. The specification contains both graphical and textual components.

R. Cleaveland and S.Purushothaman Iyer.
Branching Time Probabilistic Model Checking
In J.D.P. Rolim, et al., editors, ICALP Workshops 2000, volume 8 of Proceedings in Informatics, pages 487-500, Geneva, July 2000. Carleton Scientific.
(C)2000 Carleton Scientific.

This paper presents a probabilistic semantics for the alternation-free modal mu-calculus. This semantics precisely defines the probability with which a system that includes a mixture of probabilistic and nondeterministic choices satisfies a formula in the logic. An algorithm for computing these probabilities is also given.

R. Cleaveland and G. Lüttgen.
A Semantic Theory for Heterogeneous System Design
In S. Kapoor and S. Prasad, editors, Foundations of Software Technology and Theoretical Computer Science, volume 1974 of Lecture Notes in Computer Science, pages 312-324, New Delhi, December 2000. Springer-Verlag.
(C)2000 Springer-Verlag.

This paper extends DeNicola and Hennessy's testing theory from labeled transition system to Büchi processes and establishes a tight connection between the resulting Büchi must--preorder and satisfaction of linear--time temporal logic (LTL) formulas. An example dealing with the design of a communications protocol testifies to the utility of the theory for heterogeneous system design, in which some components are specified as labeled transition systems and others are given as LTL formulas.

G. Lüttgen, M. van der Beeck and R. Cleaveland
A Compositional Approach to Statecharts Semantics
In D. Rosenblum, editor, Eighth International Symposium on Foundations of Software Engineering, pages 120-129, San Diego, California, November 2000. ACM Press.
(C)2000 ACM

Statecharts is a visual language for specifying reactive system behavior. The formalism extends traditional finite--state machines with notions of hierarchy and concurrency, and it is used in many popular software design notations. A large part of the appeal of Statecharts derives from its basis in state machines, with their intuitive operational interpretation. The traditional semantics of Statecharts, however, suffers from a serious defect: it is not compositional, meaning that the behavior of system descriptions cannot be inferred from the behavior of their subsystems. Compositionality is a prerequisite for exploiting the modular structure of Statecharts for simulation, verification, and code generation, and it also provides the necessary foundation for reusability.

This paper suggests a new compositional approach to formalizing Statecharts semantics as flattened transition systems in which transitions represent system steps. The approach builds on ideas developed for timed process calculi and employs structural operational rules to define the transitions of a Statecharts expression in terms of the transitions of its subexpressions. It is first investigated for a simple dialect of Statecharts, with respect to a variant of Pnueli and Shalev's semantics, and is illustrated by means of a small example. To demonstrate its flexibility, the proposed approach is then extended to deal with practically useful features available in many Statecharts variants, namely state references, history states, and priority concepts along state hierarchies.

Go to Rance Cleaveland's publication home page.

Rance Cleaveland
Last modified: Tue Jan 2 10:46:31 EST 2001