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

nel_h2

MongoDB Atlas runs apps anywhere

Deploy in 115+ regions with the modern database for every enterprise.

MongoDB Atlas gives you the freedom to build and run modern applications anywhere—across AWS, Azure, and Google Cloud. With global availability in over 115 regions, Atlas lets you deploy close to your users, meet compliance needs, and scale with confidence across any geography.

Start Free

Rate This Project