Model checking embedded systems with PROMELA Artigo de Conferência