共查询到20条相似文献,搜索用时 15 毫秒
1.
《Journal of Systems Architecture》2014,60(10):783-795
Complex systems on chip containing dozens of processing resources with critical communication requirements usually rely on the use of networks on chip (NoCs) as communication infrastructure. NoCs provide significant advantages over simpler infrastructures such as shared busses or point to point communication, including higher scalability, more efficient energy management, higher bandwidth and lower average latency. Applications running on NoCs with more than 10% of bandwidth usage attest that the most significant portion of message latencies refers to buffered packets waiting to enter the NoC, whereas the latency portion that depends on the packet traversing the NoC is sometimes negligible. This work presents an adaptive routing architecture, named Monitored NoC (MoNoC), which is based on a traffic monitoring mechanism and the exchange of high priority control packets. This method enables to adapt paths by choosing less congested routes. Practical experiments show that the proposed path adaptation is a fast process, enabling to transmit packets with smaller latencies, up to 9 times smaller, by using non-congested NoC regions. 相似文献
2.
The MSMIE protocol [SBC89] allows processors in a distributed system to communicate via shared memory. It was designed to meet the reliability and efficiency needs of applications such as nuclear safety systems. We present a formal model of the MSMIE protocol expressed in the notation CCS. Desirable properties of the protocol are expressed in the modal mu-calculus, an expressive modal logic. We show that the protocol lacks an important liveness property. In actual operation, additional operating constraints are checked to avoid potential problems. We present a modified protocol and show that it possesses the liveness property even without checking operating constraints. We also show how parts of the analysis were automated with the Concurrency Workbench. 相似文献
3.
4.
Stéphanie Delaune 《Information Processing Letters》2006,97(6):213-218
We present complexity results for the verification of security protocols. Since the perfect cryptography assumption is unrealistic for cryptographic primitives with visible algebraic properties, we extend the classical Dolev-Yao model by permitting the intruder to exploit these properties. More precisely, we are interested in theories such as Exclusive or and Abelian groups in combination with the homomorphism axiom. We show that the intruder deduction problem is in PTIME in both cases, improving the EXPTIME complexity results of Lafourcade, Lugiez and Treinen. 相似文献
5.
Fausto Giunchiglia Paolo Traverso 《International Journal on Software Tools for Technology Transfer (STTT)》2000,3(1):1-12
The aim of this paper is to discuss the potentials, problems and critical factors for the industrial usage of mechanized theorem
proving. The approach followed in this paper is somehow unusual. The starting point is the results of an industrial project
whose goal was the assessment of the state of the art of provers (and of tools supporting formal methods in general). We describe
the project results in terms of evaluation criteria, classification of technologies and tools and critical factors for industrial
take-up. We present the results of the assessment in the same spirit, the same kind of analysis and even the same terminology
which were used in the presentations and in the deliverables of the project. This should result in a presentation of a “different
view” of the problem of technology transfer in theorem proving, that we call the “user’s point of view”. In this way, we hope to give a new perspective in the discussion of the industrial take-up of the theorem proving technology. 相似文献
6.
Hantao Zhang 《Journal of Automated Reasoning》1993,11(3):333-351
This paper reports the detailed computer proofs of nine equality problems in Overbeek's competition obtained by Herky, a completion-based theorem prover developed by the author. Advanced techniques implemented in Herky made it a high-performance theorem prover for equational reasoning. Herky is able to prove the first nine of the ten equality problems in the competition (the tenth is an open problem). These equality problems are likely to serve as good exercises for theorem provers based on different approaches, and the proofs of these problems may help people to solve them using their own theorem provers. 相似文献
7.
LarsÅke Fredlund Dilian Gurov Thomas Noll Mads Dam Thomas Arts Gennady Chugunov 《International Journal on Software Tools for Technology Transfer (STTT)》2003,4(4):405-420
This paper presents an overview of the main results of the project Verification of ERLANG Programs , which is funded by the Swedish Business Development Agency (NUTEK) and by Ericsson within the ASTEC (Advanced Software TEChnology) initiative. Its main outcome is the ERLANG Verification Tool (EVT), a theorem prover which assists in obtaining proofs that ERLANG applications satisfy their correctness requirements formulated as behavioural properties in a modal logic with recursion. We give a summary of the verification framework as supported by EVT, discuss reasoning principles essential for successful proofs such as inductive and compositional reasoning, and an efficient treatment of side-effect-free code. The experiences of applying the tool in an industrial case study are summarised, and an approach for supporting verification in the presence of program libraries is outlined.EVT is essentially a classical proof assistant, or theorem-proving tool, requiring users to intervene in the proof process at crucial steps such as stating program invariants. However, the tool offers considerable support for automatic proof discovery through higher-level tactics tailored to the particular task of the verification of ERLANG programs. In addition, a graphical interface permits easy navigation through proof tableaux, proof reuse, and meaningful feedback about the current proof state, to assist users in taking informed proof decisions. 相似文献
8.
9.
Mark E. Stickel 《Journal of Automated Reasoning》1988,4(4):353-380
A Prolog technology theorem prover (PTTP) is an extension of Prolog that is complete for the full first-order predicate calculus. It differs from Prolog in its use of unification with the occurs check for soundness, the model-elimination reduction rule that is added to Prolog inferences to make the inference system complete, and depth-first iterative-deepening search instead of unbounded depthfirst search to make the search strategy complete. A Prolog technology theorem prover has been implemented by an extended Prolog-to-LISP compiler that supports these additional features. It is capable of proving theorems in the full first-order predicate calculus at a rate of thousands of inferences per second.This is a revised and expanded version of a paper presented at the 8th International Conference on Automated Deduction, Oxford, England, July 1986.This research was supported by the Defense Advanced Research Projects Agency under Contract N00039-84-K-0078 with the Naval Electronic Systems Command and by the National Science Foundation under Grant CCR-8611116. The views and conclusions contained herein are those of the author and should not be interpreted as necessarily representing the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency, the National Science Foundation, or the United States government. Approved for public release. Distribution unlimited. 相似文献
10.
The condensed detachment ruleD is a combination of modus ponens with a minimal amount of substitution. EarlierD has been shown to be complete for intuitionistic and classical implicational logic but incomplete forBCK andBCI logic. We show thatD is complete for the relevance logic. One of the main steps is the proof of the formula ((a a) a) a found in interaction with our resolution theorem prover. Various strategies of generating consequences of the axioms and choosing best ones for the next iteration were tried until the proof was found. 相似文献
11.
An investigation is made into the ways proof planning can enhance the capability of a rule based prover for the theory of integration. The integrals are of the Riemann type and are defined in a way to maximize the theorem proving methods of predicate calculus. Approximately fifty theorems have been proved and several examples are discussed. A major shortcoming was found to be the inability of the system to work with or produce a proof plan. As a result, a planning scheme based on the idea of subgoals or milestones was considered. With user defined plans, there was a substantial increase in performance and capability of the system and, in some cases, proofs which were previously unsuccessful were completed. 相似文献
12.
Klaus Heje Munch 《Journal of Automated Reasoning》1988,4(4):425-444
A new reduction rule is introduced for the connection graph proof procedure proposed by Kowalski in 1975. The new rule considers sets of values which clause variables may take. Application of the rule often leads to massive removals of links. A proof system in which the new rule is included has successfully been implemented in PROLOG. The performance of this system is compared to other resolution based proof systems. Also, the new rule is related to order-sorted logic. 相似文献
13.
Florian Kammüller 《Formal Aspects of Computing》2008,20(3):259-275
In this paper, we describe the application of the interactive theorem prover Coq to the security analysis of bytecode as used
in Java. We provide a generic specification and proof of non-interference for bytecode languages using the Coq module system.
We illustrate the use of this formalization by applying it to a small subset of Java bytecode. The emphasis of the paper is
on modularity of a language formalization and its analysis in a machine proof.
C. B. Jones 相似文献
14.
Productive use of failure in inductive proof 总被引:2,自引:0,他引:2
Proof by mathematical induction gives rise to various kinds of eureka steps, e.g., missing lemmata and generalization. Most
inductive theorem provers rely upon user intervention in supplying the required eureka steps. In contrast, we present a novel
theorem-proving architecture for supporting the automatic discovery of eureka steps. We build upon rippling, a search control heuristic designed for inductive reasoning. We show how the failure if rippling can be used in bridging
gaps in the search for inductive proofs.
The research reported in this paper was supported by EPSRC grant GR/J/80702 and ARC grant 438. 相似文献
15.
W. Bibel 《Journal of Automated Reasoning》1990,6(3):287-297
Quadratic proofs of pigeonhole formulas are presented using connection method proof techniques. The interest of this result derives from the fact that for this class of formulas exponential lower bounds are known for the length of resolution refutations. 相似文献
16.
Commercial designs are currently integrating from 10 to 100 embedded processors in a single system on chip (SoC) and the number is likely to increase significantly in the near future. With this ever increasing degree of integration, design of communication architectures for large, multi-core SoCs is a challenge. Traditional bus-based systems will no longer be able to meet the clock cycle requirements of these big SoCs. Instead, the communication requirements of these large multi processor SoCs (MP-SoCs) are convened by the emerging network-on-chip (NoC) paradigm. Crosstalk between adjacent wires is an important signal integrity issue in NoC communication fabrics and it can cause timing violations and extra energy dissipation. Crosstalk avoidance codes (CACs) can be used to improve the signal integrity by reducing the effective coupling capacitance, lowering the energy dissipation of wire segments. As NoCs are built on packet-switching, it is advantageous to modify data packets by including coded bits to protect against the negative effects of crosstalk. By incorporating crosstalk avoidance coding in NoC data streams and organizing the CAC-encoded data packets in an efficient manner, so that total number of encoding/decoding operations can be reduced over the communication channel, we are able to achieve lower communication energy, which in turn will help to decrease the overall energy dissipation. 相似文献
17.
We report on mechanization of a correctness proof of a string-preprocessing algorithm. This preprocessing algorithm is employed
in Boyer-Moore’s pattern matching algorithm. The mechanization is carried out using the PVS system. The correctness proof
being mechanized has been formulated in Linear Time Temporal Logic. It consists of fourteen lemmata which are related to safety
properties and two additional lemmata dealing with liveness properties. The entire mechanization of the safety and liveness
parts has been completed. Several small errors and omissions were found in the handwritten proof and corrected. Yet, the manual
correctness proof of the string-preprocessing algorithm was found to satisfy the usual mathematical validity. We conclude
that the string-preprocessing algorithm in Boyer-Moore’s pattern matching algorithm, corrected a number of times because of
flaws, does not contain any more undiscovered errors.
An extended abstract of this work appears in the Proceedings of the 8th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS ‘02). 相似文献
18.
19.
20.
Skolemization is not an equivalence preserving transformation. For the purposes of refutational theorem proving it is sufficient that skolemization preserves satisfiability and unsatisfiability. Therefore there is sometimes some freedom in interpreting Skolem functions in a particular way. We show that in certain cases it is possible to exploit this freedom for simplifying formulae considerably. Examples for cases where this occurs systematically are the relational translation from modal logics to predicate logic and the relativization of first-order logics with sorts. 相似文献