共查询到20条相似文献,搜索用时 15 毫秒
1.
Steven D. Johnson Yanhong A. Liu Yuchen Zhang 《International Journal on Software Tools for Technology Transfer (STTT)》2003,4(2):211-223
A systematic transformation method based on incrementalization and value caching generalizes a broad family of program optimizations. It yields significant performance improvements in many program classes,
including iterative schemes that characterize hardware specifications. CACHET is an interactive incrementalization tool. Although incrementalization is highly structured and automatable, better results
are obtained through interaction, where the main task is to guide term rewriting based on data-specific identities. Incrementalization
specialized to iteration corresponds to strength reduction, a familiar program improvement technique. This correspondence is illustrated by the derivation of a hardware-efficient nonrestoring square-root algorithm, which has also served as an example of theorem prover-based implementation verification.
Published online: 9 October 2001
RID="*"
ID="*"S.D. Johnson supported, in part, by the National Science Foundation under grant MIP-9601358.
RID="**"
ID="**"Y.A. Liu supported in part by the National Science Foundation under grant CCR-9711253, the Office of Naval Research
under grant N00014-99-1-0132, and Motorola Inc. under a Motorola University Partnership in Research Grant.
RID="***"
ID="***"Y. Zhang is a student recipient of a Motorola University Partnership in Research Grant. 相似文献
2.
Louise A. Dennis Graham Collins Michael Norrish Richard J. Boulton Konrad Slind Thomas F. Melham 《International Journal on Software Tools for Technology Transfer (STTT)》2003,4(2):189-210
The PROSPER (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing
verification tools to be adapted to a more flexible format so that they can be treated as components. A system incorporating
such tools becomes another component that can be embedded in an application. This paper describes the software toolkit developed
by the project. The nature of communication between components is specified in a language-independent way. It is implemented
in several common programming languages to allow a wide variety of tools to have access to the toolkit.
Published online: 19 November 2002
Work funded by ESPRIT Framework IV Grant LTR 26241.
RID="*"
ID="*"Michael Norrish is supported by the Michael and Morven Heller Research Fellowship at St. Catharine’s College, Cambridge.
RID="**"
ID="**"Konrad Slind is now at the School of Computing, University of Utah, Salt Lake City UT 84112, USA. 相似文献
3.
E.E. Roubtsova L.C.M. van Gool R. Kuiper H.B.M. Jonkers 《Software and Systems Modeling》2002,1(2):98-112
The paper motivates and describes a model oriented approach for consistent specification of interface suites in UML. An interface
suite is a coherent collection of interfaces defining interactions that transcend component boundaries. The specification
of interface suites contains diagrammatic views and documentation, but it is extended with templates for structured specifications
deriving from the ISpec approach. To guarantee that the specification views, documentation and templates are consistent, a
specification model has been constructed. The model contains both structural and behavioural information, represented in the
form of sequences of carefully designed tuples. The model provides the underlying structure for the tool supporting the design
process. The tool directs the designer to specify all elements of the model in a consistent way. The specification is collected
both by customized specification templates and by diagrams. The documentation and the diagram elements – both derived from
the template information – are automatically generated. This prevents errors and provides specification consistency.
Initial submission: 15 February 2002 / Revised submission: 20 September 2002 Published online: 2 December 2002
RID="*"
ID="*"Supported by PROGRESS grant EES.5141 and ITEA DESS grant IT990211. 相似文献
4.
The dominating set problem asks for a small subset D of nodes in a graph such that every node is either in D or adjacent to a node in D. This problem arises in a number of distributed network applications, where it is important to locate a small number of centers
in the network such that every node is nearby at least one center. Finding a dominating set of minimum size is NP-complete,
and the best known approximation is logarithmic in the maximum degree of the graph and is provided by the same simple greedy
approach that gives the well-known logarithmic approximation result for the closely related set cover problem. We describe
and analyze new randomized distributed algorithms for the dominating set problem that run in polylogarithmic time, independent
of the diameter of the network, and that return a dominating set of size within a logarithmic factor from optimal, with high
probability. In particular, our best algorithm runs in rounds with high probability, where n is the number of nodes, is one plus the maximum degree of any node, and each round involves a constant number of message exchanges among any two
neighbors; the size of the dominating set obtained is within of the optimal in expectation and within of the optimal with high probability. We also describe generalizations to the weighted case and the case of multiple covering
requirements.
Received: January 2002 / Accepted: August 2002
RID="*"
ID="*" Supported by NSF CAREER award NSF CCR-9983901
RID="*"
ID="*" Supported by NSF CAREER award NSF CCR-9983901 相似文献
5.
The concept of multiplicity in UML derives from that of cardinality in entity-relationship modeling techniques. The UML documentation
defines this concept but at the same time acknowledges some lack of obviousness in the specification of multiplicities for
n-ary associations. This paper shows an ambiguity in the definition given by UML documentation and proposes a clarification
to this definition, as well as the use of outer and inner multiplicities as a simple extension to the current notation to
represent other multiplicity constraints, such as participation constraints, that are equally valuable in understanding n-ary
associations.
Initial submission: 16 January 2002 / Revised submission: 17 October 2002
Published online: 2 December 2002
RID="*"
ID="*"A previous shorter version of this paper was presented under the title “Semantics of the Minimum Multiplicity in Ternary
Associations in UML” at The 4th International Conference on the Unified Modeling Language-UML’2001, October 1–5 2001, Toronto,
Ontario, Canada, Springer Verlag, LNCS 2185, pp. 329–341. 相似文献
6.
Underflow is a floating-point phenomenon. Although the use of gradual underflow as defended in [2] and [3] is now widespread,
most numerical analysts may not be aware of the fact that several implementations of the same principle are in existence,
leading to different behavior of code on different platforms, mainly with respect to exception signaling. We intend to thoroughly
discuss the slight differences among these implementations. Examples will be taken from current hardware and from our own
multiprecision software class library. Throughout the discussion the focus is on the analysis of the phenomenon and not on
any implementation issues. Many programmers are also unaware of the fact that the IEEE 754 and 854 standards do not guarantee
that a program will deliver identical results on all conforming systems. Of all the differences that can occur cross-platform,
the underflow exception is just one.
Received: January 2002 / Accepted: June 2002
RID="*"
ID="*"Research Director, FWO-Vlaanderen
RID="**"
ID="**"Supported by an NOI-grant from the Universiteit Antwerpen (UIA)
RID="***"
ID="***"Postdoctoral Fellow, FWO-Vlaanderen
RID="****"
ID="****"Research Fellow, IWT (Institute for Science and Technology) 相似文献
7.
Relevance feedback in image retrieval: A comprehensive review 总被引:23,自引:1,他引:22
We analyze the nature of the relevance feedback problem in a continuous representation space in the context of content-based
image retrieval. Emphasis is put on exploring the uniqueness of the problem and comparing the assumptions, implementations,
and merits of various solutions in the literature. An attempt is made to compile a list of critical issues to consider when
designing a relevance feedback algorithm. With a comprehensive review as the main portion, this paper also offers some novel
solutions and perspectives throughout the discussion.
RID="*"
ID="*" Work was done while at the University of Illinois. 相似文献
8.
Symmetric Spin 总被引:1,自引:0,他引:1
Dragan Bošnački Dennis Dams Leszek Holenderski 《International Journal on Software Tools for Technology Transfer (STTT)》2002,4(1):92-106
9.
Monika Kapus-Kolar 《Distributed Computing》1999,12(4):175-177
Summary. An algorithm by Kant, Higashino and Bochmann for service-based protocol synthesis in the standard specification language
LOTOS is discussed. It is demonstrated that the transformations for distributed implementation of synchronised parallel execution
and of disabling are not correct in a general case.
Received: January 1998 / Accepted: January 1999 相似文献
10.
Handling a tertiary storage device, such as an optical disk library, in the framework of a disk-based stream service model,
requires a sophisticated streaming model for the server, and it should consider the device-specific performance characteristics
of tertiary storage. This paper discusses the design and implementation of a video server which uses tertiary storage as a
source of media archiving. We have carefully designed the streaming mechanism for a server whose key functionalities include
stream scheduling, disk caching and admission control. The stream scheduling model incorporates the tertiary media staging
into a disk-based scheduling process, and also enhances the utilization of tertiary device bandwidth. The disk caching mechanism
manages the limited capacity of the hard disk efficiently to guarantee the availability of media segments on the hard disk.
The admission controller provides an adequate mechanism which decides upon the admission of a new request based on the current
resource availability of the server. The proposed system has been implemented on a general-purpose operating system and it
is fully operational. The design principles of the server are validated with real experiments, and the performance characteristics
are analyzed. The results guide us on how servers with tertiary storage should be deployed effectively in a real environment.
RID="*"
ID="*" e-mail: hjcha@cs.yonsei.ac.kr 相似文献
11.
M. Janžura 《Soft Computing - A Fusion of Foundations, Methodologies and Applications》2003,7(5):321-327
The knowledge representation problem is understood as finding a reasonable joint distribution for a collection of marginal
distributions. The problem is reformulated as a “moment problem”, and the solution is searched in the exponential form. Further,
an equivalent parametrization is introduced with a parameter which can be easily identified even in higher dimensional cases.
The problem of evaluating relevant model characteristics is discussed.
RID="*"
ID="*" Supported by grant GA ČR 102/99/1137. 相似文献
12.
Yehuda Afek Anat Bremler-Barr Haim Kaplan Edith Cohen Michael Merritt 《Distributed Computing》2002,15(4):273-283
A new general theory about restoration of network paths is first introduced. The theory pertains to restoration of shortest paths in a network following failure,
e.g., we prove that a shortest path in a network after removing k edges is the concatenation of at most k+1 shortest paths in the original network. The theory is then combined with efficient path concatenation techniques in MPLS
(multi-protocol label switching), to achieve powerful schemes for restoration in MPLS based networks. We thus transform MPLS
into a flexible and robust method for forwarding packets in a network. Finally, the different schemes suggested are evaluated
experimentally on three large networks (a large ISP, the AS graph of the Internet, and the full Internet topology). These
experiments demonstrate that the restoration schemes perform well in actual topologies.
Received: December 2001 / Accepted: July 2002
RID="*"
ID="*" This research was supported by a grant from the Ministry of Science, Israel 相似文献
13.
We establish a lower bound of remote memory references for N-process mutual exclusion algorithms based on reads, writes, or comparison primitives such as test-and-set and compare-and-swap. Our bound improves an earlier lower bound of established by Cypher. Our lower bound is of importance for two reasons. First, it almost matches the time complexity of the best known algorithms based on reads, writes, or comparison primitives. Second, our lower bound suggests
that it is likely that, from an asymptotic standpoint, comparison primitives are no better than reads and writes when implementing
local-spin mutual exclusion algorithms. Thus, comparison primitives may not be the best choice to provide in hardware if one
is interested in scalable synchronization.
Received: January 2002 / Accepted: September 2002
RID="*"
ID="*" Work supported by NSF grants CCR 9732916, CCR 9972211, CCR 9988327, ITR 0082866, and CCR 0208289. 相似文献
14.
Moataz Kamel Stefan Leue 《International Journal on Software Tools for Technology Transfer (STTT)》2000,2(4):394-409
The General Inter-Orb Protocol (GIOP) is a key component of the Common Object Request Broker Architecture (CORBA) specification.
We present the formal modeling and validation of the GIOP protocol using the Promela language, Linear Time Temporal Logic
(LTL) and the Spin model checker. We validate the Promela model using ten high-level requirements which we elicit from the
informal CORBA specification. These requirements are then formalized in LTL and the Spin model checker is used to determine
their validity. During the validation process we discovered a few problems in GIOP: a potential transport-layer interface
deadlock and problems with the server migration protocol. We also describe how property specification patterns helped us in
formalizing the high-level requirements that we have elicited. 相似文献
15.
Abstract. This paper describes the design of a reconfigurable architecture for implementing image processing algorithms. This architecture
is a pipeline of small identical processing elements that contain a programmable logic device (FPGA) and double port memories.
This processing system has been adapted to accelerate the computation of differential algorithms. The log-polar vision selectively
reduces the amount of data to be processed and simplifies several vision algorithms, making possible their implementation
using few hardware resources. The reconfigurable architecture design has been devoted to implementation, and has been employed
in an autonomous platform, which has power consumption, size and weight restrictions. Two different vision algorithms have
been implemented in the reconfigurable pipeline, for which some experimental results are shown.
Received: 30 March 2001 / Accepted: 11 February 2002
RID="*"
ID="*" This work has been supported by the Ministerio de Ciencia y Tecnología and FEDER under project TIC2001-3546
Correspondence to: J.A. Boluda 相似文献
16.
Scott D. Stoller 《International Journal on Software Tools for Technology Transfer (STTT)》2002,4(1):71-91
State-space exploration is a powerful technique for verification of concurrent software systems. Applying it to software systems
written in standard programming languages requires powerful abstractions (of data) and reductions (of atomicity), which focus
on simplifying the data and control, respectively, by aggregation. We propose a reduction that exploits a common pattern of
synchronization, namely, the use of locks to protect shared data structures. This pattern of synchronization is particularly
common in concurrent Java programs, because Java provides built-in locks. We describe the design of a new tool for state-less
state-space exploration of Java programs that incorporates this reduction. We also describe an implementation of the reduction
in Java PathFinder, a more traditional state-space exploration tool for Java programs.
Published online: 2 October 2002
RID="*"
ID="*"Present address: Computer Science Dept., SUNY at Stony Brook, Stony Brook, NY 11794-4400, USA. The author gratefully
acknowledges the support of ONR under Grants N00014-99-1-0358 and N00014-01-1-0109 and the support of NSF under Grant CCR-9876058. 相似文献
17.
Cynthia E. Irvine Timothy Levin Jeffery D. Wilson David Shifflett Barbara Pereira 《Requirements Engineering》2002,7(4):192-206
Requirements specifications for high-assurance secure systems are rare in the open literature. This paper examines the development
of a requirements document for a multilevel secure system that must meet stringent assurance and evaluation requirements.
The system is designed to be secure, yet combines popular commercial components with specialised high-assurance ones. Functional
and non-functional requirements pertinent to security are discussed. A multidimensional threat model is presented. The threat
model accounts for the developmental and operational phases of system evolution and for each phase accounts for both physical
and non-physical threats. We describe our team-based method for developing a requirements document and relate that process
to techniques in requirements engineering. The system requirements document presented provides a calibration point for future
security requirements engineering techniques intended to meet both functional and assurance goals.
RID="*"
ID="*"The views expressed in this paper are those of the authors and should not be construed to reflect those of their employers
or the Department of Defense. This work was supported in part by the MSHN project of the DARPA/ITO Quorum programme and by
the MYSEA project of the DARPA/ATO CHATS programme.
Correspondence and offprint requests to: T. Levin, Department of Computer Science, Naval Postgraduate School, Monterey, CA 93943-5118, USA. Tel.: +1 831 656 2339;
Fax: +1 831 656 2814; Email: levin@nps.navy.mil 相似文献
18.
Constructing communication protocols from component service specifications, each of which specifies a subfunction of the target protocol, enables efficient development of a large and complex communication protocol. Concerning this construction, related techniques have been already proposed: integration of component protocol specifications into a single protocol specification and transformation of service specifications to protocol specifications. However, the integration needs special knowledge of communication protocols, and the transformation requires that a large and complex service specification should be developed as input to produce the target protocol. In order to cope with these problems, this paper proposes a new method which at first integrates component service specifications into a single service specification, and then transforms the service specification into the target protocol by a protocol synthesis technique. The most important point of view is that component integration is performed at the service specification level rather than the protocol specification level. Additionally, we define a class of ‘well-formed’ service specification which ensures correctness of the target protocol. As a result, the integration and transformation can be efficiently executed in small state space without special knowledge of communication protocols. Finally, we have shown the effectiveness of the proposed method by constructing a part of the real-life OSI protocol FTAM. 相似文献
19.
The success of the Object Management Group's General Inter-ORB Protocol (GIOP) is leading to the desire to deploy GIOP in
an ever-wider range of application areas, many of which are significantly more demanding than traditional areas in terms of
performance. The well-known performance limitations of present day GIOP-based object request brokers (ORBs) are therefore
increasingly being seen as a problem. To help address this problem, this paper discusses a GIOP implementation which has high
performance and quality of service support as explicit goals. The implementation, which is embedded in a research ORB called
Gopi, is modular and extensible in nature and includes novel optimization techniques which should be separately portable to other
ORB environments. This paper focuses on the message protocol aspects of Gopi's GIOP implementation; higher layer issues such as marshalling and operation demultiplexing are not covered in detail. Figures
are provided which position Gopi's GIOP performance against comparable ORBs. The paper also discusses some of the design decisions that have been made in
the development of the GIOP protocol in the light of our implementation experience.
Received: May 2000 / Accepted: December 2000 相似文献
20.
We introduce an alternative definition of random graphs as a language generated by a stochastic cooperating distributed grammar
system. We show a relationship between our definition and four known definitions of random graphs, an example of using our
model to prove graph-theoretic properties, and we define k-probabilistic model of random graphs as an extension. The first important acquisition of our definition is that only a small
modification of a stochastic cooperating distributed grammar system may effect the substantial change of the generated random
graph model. Other important result resides in the fact that our approach enables the use of a new proving technique in the
random graph theory which is based on the generative paradigm inherent in the formal languages theory.
Received: 14 May 2002 / 30 October 2002
RID="*"
ID="*" Supported by the VEGA grant No. 1/7152/20. 相似文献