Compiling timed algebras into timed automata

• Autores: Sergio Yovine
• Localización: Panel '92: actas, XVIII Conferencia Latinoamericana de Informática, 1992, págs. 1243-1250
• Idioma: inglés
• Texto completo no disponible (Saber más ...)
• Resumen

  • Real-time systems are hard to model, specify and design. It is common practice today to pass from informal specifications to implementations and then test the behavoir of the system on some cases, which is inadequate to develop bug-free real-time systems. To ensure correctness we need to employ automatic verification methods and tools. The following real-time software development process has been proposed in [7]: ATP is used to describe real-time systems and TCTL to specify the real-time requirements. The verification approach consists in translating ATP to timed automata and then performing model-checking. In this work we present a tool that compiles ATP terms into timed automata.