• About Promise
• Probabilistic Network Fault and Performance Analysis
• Compositional Verification of Hybrid Dynamical Systems
• Probabilistic Failure Analysis
• Integrated Design Flow and Verification
• Publications
• Posters
• Tools

Integrated Design Flow and Verification

• We integrated two verification tools into the META workflow:

  1. the HybridSAL hybrid model checker and
  2. the Honeywell Lifecycle Tools & Environment (HiLiTE).

  The integration of HybridSAL and HiLiTE into the CyPhy language and design environment enhances the META workflow with essential verification capabilities:

  1. model checking of dynamic properties based on qualitative and relational abstractions and
  2. static analysis of signal properties in large-scale, embedded control software. Further, we adopted a general approach, which is independent of the verification tools and provides the infrastructure to integrate additional tools.

  The implementation provides generic templates for:

  1. integrating models suitable for verification and linking them to architecture models in CyPhy and
  2. incorporating verification certificates into the system models that can be used in the design space exploration.

  
  The META approach to reusability of library components can only be realized if detailed design properties of integrated components are automatically verified as parameters are selected and fine-tuned for specific vehicle configurations. Providing automated verification tools that give feedback to the designer by tracing causes of violations across components is key to success. The integrated CyPhy-HiLiTE tool provides such capability.
  
  Checking safety and stability properties of designs early in the process is important so as to avoid proceeding with designs that do not satisfy these crucial requirements. The integrated CyPhy-HybridSAL capability allows checking such requirements during the design phase.
  
  Industry observation has shown that 40-50% of all defects are injected in model design phases. Other studies have shown that problems found at code testing can cause much more effort than if caught in early design. Thus, integrating verification tools into the design phase is a solution to reduce time and cost of software development because errors can be detected early.
  
  A feature which is critical in decreasing time schedules is the capability to automate the management of labor intensive tasks, such as the static analysis of large scale embedded control software, and seamlessly integrating the verification results with the architecture models and the design space exploration process.
  
  Related Publications TBA
  
  Related Posters TBA
  
  Tool Download TBA