Specification by existing design plus use-cases

摘要

It is difficult to specify a system completely with formal methods. There are don't care situations which may not be so clearly defined, and behaviors of some special cases are hard to describe. Recently, it has been found that if the changes inside a design are local (limited within a set of sub-circuits), complete verification becomes feasible with small numbers of simulations. This gives us a way to specify a system as a modification of an existing design. By defining which portions of the existing design should be modified in which ways, it can become a design for the new specification. In this paper, we propose such a specification method, i.e., specifying new designs by giving existing designs and use-cases that discribes the difference from the new specification. The difference may be completely described with a small set of simulation patterns. Illustrative examples and some preliminary experimental results are shown.