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.

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.

None available.

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.

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?).