¿Herramienta para el control de modelos de proyectos grandes y distribuidos de C++ como KDE?

Question

¿Existe alguna herramienta que pueda manejar el modelo de comprobación de sistemas distribuidos grandes, del mundo real, mayormente C++, como KDE?

(KDE es un sistema distribuido en el sentido de que usa IPC, aunque normalmente todos los procesos están en la misma máquina. Sí, por cierto, este es un uso válido de "sistema distribuido" - ver Wikipedia.)

La herramienta necesitaría ser capaz de manejar eventos de intraproceso y mensajes entre procesos.

(Vamos a suponer que si la herramienta es compatible con C++, pero no admite otras cosas que KDE utiliza como moc, podemos hackear algo juntos para solucionar eso.)

voy a aceptar alegremente menos general (por ejemplo, analizadores estáticos especializados para encontrar clases específicas de errores) o alternativas de análisis estático más generales, en lugar de verificadores de modelos reales. Pero solo estoy interesado en las herramientas que pueden realmente manejar proyectos del tamaño y la complejidad de KDE.

Answer 1

obviamente estás buscando una herramienta de análisis estático que puede

• de análisis C++ en escala
• localizar fragmentos de código de interés
• extraer un modelo
• pase ese modelo a un comprobador de modelos
• informe que resultan a que

Un problema importante es que todos tienen una idea diferente sobre qué modelo desean verificar. Eso solo probablemente mate la posibilidad de encontrar exactamente lo que desea, ya que cada herramienta de extracción de modelo generalmente ha elegido lo que quiere capturar como modelo, y las posibilidades de que coincida con lo que usted quiere, precisamente, están en mi humilde opinión a cero.

No tiene claro qué modelo desea específicamente, pero supongo que quiere encontrar las primitivas de comunicación y modelar las interacciones del proceso para buscar algo así como un punto muerto?

Los vendedores de herramientas de análisis estáticos comerciales parecen ser un lugar lógico para mirar, pero aún no creo que estén ahí. Coverity parece ser la mejor opción, pero parece que solo tienen algún tipo de análisis dinámico para Java.

Este documento pretende hacer esto, pero no he examinado en detalle: Compositional analysis of C/C++ programs with VeriSoft. Relacionado es [PDF] Computer-Assisted Assume/Guarantee Reasoning with VeriSoft. Parece que debe anotar a mano el código fuente para indicar los elementos de modelado de interés. La herramienta Verifysoft en sí misma parece ser propiedad de Bell Labs y es probable que sea difícil de obtener.

De manera similar esta: Distributed Verification of Multi-threaded C++ Programs.

Este documento también hace afirmaciones interesantes, pero no procesa C++ a pesar del título: Runtime Model Checking of Multithreaded C/C++ Programs.

Si bien todas las partes de esto son difíciles, un problema que todos comparten es analizar C++ (como se ejemplifica en el documento citado anteriormente) y encontrar los patrones de código que proporcionan la información bruta para el modelo. También necesita analizar el dialecto específico de C++ que está utilizando; no es agradable que los compiladores de C++ acepten diferentes idiomas. Y, como ha observado, es necesario procesar grandes códigos C++. Los inspectores modelo (SPIN y amigos) son relativamente fáciles de encontrar.

Nuestro DMS Software Reengineering Toolkit proporciona un análisis de propósito general, con coincidencia de patrones personalizables y extracción de hechos, y tiene un robusto C++ Front End que maneja muchos dialectos de C++. Probablemente podría configurarse para buscar y extraer los hechos que corresponden al modelo que le interesa. Pero no hace esto de la estantería.

DMS con su C front end se han utilizado para procesar aplicaciones C extremadamente grandes (¡19,000 unidades de compilación!). El front-end de C++ ha sido utilizado con enojo en una variedad de proyectos de C++ a gran escala, pero generalmente no a esa escala. Dada la capacidad general de DMS, creo que probablemente sea capaz de manejar grandes cantidades de código. YMMV.

Answer 2

Los analizadores de códigos estáticos cuando se usan contra la base de código grande la primera vez generalmente producen tantas advertencias y alertas que no podrá analizarlos todos en un período de tiempo razonable. Es difícil distinguir problemas reales del código que parecen sospechosos para una herramienta.

Puede intentar utilizar herramientas automáticas de descubrimiento invariante como "Daikon" que capturan invariantes percibidos en tiempo de ejecución. Puede validar más tarde si las invariantes descubiertas (equivalencia de las variables "a == b + 1", por ejemplo) tienen sentido y luego inserte las afirmaciones permanentes en su código. De esta forma, cuando se infringe una invariante como resultado de su cambio, recibirá una advertencia de que quizás usted haya roto algo con su cambio. Este método ayuda a evitar la reestructuración o cambiar el código para agregar pruebas y burlas.

Answer 3

La forma habitual de aplicar técnicas formales a sistemas grandes es modularizarlas y escribir especificaciones para las interfaces de cada módulo. Luego puede verificar cada módulo de forma independiente (mientras verifica un módulo, importa las especificaciones, pero no el código, de los otros módulos a los que llama). Este enfoque hace que la verificación sea escalable.