Tools
ReqsCov
ReqsCov is a tool which allows a user to measure the requirements coverage provided by a test suite over a Lustre model. The tool allows three requirements coverage metrics (each defined over Linear Temporal Logic requirements) to be measured: naive coverage, antecedant coverage, and Unique First Clause (UFC) coverage.
Downloads
The Crisys Eclipse plugin update site is found here: http://crisys.cs.umn.edu/eclipse-updates/
The ReqsCov command line tool is found here: reqscov.zip
Installation
Installation of ReqsCov is done as follows:
First, the command line tool must be installed. This is as simple as downloading the tool, unpacking it into an appropriate directory (e.g. "C:\Crisys_Tools"), and then adding said directory to your working path. Note that currently, ReqsCov is only available for Windows and has only been tested on Windows XP.
Second, a ReqsCov Eclipse plugin can be installed. While this plugin is not required to use ReqsCov, it is a little easier than using the command line tool. The plugin requires that the command line tool be already installed.
A command line usage message is displayed by calling "ReqsCov" with no arguments. The ReqsCov Eclipse plugin is used by selecting "ReqsCov" from the "FormulaEvaluator" menu.
Publications
Below is a list of papers related to ReqsCov. These papers outline the requirements coverage metrics measured by ReqsCov and the reasoning behind using such metrics. (Papers outlining the effectiveness of the metrics are forthcoming.)
SMACCM Tools
New generations of military vehicles, including unmanned air vehicles (UAVs), are almost universally being equipped with network interfaces. In addition to the baseline control and monitoring capabilities, network connectivity can provide advanced features such as the ability to adapt to new missions through field upgrades and remote access for maintenance. These network connections typically rely on standard protocols for compatibility with other networked systems and reduction of cost through the use of COTS equipment. As UAV systems continue this rapid evolution toward network access, there is great danger that insufficient attention is being paid to security concerns. A new approach based on comprehensive use of formal methods throughout the development process is needed to ensure that such vulnerabilities are eliminated from critical military assets. Rockwell Collins and University of Minnesota teams bring together key technologies and leading researchers with the experience needed to create a revolutionary approach to the development of these high-assurance systems.
Downloads
FM Workbench: This software package contains the AADL model and some verification properties for the unmanned aerial system used as part of the Secure Mathematically-Assured Composition of Control Models (SMACCM) research project under the HACMS program. This package also contains the Lute plug-in for OSATE in which the properties are encoded.
META Tools
The Rockwell Collins/UMN META toolset was developed under DARPA's META program.
Downloads
META-demo: This Eclipse-based toolset provides a SysML-AADL translator, a static model verification tool (Lute), and a compositional verification tool (AGREE) based on the JKind model checker. It requires the OSATE AADL tool environment.