Contributions to Improvement of the Formal Properties Verification Process in AADL Programs

Assuring the correctness of a system´s behavior is a must when dealing with critical systems. For instance, the Topcased project proposed several tools and methods in order to model such systems and to verify its behavior prior to implementation. In this scenario, the AADL modeling language plays a key role. Using this language, one can perform transformations to models with lower abstraction levels and perform the verification of properties. To ease this process, this paper presents a recently developed tool that provides a more intuitive way of constructing the sentences for property verification. It also helps the visualization of the verification results and enables to track the system´s behavior from its initialization up to the point where the property couldn´t be sustained. We illustrate its use and highlight its contributions with the modeling and verification of a pacemaker system.