VECA enables you to design correct component architectures using an expressive domain specific modeling language with a hierarchical component model, both operation-level and behavioral signatures (protocols), timed-related constraints and aspect-oriented features.
Mehdi Hariati, Pascal Poizat, and Djamel Meslati. Timed Verification of Aspect-Oriented Component Architectures.