Tools

Software Tools used in CIS 771

Below are the links to the tools that we will use in the course. Each of these tools is available for Windows, Linux or Mac OS X platforms. If you want your own copy just download and install (its pretty easy).

• Alloy and its Constraint Analyzer are an object modeling language and analysis tool, respectively.

• USE is a UML-based tool that processes class diagrams and OCL specifications. Models conforming to the class diagrams can be animated and automatically checked against the given OCL specifications.

  • SourceForge page for USE.

• Bakar Kiasan is a contract-based automated verification and test case generation tool-set for Spark/Ada.

  To download and install Bakar, see the instructions given on the Sireum Download page. Ensure that you download the "managed" version. After running sireum for the first time, install Bakar by running the command: sireum launch bakar.