Publications (co-)authored by Rance Cleaveland: 2002

R. Cleaveland and H. Garavel, editors.
FMICS'02: 7th International ERCIM Workshop in Formal Methods for Industrial Critical Systems.
Volume 66, number 2 of Electronic Notes in Theoretical Computer Science. Elsevier Science, University of Malaga, Spain, December 2002. ISBN: 0444513418.
©2002 Elsevier.

R. Cleaveland and S. Sims.
Generic Tools for Verifying Concurrent Systems.
Science of Computer Programming 41(1):39-47, January 2002.
©2002 Elsevier. Abstract:

Despite the enormous strides made in automatic verification technology over the past decade and a half, tools such as model checkers remain relatively underused in the development of software. One reason for this is that the bewildering array of specification and verification formalisms complicates the development and adoption by users of relevant tool support. This paper proposes a remedy to this state of affairs in the case of finite-state concurrent systems by describing an approach to developing customizable yet efficient verification tools.

R. Cleaveland and G. Luettgen.
A Logical Process Calculus.
In U. Nestmann and P. Panangaden, editors, 9th International Workshop on Expressiveness in Concurrency, volume 68 of Electronic Notes in Theoretical Computer Science Brno, Czech Republic, August 2002. Elseveier Science.
©2002 Elsevier Science B.V. Abstract:

This paper presents the Logical Process Calculus (LPC), a formalism that supports heterogeneous system specifications containing both operational and declarative subspecifications. Syntactically, LPC extends Milner's Calculus of Communicating Systems with operators from the alternation--free linear--time mu--calculus (LTm). Semantically, LPC is equipped with a behavioral preorder that generalizes Hennessy's and De Nicola's must--testing preorder as well as LTm's satisfaction relation, while being compositional for all LPC operators.

From a technical point of view, the new calculus is distinguished by the inclusion of (i) both minimal and maximal fixed--point operators and (ii) an unimplementability predicate on process terms which tags inconsistent specifications. The utility of LPC is demonstrated by means of an example highlighting the benefits of heterogeneous system specification.

R. Grosu, E. Zadok, S. Smolka, R. Cleaveland and Y. Liu
High-Confidence Operating Systems
In Tenth ACM SIGOPS European Workshop, Saint-Emilion, France, September 2002. ACM Press.
©2002 ACM. Abstract:

None available.

B. Sengupta and R. Cleaveland
Triggered Message Sequence Charts.
In SIGSOFT2002/FSE-10, Charleston, SC, USA, November 2002. ACM Press.
©2002 ACM. Abstract:

We propose an extension to Message Sequence Charts called Triggered Message Sequence Charts (TMSCs) that are intended to capture system specifications involving nondeterminism in the form of conditional scenarios. The visual syntax of TMSCs closely resembles that of MSCs; the semantics allows us to translate a TMSC specification into a framework that supports a notion of refinement based on Denicola's and Hennessy's must preorder. A simple but non-trivial example illustrates the utility of our extension to MSCs.

This paper has been subsumed by a journal version.

L. Tan and R. Cleaveland
Evidence-Based Model Checking.
In E. Brimksma and K.G. Larsen, editors, Computer-Aided Verification 2002, volume 2404 of Lecture Notes in Computer Science, pages 455-470, Copenhagen, July 2002. Springer Verlag.
©2002 Springer Verlag. Abstract:

This paper shows that different ``meta-model-checking'' analyses can be conducted efficiently on a generic data structure we call a support set. Support sets may be viewed as abstract encodings of the ``evidence'' a model checker uses to justify the yes/no answers it computes. We indicate how model checkers may be modified to compute supports sets without compromising their time or space complexity. We also show how support sets may be used for a variety of different analyses of model-checking results, including: the generation of diagnostic information for explaining negative model-checking results; and certifying the results of model checking (is the evidence internally consistent?).

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