Last update: Sun Aug 5 02:03:07 MDT 2018
@Article{Cleaveland:2000:SFC,
author = "Rance Cleaveland",
title = "Specification formalisms for component-based
concurrent systems",
journal = j-SIGSOFT,
volume = "25",
number = "1",
pages = "42--43",
month = jan,
year = "2000",
CODEN = "SFENDP",
DOI = "https://doi.org/10.1145/340855.340876",
ISSN = "0163-5948 (print), 1943-5843 (electronic)",
ISSN-L = "0163-5948",
bibdate = "Wed Aug 1 17:13:50 MDT 2018",
bibsource = "http://www.math.utah.edu/pub/tex/bib/sigsoft2000.bib",
abstract = "This project builds on my ongoing research into design
formalisms for, and the automatic verification of,
concurrent systems. The difficulties such systems pose
for system engineers are well-known and result in large
part from the the complexities of process interaction
and the possibilities for nondeterminism. My work is
motivated by a belief that mathematically rigorous
specification and verification techniques will
ultimately lead to better and easier-to-build
concurrent systems. My specific research interests lie
in the development of fully automatic analysis methods
and process-algebraic design formalisms for modeling
system behavior. I have worked on algorithms for
checking properties of, and refinement relations
between, system descriptions [CH93, CS93]; the
implementation and release of a verification tool, the
CWB-NC [CS96] (see http://www.cs.sunysb.edu/~rance to
obtain the distribution); case studies [BCL99, ECB97];
and the formalization of system features, such as real
time, probability, and priority, in process algebra
[BCL99, CDSYar]. The aims of this project include the
development of expressive and usable formalisms for
specifying and reasoning about properties of open,
component-based concurrent systems. More specifically,
my colleagues and I have been investigating new
approaches for describing component requirements and
automated techniques for determining when finite-state
components meet their requirements. The key topics
under study include the following. A temporal logic for
open systems. We are working on a notation for
conveniently expressing properties constraining the
behavior of open systems. Implicit specifications.
Implicit specifications use system contexts, or ``test
harness,'' to define requirements for open systems. We
are studying expressiveness issues and model-checking
algorithms for such specifications. Automatic
model-checker generation. We have been developing a
model-checker generator that, given a temporal logic
and ``proof rules'' for the logic, automatically
produces an efficient model checker.",
acknowledgement = ack-nhfb,
fjournal = "ACM SIGSOFT Software Engineering Notes",
journal-URL = "https://dl.acm.org/citation.cfm?id=J728",
}