next up previous

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
Aalborg University
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.

Back to the VASY Home page