The D-MILS technologies provide a distributed MILS platform and toolset for developing, verifying, configuring and deploying secure and dependable critical systems. The technologies that comprise the D-MILS development and deployment environments are the following:

• Modelling and Anlaysis Tools - Includes the MILS-AADL extended subset of standard AADL, syntax and formal semantics, and transformation technologies to support the languages of the backend tools in the D-MILS tool chain. Partner contacts for further information are FBK and RWTH Aachen University.
  Download the Modelling and Analysis Tools for evaluation.
  
• Compositional Verification Tools - Application of Contract-Based Design to in supporting MILS refinement claims and an integrated framework providing a high degree of verification automation and simulation. Partner contact for further information is FBK.
  Download the Compositional Verification Tools for evaluation.
  
• Assurance Case Tool - Automated support for compositional assurance with modular assurance case guided by declarative language features, and integration of verification results. Partner contact for futher information is University of York.
  Download the Assurance Case Tool.
  
• Configuration Compiler - Automated configuration of distributed MILS system that flows from high-level design specification and ensures coherency of system deployment across multiple nodes. The Configuration Compiler typically accompanies the commercial Platform components. Partner contact for further information is Universite Joseph Fourier.
  Download the Configuration Compiler for evaluation.
  
• Platform - Composed of an extended separation kernel developed by LynuxWorks to support distributed MILS implementations, and an enhanced time-triggered Ethernet system developed by TTTech. Platform components will be licensed as commercial products from these project partners.