Eliciting Unitary Constraints from Timed Sequence Diagram with Symbolic Techniques: Application to Testing

In early design phases, system models can be characterized as intended interactions between black box components. Moreover, when dealing with embedded systems, it is usual that interactions are constrained by timing issues. We propose to represent such system models as structured scenarios by using UML sequence diagrams specialized with the MARTE profile to handle timing constraints. By using symbolic execution techniques, we show how to analyze these system models and how to extract behavioral constraints concerning components. Those constraints can be used as unitary test purposes to select components of the system.