VERDICT-0.6.0

This release includes bug fixes and improvements:

• Fix the parsing issue of antiJamming and antiJammingDAL
• Fix case-sensitivity of truth values in AADL
• Fix null pointer exception in CRV instrumentor and VDM2CSV
• Fix CSV printing for DAL properties for STEM
• Fix Soteria++ XML output format issue
• Update STEM queries and graphing
• Support safety analysis of AADL models

Known issue for Mac: Syntax highlight feature of VERDICT annex is not working for OSATE 2.3.2 + AGREE 2.3.7. However, you have a higher chance to get it working on Mac if you use OSATE 2.6.0 + AGREE 2.3.7. We have confirmed that the syntax highlight feature is working for that combination on Ubuntu. If you use OSATE 2.6.0, you will need to manually install AGREE 2.3.7 from the update site.

VERDICT-0.5.0

This release includes the following features:

• Use STEM runner to invoke STEM
• Support more AADL properties, although they are still hardcoded through the tool chain. The full list of properties can be found here.
• Support analysis on AADL hierarchical models

Currently, VERDICT only supports Mac OS and Ubuntu, and supports AGREE 2.3.7 or lower. This release does not support analysis of any of the Hawkeye UAV models because of the property name changes.

For Mac OS,

• We have tested the installation with OSATE 2.3.2 + AGREE 2.3.7
• Known issue: syntax highlighting function of VERDICT language annex is not working.

For Ubuntu,

• We have tested the installation with OSATE 2.5.0 + AGREE 2.3.7 and OSATE 2.6.0 + AGREE 2.3.7.

Please follow the README file in the release to install VERDICT.

2019-10-25-pre-release

Unpacking this tar archive and following the instructions in the README, if done without problems, will set up the VERDICT plugin in an OSATE IDE along with the VERDICT back-end tools ready to be called by the plugin to perform architectural and behavioral analysis of AADL models. This version removes the dependency on SADL Eclipse IDE.

2019-08-22 PI Demo binaries

Unpacking this tar archive and following the instructions in the README.md, if done without problems, will set up the VERDICT plugin in an OSATE 2.5.0 IDE along with the VERDICT back-end tools ready to be called by the plugin to perform architectural and behavioral analysis of AADL models, as was demo'ed during PI Day on August 22, 2019.