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

Our Free Plans just got better! | Auth0

With up to 25k MAUs and unlimited Okta connections, our Free Plan lets you focus on what you do best—building great apps.

You asked, we delivered! Auth0 is excited to expand our Free and Paid plans to include more options so you can focus on building, deploying, and scaling applications without having to worry about your security. Auth0 now, thank yourself later.

Try free now

Rate This Project