RC META

From AadlWiki

Jump to: navigation, search

The Rockwell Collins META toolset was developed under DARPA's META program. This Eclipse-based toolset provides a SysML-AADL translator, an architectural design pattern tool based on EDICT, a static model verification tool (Lute), and a compositional verification tool (AGREE) based on the KIND model checker.

For more information contact Darren Cofer at Rockwell Collins Advanced Technology Center.

Contents

Installation

An installer for Windows is available (warning: >300MB). The Guided Tour document provides an overview of the tools and a demonstration based on the example models.

In general, all of the files you need will be provided by the installer. However, there are several additional steps and dependencies, some of which are automated by the installer. In case you need to complete any of them manually, they are:

  • Add the C:\Program Files\RC_META_TOOLS\KIND directory to your path.
  • Create a new environment variable PKIND_HOME with value C:\Program Files\RC_META_TOOLS\KIND (or wherever kind is installed)
  • Download libyices.dll. You need version 1.0.29 of yices. Copy this dll file into your KIND directory.
  • Run the installer for MPICH2 (mpich2-1.4.1p1-win-ia32.msi) in the RC_META_TOOLS\KIND directory. Accept any default options. This program is needed by Kind.
  • If you install Enterprise Architect (or the trial version) and want to import/export SysML models, you will need to copy the files eaapi.jar and SSJavaCOM.dll from C:\Program Files\Sparx Systems\EA\Java API. Put eaapi.jar into the EDICT\plugins directory (also OSATE\plugins if you use it instead) and put SSJavaCOM.dll in your C:\WINDOWS\system32 directory.

Instructions for manually installing and using the tools can be found in README files located in the subdirectories. Manual installation should be done in the following order.

Enterprise Architect

The example models provided in this distribution were created in SysML using Enterprise Architect and translated into AADL with the SysML to AADL plug-in. While the AADL models can be modified directly, to modify the SysML models and re-translate them into AADL, a copy of Enterprise Architect is needed. Instructions on how to obtain a trial version can be found in the README file in the Enterprise Architect directory on at the Sparx Systems website.

Examples

The Example Models directory contains three example models. The first is the "Initial Avionics System" that contains an idealized model of the avionics system before patterns are applied. The second is the "Avionics_System_After_Pattern_Application" that contains an intermediate version created by the application of patterns. The third is the "Final_Avionics_System" that contains the final version after the intermediate version is edited. SysML and AADL versions of all models can be found in their respective directories.

OSATE

OSATE is an open-source eclipse-based framework for constructing and analyzing AADL models. Our tools are based on OSATE version 2 (alpha-3). Instructions on installing OSATE can be found in the README file in the OSATE directory.

EDICT

The EDICT tool is a proprietary extension of OSATE developed by WW Technology Group. Our tools are compatible with both OSATE and EDICT, though the pattern application tool developed by WWTG is only available through EDICT. Instructions on installing EDICT can be found in the README file in the EDICT directory. You will need to request an evaluation license for EDICT from WW Technology.

Users who wish to forgo the propritary EDICT tool may still use the other tools by installing OSATE version 2 (alpha-3).

Plug-ins for OSATE and EDICT

The OSATE/EDICT Plug-ins are located in the Plugins directory of this distribution. Instructions on installing them in OSATE and EDICT can be found in the README file in the Plugins directory.

Kind

Kind is a k-induction smt-solver developed by the University of Iowa used to check behavioral properties of the example models. Instructions on installing Kind can be found in the README file in the Kind directory.

User Manuals

User manuals for the plug-ins are located in the User Manuals directory. Once the tools are installed, the Guided Tour can be followed to use the tools on a demonstration example.

Personal tools