Formal Verification of AADL Models Using UPPAAL

• Fernando Silvano Gonçalves UFSC
• David Pereira CISTER/INESC-TEC Research Centre / ISEP/IPP
• Eduardo Tovar CISTER/INESC-TEC Research Centre / ISEP/IPP
• Leandro Buss Becker UFSC

Resumo

Cyber-Physical Systems (CPS) are known to be highly complex systems which can be applied to a variety of different environments, covering both civil and military application domains. As CPS are typically complex systems, its design process requires strong guarantees that the specified functional and non-functional properties are satisfied on the designed application. Model-Driven Engineering (MDE) and high-level specification languages are a valuable asset to help the design and evaluation of such complex systems. However, when looking at the existing MDE tool-support, it is observed that there is still little support for the automated integration of formal verification techniques in these tools. Given that formal verification is necessary to ensure the levels of reliability required by safety critical CPS, this paper presents an approach that aims to integrate the Model Checking technique in the CPS design process for the purpose of correctly analyzing temporal and safety characteristics. A tool named ECPS Verifier was designed to support the model checking integration into the design process, providing the generation of timed automata models from high-levels specifications in AADL. The proposed method is illustrated by means of the design of an Unmanned Aerial Vehicle, from where we derive the timed automata models to be analyzed in the UPPAAL tool.

Palavras-chave: Tools, Automata, Analytical models, Safety, System recovery, Complex systems, Model checking, Formal Verification, CPS Verification, Model-Driven Design Method, Model Checking, Models transformation, AADL, UPPAAL