Hispanopedia WikiLibdmc [ 1 ] [ 2 ] es una biblioteca diseñada en el laboratorio LIP6 [ 3 ] . Su objetivo es facilitar la distribución de verificadores de modelos existentes . También se ha diseñado para proporcionar las interfaces más genéricas, sin sacrificar el rendimiento, gracias al lenguaje C++ .
La verificación de modelos ofrece una forma de demostrar automáticamente que el comportamiento de un sistema modelado es correcto mediante la verificación de propiedades. Sin embargo, adolece del problema de la explosión del espacio de estados , causado por un uso intensivo de la memoria. Se han propuesto muchas soluciones para superar este problema (por ejemplo, representaciones simbólicas con diagramas de decisión, como BDD ), pero estos métodos pueden generar rápidamente un consumo de tiempo inaceptable.
La verificación de modelos distribuida es una forma de superar los problemas de consumo de memoria y tiempo mediante el uso de recursos agregados de un clúster dedicado. Sin embargo, reescribir un verificador de modelos completo es una tarea difícil, por lo que el enfoque de libdmc consiste en proporcionar un marco para construir un verificador de modelos.
Referencias
- ↑ Hamez, Alexandre; Kordon, Fabrice; Thierry-Mieg, Yann (2007). "IibDMC: Una biblioteca para operar una verificación de modelos distribuidos eficiente". 2007 IEEE International Parallel and Distributed Processing Symposium . pp. 1–8 . doi : 10.1109/IPDPS.2007.370647 . ISBN 978-1-4244-0909-9. S2CID 12586847 .
- ↑ Hamez, Alexandre; Kordon, Fabrice; Thierry-Mieg, Yann; Legond-Aubry, Fabrice (2007). "DMCG: Un verificador de modelos simbólicos distribuidos basado en GreatSPN". Redes de Petri y otros modelos de concurrencia – ICATPN 2007. Notas de clase en informática. Vol. 4546. pp. 495–504 . doi : 10.1007/978-3-540-73094-1_29 . ISBN 978-3-540-73093-4.
- ↑ Inicio LIP6
- Verificadores de modelos
- Esbozos de bioinformática
- Stubs de Unix