EMERALD: An Automated Modeling and Verification Tool for Component-Based Real-Time Systems

Abstract—Controller automata are a formal theory to model and analyze real-time systems with mutex components. It is mainly designed for a small scale real-time system in the low-level sequential behaviors, where control passing is explicitly handled. A controller automaton properly extends a timed automaton. Given a strict partial order over states, an ordered controller automaton can be faithfully translated into a timed automaton. We present a tool named EMERALD to translate ordered controller automata into timed automata and perform the transformation between their specifications in order to use the existing model checking engine or timed automata, say, UPPAAL. Case studies show that our tool can be effectively used in modeling and verification of component-based real-time systems. Keywords-Real-time systems, modeling, verification, con-troller automata, timed automata I