|Final Report of the COST-247 Action|
Timed Modal Specifications: An Extension of CCS with Time and Refinement
Kim Guldstrand Larsen
|Department of Computer Science|
|Fredrik Bajers Vej 7E|
|DK - 9220 Aalborg|
|Tel: +45 98158522|
|Fax: +45 98158129|
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.
This presentation has been given during the COST-247 4th Management Committee Meeting (Berlin, Germany, February 9--10, 1995).
COST-247 Working Group(s): 1-2
This Page was prepared by Mark Jorgensen.