SAL is a toolkit for analyzing transition systems, providing several different tools. Among the tools are a BDD-based symbolic model checker (SMC) and an SMT-based infinite bounded model checker (infBMC). The unique functionality provided by SAL is k-induction, which is supported by infBMC. Given appropriate lemmas, infBMC can prove automatically by k-induction that an infinite-state transition system satisfies invariant properties. Maude is a specification language and system based on membership equational logic and rewriting logic. Maude is equipped with an on-the-fly explicit state model checker. The unique functionality provided by the Maude model checker supports inductive data types. We make a comparison of SAL (especially SMC and infBMC) and the Maude model checker by conducting case studies in which the Suzuki-Kasami distributed mutual exclusion algorithm is analyzed. The purpose of the comparison is to clarify some of the two tools' functionalities, especially the unique ones, through the case studies.

Shared buffer ATM switches have been attractive since they can achieve a superior performance in terms of cell loss ratio and throughput with a relatively small buffer size. Shared multi-buffer structures have also been considered by several researchers to enhance the access speed of the cell memory for a large switch. High quality services, however, cannot be provided without reliable operation at each module comprising the ATM switches. In this paper, we present a novel on-line error monitoring technique for shared-buffer ATM switches. The technique detects almost all of the functional errors that could occur in the ATM switches. Moreover, it can detect errors with small hardware overhead and negligible time overhead. An early detection of functional errors in ATM switches could not only reduce the wasted bandwidth due to the transmission of erroneous cells, but greatly enhance the recovery time.

Checkers, self-testers, and self-correctors for a function f are powerful tools in designing programs that compute f. However, the relationships among them have not been known well. In this paper, we first show that (1) if oneway permutations exist, then there exists a language L that has a checker but does not have a self-corrector. We then introduce a novel notion of "self-improvers" that trans form a faulty program into a less faulty program, and show that (2) if a function f has a self-tester/corrector pair, then f has a self-improver. As the applications of self-improvers, we finally show that (3) if a function f has a self-tester/corrector pair, then f has a flexible self-tester and (4) if a function f has a self-tester/corrector pair, then f has self-improver that transforms a faulty program into an alomost correct program.

Let L{0,1}* be a language and let λL : {0,1}*{0,1} be the characteristic function of the language L, i.e., if x ∈ L, λL (x) = 1; otherwise,λL (x) = 0. In this paper, we consider an adaptive checker with a single program F (resp. noncommunicating multiple programs F1, F2,...) for λL that works even when an incorrect program F* (resp. incorrect noncommunicating multiple programs F*1,F*2,...) for λL adaptively behaves according to inputs previously provided to the program F* (resp. the programs F*1,F*2,...). We show that (1) for any language L, there exists an adaptive checker with a single program for λL iff L and respectively have competitive interactive proof systems; and (2) that for any language L, there exists an adaptive checker with noncommunicating multiple programs for λL iff L and respectively have function-restricted interactive proof systems. This implies that for any language L, adaptive chekers with noncommunicating multiple programs for λL are as powerful as static ones with a single program for λL.

In complex self-checking systems several blocks (i.e. functional blocks and checkers) are embedded. In order to check the self-checking properties of such blocks we need to know the set of vectors they receive from the blocks feeding their inputs (i.e. the code word output spaces of the source blocks). In a complex system the computation of the output spaces by means of exhaustive simulation of the system is intractable. In this paper we present a tool which performs this computation with low CPU time. Some other tools allowing to verify the self-checking properties of embedded blocks (like the strongly fault secure property of embedded PLAs and the self-testing property of embedded checkers), have also been developed and experimented.