/ V. B. Marakhovsky / Professor
/ Zi Xue Cheng / Assistant Professor
/ Kshirasagar Naik / Assistant Professor
Computer Networks Laboratory is working in two directions within Group Research Development Projects:
1) ``Self-timing and Event-driven Systems";
2) ``Conformance Testing, Open Distributed Processing, and Quality of Service to Support Multimedia Communications".
1. In 1993, work on the first project was as follows:
1.1 Developing Self-timed circuit Design method: High level logic design is an art and good results can be obtained only in man-computer synthesis. An experienced designer usually has a notion about the device structure and successfully applies it in the specification design. We have developed the man-machine method of self-timed device synthesis based on ``master-slave" gate structure implementation of finite automata.
1.2 Self-timing Application in Fault-tolerant Systems: Self-timed circuits can be the basis to implement a fault-tolerant system interface since such circuits are fully self-checked with respect to stuck-at faults and are notable for relatively simple organization of self-repairing. The problems of fault tolerant self-timed communication channel design for the control of a multicomputer system with local area network architecture and their decisions has been reported in two Japanese conferences.
1.3 Global Synchronization of Asynchronous Arrays: One of the ways to overcome the synchronization problem of Wave Propagation and Systolic Arrays is the transition to asynchronous pipelined interaction between the array processors. However, in using this approach, arbitration situations can appear that reduces the reliability. The new general solution of the asynchronous array global synchronization problem has been suggested. The solution is based on the array dividing into two strata - synchronizing self-timed pipelined stratum, where a system of divergent synchrowaves is generated, and processor array synchronized by these synchrowaves.
1.4 Self-timed Systems with Current Sensors: In CMOS-circuits, the current flows only during transient processes. Therefore, usual (synchronous) circuits with current sensors can be used to construct self-timed CMOS devices. We suggested the idea of current shunt that transforms pulse reaction of a current sensor to potential form that gives an opportunity to design delay-insensitive circuits. Several variants of asynchronous interfaces with current indication possessed the minimal redundancy and the maximal throughput, have been developed.
2. In 1993, work on the second project was as follows:
2.1 Verification of Timed Properties of Test Cases: In order to test timed behavior of communication protocols, test suites contain many time-related test cases. We investigated a methodology to specify the timed properties of test cases and verify them using a model checking approach.
2.2 Design of Reliable Test Architecture: Because of the real-time and reactive nature of communication protocols, testing their implementations is a difficult task. We designed a reliable architecture that eliminates the occurrence of spurious events and allows a test case to dynamically compute timeout values.
2.3 Design of Multimedia Synchronizers: Synchronization of different media streams in a multimedia application is essential for capturing the meaning of the application. There is a need to specify synchronization requirements at the presentation level, verify such requirements, and obtain implementations from them. Our work focused on the hardware implementation of synchronizers.
2.4 Protocol Implementation: One FDT called LOTOS is developed by ISO for specification of computer network protocols. System specifications written in LOTOS are complete, consistent, concise, unambiguous and precise in a very abstract level, because LOTOS is based on the process algebra and provides a powerful communication mechanism called Multi-Rendezvous. However, because of the high level abstraction, it is very difficult to implement the specification in a real system. In order to implement a LOTOS specification on a real system, we worked on the following problems in the last year:
Refereed Journal Papers
Verification of test case for testing the conformance of protocol implementations against the formal description of the protocol involves verifying three aspects of the test case: expected input-output test behavior, test verdicts, and the test purpose. We model the safety and liveness properties of a test case using branching time temporal logic. There are four types of safety properties: transmission safety, reception safety, synchronization safety, and verdict safety. We model a test purpose as a liveness property and give a set of notations to formally specify a test purpose. All these properties expressed as temporal formulas are verified using model checking on an extended state machine graph representing the composed behavior of a test case and protocol specification. This methodology is shown to be effective in finding errors in manually developed conformance test suites.
A procedure of designing a self-timed device defined by the model of finite automaton is suggested. In accordance with the chosen automaton standard implementation structure from the automaton transition/output graph one derives the Signal Graph Specification that then is processed by the formal synthesis procedure for self-timed implementation. The design procedure is illustrated by two examples: Stack Memory and Counter with Constant Acknowledge Delay.
Refereed Proceeding Papers
In this paper we synthesize the detailed behavior of a synchronizer for multimedia applications. A protocol architecture is presented to separate synchronization concerns from communication issues. Application-level sync. requirements (ASR) are built by combining high-level timing primitives and analyzed to detect any inconsistency. The behavior of a synchronizer is modeled as a system of concurrent timed automata. An algorithm is given to transform an ASR into a system of timed automata representing the detailed behavior of the synchronizer. The timed automata model will lead to easy implementation of synchronizers.
We develop a methodology to verify the correctness of test cases designed to check timed behavior of protocol implementations. The verification process consists of four steps. First, we model a protocol specification, a test case, and an underlying service provider as Timed Extended Finite-State Machines (TEFSM) and define the resulting system as a Test Verification System (TVS). Next, we algorithmically obtain a model, i.e., a predicated global state space, from the TVS. Test case properties are formulated in terms of safety and liveness using branching time temporal logic. Finally we verify the test case properties on the model of the TVS using a model checking algorithm. We apply the verification technique to a test case for the Inres protocol. A few errors are detected in the design of the test case. We observe that without the use of TEFSM model, it would not have been possible to detect any time related errors in the test case.
There are two contributions of this paper. First, we introduce the notion of a time-server protocol in a test architecture to dynamically estimate the round-trip network delay in the service provider. The generalization capability of neural networks is used as the central idea in the dynamic estimation of round-trip delays from actual measurement of delays in the past. Second, we define the notion of architecture reliability and the properties a reliable architecture must satisfy. The notion of a filter protocol is introduced to obtain reliability in a test architecture. Finally, we combine the time-server and filter protocols with a basic architecture to obtain a reliable test architecture.
Technical Reports
Academic Activities
Invited presentation in Ibaraki Workshop on Self-Timing.
Invited presentation in Aizu Workshop on Fault-Tolerance.