Verification tool announcement: RED v.1.0

• Subject: Verification tool announcement: RED v.1.0
• From: farn@iis.sinica.edu.tw (Farn Wang)
• Date: Thu, 10 Feb 2000 11:33:22 +0800
• Cc: farn@iiserv.iis.sinica.edu.tw

We apologize if you have received multiple copies of this message. 

======================================
ANNOUNCEMENT OF NEW VERIFICATION TOOL.  
======================================
RED
Region-Encoding Diagram Verification Tool
Version 1.0

http://www.iis.sinica.edu.tw/~farn/red
---------------------------------------

Farn Wang 
Institute of Information Science, Academia Sinica
Taipei, Taiwan 115, ROC

RED is a fully symbolic verification tool with a new data-structure 
for the encoding of regions of timed automata. 
Unlike DBM-technology, RED records the ordering among fractional parts
of clock readings with one auxiliary variable per clock.  
This new version 1.0 is for multiprocess real-time systems 
with unrestricted number of global clocks and local clocks.  
Version 1.0 also supports synchronizers among processes and 
more general assignment and literal syntax.  
You are most welcome to download the tool and relevant reports at 

  http://www.iis.sinica.edu.tw/~farn/red

All comments on the tool will be appreciated.  

Note that RED version 0.0 was announced around November 1999 
with the name DDD (Data-Decision Diagram).  
We changed to the new name "RED" because two parties 
notified us that they had used the name before. 
Version 0.0 is for symmetric systems with single local clock per process 
and without synchronizers and global clocks.  
For such target systems, version 0.0 performs better. 
We plan to merge the two versions (0.0 and 1.0) into the upcoming 
version 1.1 shortly.  

• Prev: FMOODS'2000 cfp - WITH SUBMISSION INSTRUCTIONS!
• Next: CfP: ECOOP 2000 Workshop on Formal Techniques for Java Programs
• Index: AMAST Mail 2000