Home BLESS plugins to Eclipse/OSATE

BLESS plugins to Eclipse/OSATE

The on-line update does not work, yet. Until I figure out how to get Eclipse to recognize the update site, use the "local" site installation instructions below.

The BLESS editor and proof tool are Eclipse plugins to the Open-Source AADL Tool Environment (OSATE) which is itself plugins to Eclipse.

To use BLESS, OSATE must first be downloaded and installed. Then the BLESS plugins can be added by an Eclipse update site.

Although you could download Eclipse, and then install OSATE using update sites, it's much easier to download a pre-build version of Eclipse having OSATE already installed. OSATE builds for Linux, Mac OS, and Windows can be downloaded from OSATE Stable Latest Products. The version current at this writing is osate2-2.2.1, 14-Oct-2016. More about AADL and OSATE can be found at the websites linked below.

For Mac OS, download osate2-2.2.1-vupdate02-macosx.cocoa.x86_64.tar.gz, double click the file to unzip it, drag the result to your Applications folder, make an alias and drop it on your dock for easy launch. Double-click the "osate2" icon to launch it.

Eclipse will ask you for a "Workspace", and suggest a default. Better to click the "Browse" button to select, or create, a folder easy to find.

To install BLESS, under the "File" menu, find "Install New Software...". Click the "Add..." button; choose a name (like "BLESS") and then copy this address into "Location": http://bless.santoslab.org/update. Uncheck the "Group items by category" box. Click "Next". Select the two BLESS plugins. Click "Next" again. Carefully read the license terms for each plugin (they are different), accept the license (if you agree). Click "Finish". Agree if asked whether you want to install software from unknown sources, and restart Eclipse to use the new software.

Alternatively, you could download the bless_update.zip update site, unzip it, then install it as a "Local" update site, selecting the unzipped folder (com.multitude.bless.update) in the file-chooser pop-up.

You must then File -> Import... any example projects, open just projects you want to prove. Click the praying-hand icon to wake-up the BLESS plugins, then start to use it! Try BLESS -> "get new script" selecting the proof script in an open project. Use "step script" repeatedly to see what it does, or "run script" to do it all at once.

All of the proof scripts have been tested to work with this version of the plugins, and a copy of the resulting proof put in the "proof" folder.

If you need assistance please email: brl@ksu.edu or brl@multitude.net