Tools

ome of the tools we have or are developing:

Contractor

 

Contractor.NET

 

MTSA

An automated tool that takes a software contract or an API source code and generates a finite abstract representation useful for its validation.

 

A .NET version of Contractor, a validation and specification strengthening tool.

 

The Modal Transition System Analyzer.

         

JConsume2

 

Consume.NET

 

Resource Contracts.NET

A compositional analysis for inferring heap memory consumption in Java programs.

 

A .NET version of JConsume, a compositional analysis for inferring heap memory consumption in .NET programs.

 

 

An extenstion of Code Contracts to specify and verify memory consumption constraints in .NET programs.

         

JScoper

 

VIn Time

 

ObsSlice

 

An Eclipse plug-in that assist transalation of Java applications to Java Real Time ones.

 

 

A tool suite for the verification of Real Time systems.

 

 

A timed Automa Slicer based on Observers.

         

VTS

 

Zeus

 

SetPoint

Is a notation for expressing real-time requirements in a visual and friendly, yet powerful, language, by means of negative scenarios.

 

 

Is a distributed model checker that evolves from KRONOS.

 

 

An Aspect-Oriented Tool based on semantic pointcuts, developed using Microsoft's .NET framework.

         

TraceIt!

 

BudaPest

   

 

Event Trace Generator for Distributed Real-Time Applications.

 

An automated Software Verifier.

   
English