|
|
The Bandera Project integrates
existing programming language processing techniques with newly developed techniques
to provide automated support for the extraction of safe, compact, finite-state models
that are suitable for verification from Java source code.
|
| |
|
|
Bogor is an extensible software model checking
framework with state of the art software model checking algorithms, visualizations, and a user
interface designed to support both general purpose and domain-specific software model checking.
|
| |
|
|
Indus is an effort to provide a collection of
program analyses and transformations implemented in Java to customize and adapt Java programs.
|
| |
|
The S2aVES (Specification,
Synthesis and Verification of Embedded Systems) is investigating technologies for
specifying synchronization, distribution, and timing requirements of concurrent
embedded software, for synthesizing efficient low-level implementations from those
specifications and for verifying requirements of those implementations.
|
| |
|
|
Cadena is Eclipse Ready
and leverages several of its plugins (GEF and
EMF in particular) to provide a component-based
integrated development environment.
|
| |
|
|
TinyOS is an open-source operating system designed for wireless embedded sensor networks.
It features a component-based architecture which enables rapid innovation and implementation
while minimizing code size as required by the severe memory constraints inherent in sensor networks.
The Cadena team is currently developing extensions to the Cadena core framework that will allow
sensor network developers to model, analyze, develop, and deploy applications using Cadena. This
is all done through the plugin framework and provides an example of what can be accomplished
using the Cadena framework as a starting point for component-based development.
|
| |
|
|
OpenCCM is an Open Source project dedicated
to creating an open source implementation of the Object Management Group's CORBA Component
Model. The OpenCCM project is maintained by LIFL's
GOAL research team. Currently, OpenCCM
allows the compilation of OMG IDL3 specifications, and even generation of Java components
from IDL3 specifications.
|
| |
|
|
The development team uses JUnit for automated testing.
|
| |
|
|
The development team uses ANTLR for generating parsers. This
includes the custom built parser for nesC
used in the TinyOS platform plugin.
|
| |
|
|
The development team uses Apache Ant for automating
many routine tasks.
|
