AGAVE

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 ﬁles, 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

Gen AI apps are built with MongoDB Atlas

The database for AI-powered applications.

MongoDB Atlas is the developer-friendly database used to build, scale, and run gen AI and LLM-powered apps—without needing a separate vector database. Atlas offers built-in vector search, global availability across 115+ regions, and flexible document modeling. Start building AI apps faster, all in one place.

Start Free

Rate This Project