Abstract:

In this talk the two verification tools TAV and EPSILON will be presented. The presentation will include the formal basis and emphasize the underlying philosophy and pragmatics through applications. TAV is a tool intended to be useful in constructing CCS (or finite state) implementations in a stepwise refinement and compositional manner. This tool is firmly based on the theory of Modal Specifications allowing loose specifications to be expressed. The theory includes a "bisimulation"-like refinement between specifications and allows specifications to be combined with respect to the operations of CCS. Recently the theory of Modal Specifications has been extended with explicit real--time constructs. The tool EPSILON provides automatic support for verifying several abstracting refinements between real--time specifications and real--time processes (using Wang Yi's TCCS) as well as model--checking facilities.