Red

RED

Description: RED is a model-checker for timed automatas (TA). REDLIB is a library that allows programmers to access the functions in RED. Now REDLIB supports the following verification tasks.

• Full TCTL model-checking with event specifications and multiple fairness assumptions. (See examples)
• Simulation checking between TAs with event specifications and multiple fairness assumptions. (See examples)
• Parametric safety/risk analysis of linear hybrid autoamtas (LHA). (See examples)

A feature of the RED technology is that it is totally based on symbolic technology with BDD-like diagrams. Specifically, now it supports the following two data-structures. All state spaces, including pre-condition and post-conditions are represented and manipulated with these data-structures in RED and REDLIB.

VO Integration: No

Active: No

Available Benchmarks: No

Website: https://sites.google.com/site/redlibtw/

Download: Link to sourceforge project.

Documentation: Link

Contact: N/A

Excerpt from: https://sites.google.com/site/redlibtw/