AGAVE is an agile -iterative and incremental- tool to verify evolving software specifications. AGAVE can be applied in different modeling languages, but so far has been implemented to verify Statecharts against Path-CTL properties.

The tool takes as input two XML files, one representing the model of the system (Statechart) and one representing the property to verify (in Path-qCTL). The property is specified into a txt file. The tool return “true”, “false”, or “conditional”. In the conditional case, a set of constraints on transparent states is reported as well.

AGAVE takes as input three files:
Example1.xml contains the Statechart to be analyzed
Example1Property.txt contains the property to be verified
Example1InitialState.txt contains the initial values of the atomic propositions
To run AGAVE download these three file plus AGAVE.jar in the same folder .
Then, from the command line type:
java -jar AGAVE.jar

Project Activity

See All Activity >

Follow AGAVE

AGAVE Web Site

Other Useful Business Software
Build Agents and Models on One Platform Icon
Build Agents and Models on One Platform

Everything you need to build production-ready agents and models. Access 200+ Google and third-party AI models and tools.

Gemini Enterprise Agent Platform is Google Cloud's comprehensive platform for developers to build, scale, govern, and optimize agents and models. Choose from Google's most advanced models and third-party models like Anthropic's Claude Model Family.
Start Free
Rate This Project
Login To Rate This Project

User Reviews

Be the first to post a review of AGAVE!

Additional Project Details

Registered

2013-02-06
Report inappropriate content