Home BLESS plugins to Eclipse/OSATE

BLESS plugins to Eclipse/OSATE

Eclipse Update Site: http://santoslab.org/pub/bless/update/site2.xml

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. More about AADL and OSATE can be found at the websites linked below.

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.

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