Resumen

Event-B es un lenguaje de modelado formal que es muy adecuado para la ingeniería de software, pero carece de la capacidad de modelar el tiempo. Los investigadores han propuesto algunos métodos para modelar restricciones de tiempo en Event-B. Las limitaciones de los métodos existentes son que, en primer lugar, el trabajo de investigación existente carece de un marco sistemático de refinamiento temporal basado en Event-B; en segundo lugar, los métodos existentes solo modelan el tiempo en el marco de Event-B y no pueden convertirse fácilmente en modelos basados en autómatas como autómatas temporizados que facilitan la verificación de propiedades temporales. Estas limitaciones hacen que sea más difícil modelar y verificar sistemas en tiempo real con Event-B, ya que es muy consumidor de tiempo probar propiedades temporales en el marco de Event-B. En este artículo, en primer lugar, proponemos un marco sistemático de refinamiento temporal para expresar y refinar restricciones de tiempo en Event-B. En segundo lugar, también proponemos varios patrones de refinamiento vertical y patrones de extensión horizontal para

• Materias:Colonias de abejas artificiales Inteligencia artificial Patrón espacial Innovación de la comunicación Algoritmo de red neuronal
• Subjects:Artificial bee colonies Artificial intelligence Spatial pattern Communication innovation Neural network algorithm
• Palabras claves:Propuesto; Modelando restricciones de tiempo; Limitaciones; Marco sistemático de refinamiento de tiempo; Sistemas en tiempo real; Propiedades de verificación
• Keywords:Proposed; Modeling time constraints; Limitations; Systematic time refinement framework; Real-time systems; Verification properties