CorrettoUML is a prototype research tool developed at Politecnico di Milano to translate Corretto UML (C-UML) models into the TRIO temporal logic formalism which is suitable to be formally verified using the Zot bounded model/satisfiability checker.
The following figure describea in more details how Corretto works.
The user creates a C-UML models using Papyrus. Corretto supports both static and behavioral diagrams of different types. The different views communicates by means of a shared set of events enabling the possibility to define complex behaviors. Also, dedicated time concepts borrowed from UML/MARTE have been included to predicate on the time dimension of the system. The C-UML Superstructure Specification presents the metamodels for C-UML models.
Once the C-UML model is completed the user can use Corretto to formally verify its correctness with two types of checks:
-
Model consistency: A C-UML model is consistent if the different views do not contradict each other. Formally this is translated into the fact that the underlying formal model has at least one execution trace.
-
User defined properties: In C-UML, the properties to be checked are expressed through the Corretto Property Language (CPL), which is inspired by OCL and has a straightforward translation into the TRIO metric temporal logic. The properties to be checked are introduced through a special-purpose constraint associated with the main C-UML model package, which is tagged with stereotype «property» and contains a sequence of declarations in CPL.
Once the user decides to run the formal verification, the C-UML models are first exported in the XMI format, and then translated into their corresponding TRIO metric temporal logic semantics with a suitable transformation tool. Zot is then fed by the formal model. Zot relies on both the Satisfiability solvers (SAT) and the Satisfiability Modulo Theories solvers (SMT) to verify if the property specified by the user holds or not. If the property holds no action is required on the model and the user is just notified of the result. If the property does not hold, a counterexample is returned. Counterexamples in Zot are simple text traces representing an execution of the system that violates the property.
Corretto automatically associate each element in the Zot trace to its corresponding element in the C-UML model. Navigating the trace resume closely the debugging paradigm of well know programming languages. This is an example:
