共查询到20条相似文献,搜索用时 576 毫秒
1.
LIN Huimin 《计算机科学技术学报》2000,15(1):1-9
Symbolic bisimulation avoids the infinite branching problem caused by instantiating input names with all names in the standard definition of bisimulation in π-calculus.However,it does not automatically lead to an efficient algorithm,because symbolic bisimulation is indexed by conditions on names,and directly manipulating such conditions can be computationally costly.In this paper a new notion of bisimulation is introduced,in which the manipulation of maximally consistent conditions is replaced with a systematic employment of schematic names.It is shown that the new notion captures symbolic bisimulation in a precise sense.Based on the new definition an efficient algorithm,which instantiates input names “on-the -fly“,is presented to check bisimulations for finite-control π-calculus. 相似文献
2.
Fu Yuxi 《计算机科学技术学报》1998,13(3):202-208
An alternative presentation of the π-calculus is given.This version of the π-calculus is symmetric in the sense that communications are symmetric and there is no difference between input and output prefixes.The point of the symmetric π-calculus is that it has no abstract names.The set of closed names is therefore homogeneous.The π-calculus can be fully embedded into the symmetric π-calculus.The symmetry changes the emphasis of the communication mechanism of the π-calculus and opens up possibility for further variations. 相似文献
3.
Davide Sangiorgi 《Acta Informatica》1996,33(1):69-97
We study a new formulation of bisimulation for the π-calculus [MPW92], which we have called open bisimulation (∼). In contrast with the previously known bisimilarity equivalences, ∼ is preserved by allπ-calculus operators, including input prefix. The differences among all these equivalences already appear in the sublanguage
without name restrictions: Here the definition of ∼ can be factorised into a “standard” part which, modulo the different syntax
of actions, is the CCS bisimulation, and a part specific to the π-calculus, which requires name instantiation. Attractive
features of ∼ are: A simple axiomatisation (of the finite terms), with a completeness proof which leads to the construction
of minimal canonical representatives for the equivalence classes of ∼; an “efficient” characterisation, based on a modified transition system. This characterisation
seems promising for the development of automated-verification tools and also shows the call-by-need flavour of ∼. Although
in the paper we stick to the π-calculus, the issues developed may be relevant to value-passing calculi in general.
Received: June 11, 1993/November 28, 1994 相似文献
4.
Expressing First-Order pi-Calculus in Higher-Order Calculus of Communicating Systems 总被引:1,自引:0,他引:1 下载免费PDF全文
Xian Xu 《计算机科学技术学报》2009,24(1):122-137
In the study of process calculi, encoding between different calculi is an effective way to compare the expressive power of calculi and can shed light on the essence of where the difference lies. Thomsen and Sangiorgi have worked on the higher-order calculi (higher-order Calculus of Communicating Systems (CCS) and higher-orderπ-calculus, respectively) and the encoding from and to first-orderπ-calculus. However a fully abstract encoding of first-orderπ-calculus with higher-order CCS is not available up-tod... 相似文献
5.
Theo C. Ruys Ed Brinksma 《International Journal on Software Tools for Technology Transfer (STTT)》2003,4(2):246-259
In this paper we take a closer look at the automated analysis of designs, in particular of verification by model checking.
Model checking tools are increasingly being used for the verification of real-life systems in an industrial context. In addition
to ongoing research aimed at curbing the complexity of dealing with the inherent state space explosion problem – which allows
us to apply these techniques to ever larger systems – attention must now also be paid to the methodology of model checking,
to decide how to use these techniques to their best advantage. Model checking “in the large” causes a substantial proliferation
of interrelated models and model checking sessions that must be carefully managed in order to control the overall verification
process. We show that in order to do this well both notational and tool support are required. We discuss the use of software
configuration management techniques and tools to manage and control the verification trajectory. We present Xspin/Project,
an extension to Xspin, which automatically controls and manages the validation trajectory when using the model checker Spin.
Published online: 18 June 2002 相似文献
6.
The coalgebraic framework developed for the classical process algebras, and in particular its advantages concerning minimal realizations, does not fully apply to the π-calculus, due to the constraints on the freshly generated names that appear in the bisimulation.In this paper we propose to model the transition system of the π-calculus as a coalgebra on a category of name permutation algebras and to define its abstract semantics as the final coalgebra of such a category. We show that permutations are sufficient to represent in an explicit way fresh name generation, thus allowing for the definition of minimal realizations.We also link the coalgebraic semantics with a slightly improved version of history dependent (HD) automata, a model developed for verification purposes, where states have local names and transitions are decorated with names and name relations. HD-automata associated with agents with a bounded number of threads in their derivatives are finite and can be actually minimized. We show that the bisimulation relation in the coalgebraic context corresponds to the minimal HD-automaton. 相似文献
7.
8.
Paolo Traverso Piergiorgio Bertoli 《International Journal on Software Tools for Technology Transfer (STTT)》2000,3(1):78-92
We present part of an industrial project where mechanized theorem proving is used for the validation of a translator which
generates safety critical software. In this project, the mechanized proof is decomposed in two parts: one is done “online”,
at each run of the translator, by a custom prover which checks automatically that the result of each translation meets some
verification conditions; the other is done “offline”, once for all, interactively with a general purpose prover; the offline
proof shows that the verification conditions checked by the online prover are sufficient to guarantee the correctness of each
translation. The provably correct verification conditions can thus be seen as specifications for the online prover. This approach
is called mechanized result verification. This paper describes the project requirements and explains the motivations to formal validation by mechanized result verification,
provides an overview of the formalization of the specifications for the online prover and discusses in detail some issues
we have addressed in the mechanized offline proof. 相似文献
9.
Marieke Huisman Bart Jacobs Joachim van den Berg 《International Journal on Software Tools for Technology Transfer (STTT)》2001,3(3):332-352
This paper presents a verification of an invariant property for the Vector class from JAVA’s standard library (API). The property
says (essentially) that the actual size of a vector is less than or equal to its capacity. It is shown that this “safety”
or “data integrity” property is maintained by all methods of the Vector class, and that it holds for all objects created by
the constructors of the Vector class. The verification of the Vector class invariant is done with the proof tool PVS. It is
based on a semantics of JAVA in higher order logic. The latter is incorporated in a special purpose compiler, the LOOP tool,
which translates JAVA classes into logical theories. It has been applied to the Vector class for this case study. The actual
verification takes into account the object-oriented character of JAVA: (non-final) methods may always be overridden, so that
one cannot rely on a particular implementation. Instead, one has to reason from method specifications in such cases. This
project demonstrates the feasibility of tool-assisted verification of non-trivial properties for non-trivial JAVA classes.
Published online: 10 May 2001 相似文献
10.
We consider concurrent probabilistic systems, based on probabilistic automata of Segala & Lynch [55], which allow non-deterministic
choice between probability distributions. These systems can be decomposed into a collection of “computation trees” which arise
by resolving the non-deterministic, but not probabilistic, choices. The presence of non-determinism means that certain liveness
properties cannot be established unless fairness is assumed. We introduce a probabilistic branching time logic PBTL, based on the logic TPCTL of Hansson [30] and the logic PCTL of [55], resp. pCTL [14]. The formulas of the logic express properties such as “every request is eventually granted with probability at least
p”. We give three interpretations for PBTL on concurrent probabilistic processes: the first is standard, while in the remaining two interpretations the branching time
quantifiers are taken to range over a certain kind of fair computation trees. We then present a model checking algorithm for
verifying whether a concurrent probabilistic process satisfies a PBTL formula assuming fairness constraints. We also propose adaptations of existing model checking algorithms for pCTL
[4, 14] to obtain procedures for PBTL
under fairness constraints. The techniques developed in this paper have applications in automatic verification of randomized
distributed systems.
Received: June 1997 / Accepted: May 1998 相似文献
11.
12.
Fady Copty Amitai Irron Osnat Weissberg Nathan Kropp Gila Kamhi 《International Journal on Software Tools for Technology Transfer (STTT)》2003,4(3):335-348
In this paper, we emphasize the importance of efficient debugging in formal verification and present capabilities that we
have developed in order to aid debugging in Intel’s Formal Verification Environment. We have given the name “Counter-Example
Wizard” to the bundle of capabilities that we have developed to address the needs of the verification engineer in the context
of counter-example diagnosis and rectification. The novel features of the Counter-Example Wizard are the multi-value counter-example annotation, constraint-based debugging, and multiple counter-example generation mechanisms. Our experience with the verification of real-life Intel designs shows that these capabilities complement one
another and can help the verification engineer diagnose and fix a reported failure. We use real-life verification cases to
illustrate how our system solution can significantly reduce the time spent in the loop of model checking, specification, and
design modification.
Published online: 21 February 2003 相似文献
13.
Personalized, interactive news on the Web 总被引:2,自引:0,他引:2
We present Krakatoa Chronicle, an interactive, personalized newspaper on the World Wide Web implemented as a Java applet. The newspaper is similar in appearance
to newspapers in the real world, with a multi-column layout and justified text. At the same time, it provides various interaction
techniques for browsing the content of articles, giving relevance feedback, and dynamically changing layout. As users interact
with the system, individual ‘user profiles’ are built up at the webserver site. These are used to tailor the newspaper's content
and layout to each user's declared and inferred preferences. The system allows for a balancing of personal and community interests,
allowing the user to navigate through a space of newspapers corresponding to a range of viewpoints. 相似文献
14.
David Gibson Jon Kleinberg Prabhakar Raghavan 《The VLDB Journal The International Journal on Very Large Data Bases》2000,8(3-4):222-236
We describe a novel approach for clustering collections of sets, and its application to the analysis and mining of categorical
data. By “categorical data,” we mean tables with fields that cannot be naturally ordered by a metric – e.g., the names of
producers of automobiles, or the names of products offered by a manufacturer. Our approach is based on an iterative method
for assigning and propagating weights on the categorical values in a table; this facilitates a type of similarity measure
arising from the co-occurrence of values in the dataset. Our techniques can be studied analytically in terms of certain types
of non-linear dynamical systems.
Received February 15, 1999 / Accepted August 15, 1999 相似文献
15.
16.
Speeding up construction of PMR quadtree-based spatial indexes 总被引:5,自引:0,他引:5
Gisli R. Hjaltason Hanan Samet 《The VLDB Journal The International Journal on Very Large Data Bases》2002,11(2):109-137
Spatial indexes, such as those based on the quadtree, are important in spatial databases for efficient execution of queries
involving spatial constraints, especially when the queries involve spatial joins. In this paper we present a number of techniques
for speeding up the construction of quadtree-based spatial indexes, specifically the PMR quadtree, which can index arbitrary
spatial data. We assume a quadtree implementation using the “linear quadtree”, a disk-resident representation that stores
objects contained in the leaf nodes of the quadtree in a linear index (e.g., a B-tree) ordered based on a space-filling curve.
We present two complementary techniques: an improved insertion algorithm and a bulk-loading method. The bulk-loading method
can be extended to handle bulk-insertions into an existing PMR quadtree. We make some analytical observations about the I/O
cost and CPU cost of our PMR quadtree bulk-loading algorithm, and conduct an extensive empirical study of the techniques presented
in the paper. Our techniques are found to yield significant speedup compared to traditional quadtree building methods, even
when the size of a main memory buffer is very small compared to the size of the resulting quadtrees.
Edited by R. Sacks-Davis. Received: July 10, 2001 / Accepted: March 25, 2002 Published online: September 25, 2002 相似文献
17.
Yonit Kesten Amir Pnueli 《International Journal on Software Tools for Technology Transfer (STTT)》2000,2(4):328-342
In spite of the impressive progress in the development of the two main methods for formal verification of reactive systems
– Symbolic Model Checking and Deductive Verification, they are still limited in their ability to handle large systems. It
is generally recognized that the only way these methods can ever scale up is by the extensive use of abstraction and modularization,
which break the task of verifying a large system into several smaller tasks of verifying simpler systems.
In this paper, we review the two main tools of compositionality and abstraction in the framework of linear temporal logic.
We illustrate the application of these two methods for the reduction of an infinite-state system into a finite-state system
that can then be verified using model checking.
The technical contributions contained in this paper are a full formulation of abstraction when applied to a system with both
weak and strong fairness requirements and to a general temporal formula, and a presentation of a compositional framework for
shared variables and its application for forming network invariants. 相似文献
18.
UnQL: a query language and algebra for semistructured data based on structural recursion 总被引:5,自引:0,他引:5
Peter Buneman Mary Fernandez Dan Suciu 《The VLDB Journal The International Journal on Very Large Data Bases》2000,9(1):76-110
Abstract. This paper presents structural recursion as the basis of the syntax and semantics of query languages for semistructured data
and XML. We describe a simple and powerful query language based on pattern matching and show that it can be expressed using
structural recursion, which is introduced as a top-down, recursive function, similar to the way XSL is defined on XML trees.
On cyclic data, structural recursion can be defined in two equivalent ways: as a recursive function which evaluates the data
top-down and remembers all its calls to avoid infinite loops, or as a bulk evaluation which processes the entire data in parallel
using only traditional relational algebra operators. The latter makes it possible for optimization techniques in relational
queries to be applied to structural recursion. We show that the composition of two structural recursion queries can be expressed
as a single such query, and this is used as the basis of an optimization method for mediator systems. Several other formal
properties are established: structural recursion can be expressed in first-order logic extended with transitive closure; its
data complexity is PTIME; and over relational data it is a conservative extension of the relational calculus. The underlying
data model is based on value equality, formally defined with bisimulation. Structural recursion is shown to be invariant with
respect to value equality.
Received: July 9, 1999 / Accepted: December 24, 1999 相似文献
19.
Xiaodong Wen Theodore D. Huffmire Helen H. Hu Adam Finkelstein 《Multimedia Systems》1999,7(5):350-358
We present several algorithms suitable for analysis of broadcast video. First, we show how wavelet analysis of frames of
video can be used to detect transitions between shots in a video stream, thereby dividing the stream into segments. Next we
describe how each segment can be inserted into a video database using an indexing scheme that involves a wavelet-based “signature.”
Finally, we show that during a subsequent broadcast of a similar or identical video clip, the segment can be found in the
database by quickly searching for the relevant signature. The method is robust against noise and typical variations in the
video stream, even global changes in brightness that can fool histogram-based techniques. In the paper, we compare experimentally
our shot transition mechanism to a color histogram implementation, and also evaluate the effectiveness of our database-searching
scheme. Our algorithms are very efficient and run in realtime on a desktop computer. We describe how this technology could
be employed to construct a “smart VCR” that was capable of alerting the viewer to the beginning of a specific program or identifying 相似文献
20.
Klaus Havelund Willem Visser 《International Journal on Software Tools for Technology Transfer (STTT)》2002,4(1):8-20
This paper introduces a special section of the STTT journal containing a selection of papers that were presented at the 7th
international SPIN workshop, Stanford, 30 August – 1 September 2000. The workshop was named SPIN Model Checking and Software
Verification, with an emphasis on model checking of programs. The paper outlines the motivation for stressing software verification,
rather than only design and model verification, by presenting the work done in the Automated Software Engineering group at
NASA Ames Research Center within the last 5 years. This includes work in software model checking, testing like technologies
and static analysis.
Published online: 2 October 2002 相似文献