558 Result(s)
within
English
Electronics and Microelectronics, Instrumentation
Theory of Computation
**e **an
Chapter
-
Chapter
The Connectivity of Hypergraph and the Design of Fault Tolerant Multibus Systems
In recent years, multibuses have become widely used in different systems, yet their theoretical study is still immature. Most of the references are limited to particular aspects or case studies. There seems to...
-
Chapter
Four-Valued Logic and Its Applications
Four-valued logic is generalized from the traditional binary logic in order to describe the dynamic logical behavior of objective phenomena. We are going to study its mathematical features, especially the so-c...
-
Chapter
Testability Design via Testability Measures
Testability measures are used to describe the hardness (or easiness) of test generation for a logic circuit. In the analysis part we evaluate different definitions of testability from two requirements: precisi...
-
Chapter
Fault Tolerance of Switching Interconnection ß-Networks
Multicomputer systems are mainly affected by the interconnection networks through which the computers communicate with each other. The hierarchy of communication capabilities of the interconnection networks ar...
-
Chapter
TMR Design of Distributed System for Sequential Faults
In this chapter sequential faults occurring in a distributed system are mainly considered. A TMR system dynamically composed in the distributed system which can tolerant the largest number of sequential faults...
-
Chapter
Computer System Diagnosis and Society Diagnosis
A computer system consists of units (subsystems, computers, or at least processors) which have sufficient information processing capability to test the other units directly connected to them and get a test out...
-
Chapter
NMRC: A Technique for Redundancy
NMR (N Modular Redundancy) [1] is one of the most well known and most widely used fault-tolerant techniques. NMRC (N Modular Redundancy with Comparing) proposed here covers all the NMRs with respect to fault-t...
-
Chapter and Conference Paper
Protocol design for an automated highway system
-
Chapter and Conference Paper
Reachability analysis of planar multi-linear systems
In this paper we study the reachability analysis of a simple class of hybrid systems, namely multi-linear systems. Such systems consist of a partition of the Euclidean space into a finite set of polyhedral sets (
-
Chapter and Conference Paper
Timed modal specification — Theory and tools
In this paper we present the theory of Timed Modal Specifications (TMS) together with its implementation, the tool Epsilon. TMS and Epsilon are timed extensions of respectively Modal Specifications [7, 9] and the...
-
Chapter and Conference Paper
Verification of timing properties of VHDL
This paper shows how timing properties of VHDL processes can be verified using timed transition systems. The timing model being adopted is the timed automaton model used in the timing extension of Kurshan's CO...
-
Chapter and Conference Paper
Verification of real-time systems using PVS
We present an approach to the verification of the real-time behavior of concurrent programs and describe its mechanization using the PVS proof checker. Our approach to real-time behavior extends previous verif...
-
Chapter and Conference Paper
Computer-assisted simulation proofs
This paper presents a scalable approach to reasoning formally about distributed algorithms. It uses results about I/O automata to extract a set of proof obligations for showing that the behaviors of one algori...
-
Chapter and Conference Paper
Logic synthesis and design verification
-
Chapter and Conference Paper
Efficient verification of parallel real-time systems
This paper presents an efficient model checking algorithm for one-safe time Petri nets and a timed temporal logic. The approach is based on the idea of (1) using only differences of timing variables to be able...
-
Chapter and Conference Paper
Functionality decomposition by compositional correctness preserving transformation
In this paper we present an algorithm for the decomposition of processes in a process algebraic framework. Decomposition, or the refinement of process substructure, is an important design principle in the top-...
-
Chapter
Hybrid Inference Components for Monitoring of Artificial Respiration
Medical expert systems are developed for supporting the complicated decision finding processes of the physicians. Generally, the decision finding in a clinical therapeutic process contains a complex data fusio...
-
Chapter and Conference Paper
Parametric circuit representation using inductive Boolean functions
We have developed a methodology based on symbolic manipulation of inductive Boolean functions (IBFs) for formal verification of inductively-defined hardware. This methodology combines the techniques of reasoni...
-
Chapter and Conference Paper
Verifying quantitative real-time properties of synchronous programs
We propose to apply the verification techniques available for Timed Graphs [ACD90], and particularly the symbolic model-checking algorithm of [HNSY92], to the Argos [Mar92] synchronous language. We extend the ...
-
Chapter and Conference Paper
On-the-fly verification with stubborn sets
A new on-the-fly verification method is presented. The method uses a generalization of Büchi automata called “tester processes” for representing and detecting illegal behaviour. To reduce the number of states ...
