Model checking techniques are useful for design of high-reliable information systems. The well-known problem of state explosion, however, might occur in model checking of large systems. Such explosion severely limits the scalability of model checking. In order to avoid it, several abstraction techniques have been proposed. Some of them are based on CounterExample-Guided Abstraction Refinement (CEGAR) loop technique proposed by E. Clarke et al.. This paper proposes a concrete abstraction technique for timed automata used in model checking of real time systems. Our technique is based on CEGAR, in which we use a counter example as a guide to refine the abstract model. Although, in general, the refinement operation is applied to abstract models, our method modifies the original timed automaton. Next, we generate refined abstract models from the modified automaton. This paper describes formal descriptions of the algorithm and the correctness proof of the algorithm.

This paper describes the effects of system LSI design with C language-based behavioral synthesis following several trials of design period reduction and quality improvement for a variety of circuit types. The results of these trials are analyzed from the viewpoints of description productivity, verification productivity, reusability and design flexibility as well as hardware and software co-verification. First the C-based design flow proposed by the authors is described, and the design productivity and verification productivity under this design flow is compared to RTL design. The reusability of the behavioral IP core and its efficiency with HW/SW co-verification are also shown using design examples. Next, using the example of an MPEG-4 video decoder design, a typical design process in a C-based design is shown with considerations regarding verification efficiency, reusability of the IP core and HW/SW co-verification. Finally, the authors' perspectives regarding future directions of system LSI design are discussed.