The critical nature of many complex software-intensive systems requires formal architecture descriptions for supporting automated architectural analysis regarding correctness properties. Due to the challenges of adopting formal approaches, many architects have preferred using notations such as UML, SysML, and their derivatives to describe the structure and behavior of software architectures. However, these semi-formal notations have limitations regarding the support for architectural analysis, particularly formal verification. This work investigates how to formally support SysML-based architecture descriptions to enable the formal verification of software architectures. As a result of this research, the main contribution is proposing a model-driven approach (MDD) that provides formal semantics to a SysML-based architectural language, SysADL, through a seamless transformation of SysADL architecture descriptions to the corresponding formal specifications in p-ADL, a well-founded theoretically language based on the higher-order typed p-calculus. The proposal implementation involves the execution of a four-phase process: (i) Model-to-Model (M2M) transformation of SysADL models into p-ADL model; (ii) Modelto-text (M2T) transformation of p-ADL models into p-ADL source; (iii) corresponding executable architecture generation, and architecture validation; and (iv) property verification. The work has other associated contributions to support the 4-phase process: (i) a denotational semantics to SysADL in p-ADL; (ii) a definition of a process to support the automated transformation of SysADL models into p-ADL models; (iii) The validation of the p-ADL architecture generated by the MDD transformation to demonstrate that it is in accordance with the original SysADL architecture; and (iv) the verification of formal architectural properties analyzing execution traces. The proposal was implemented and validated using a Flood Monitoring System architecture.A natureza crítica de muitos sistemas complexos de uso intensivo de software requer descrições formais de arquitetura para dar suporte à análise arquitetural automatizada em relação às propriedades de correção. Devido aos desafios de adotar abordagens formais, muitos arquitetos têm preferido usar notações como UML, SysML e seus derivados para descrever a estrutura e o comportamento das arquiteturas de software. No entanto, essas notações semi-formais têm limitações quanto ao suporte à análise arquitetural, principalmente à verificação formal. Este trabalho investiga como oferecer suporte formal a descrições de arquitetura baseadas em SysML para permitir a verificação formal de arquiteturas de software. Como resultado desta pesquisa, a principal contribuição é propor uma abordagem orientada a modelos (MDD) que fornece semântica formal para uma linguagem de arquitetura baseada em SysML, SysADL, por meio de uma transformação contínua das descrições da arquitetura SysADL para as especificações formais correspondentes em p-ADL, uma linguagem teoricamente bem fundamentada baseada no p-calculus de tipo de ordem superior. A implementação da proposta envolve a execução de um processo de 4 fases: (i) transformação modelo-a-modelo (M2M) de modelos SysADL em modelo p-ADL; (ii) transformação de modelo para texto (M2T) de modelos p-ADL em código p-ADL; (iii) geração de arquitetura executável correspondente e validação da arquitetura; e (iv) verificação de propriedades. O trabalho tem outras contribuições associadas para dar suporte ao processo de 4 fases: (i) uma semântica denotacional para SysADL; (ii) a definição de um processo para suportar a transformação automatizada de modelos SysADL em modelos p-ADL; (iii) A validação da arquitetura p-ADL gerada pela transformação MDD para mostrar que está de acordo com a arquitetura original SysADL; e (iv) a verificação de propriedades arquiteturais formais usando rastros de execução. A proposta foi implementada e validada utilizando uma arquitetura de Sistema de Monitoramento de Enchentes.