Verification of quasi-synchronous systems with Uppaal

• Formal verification for a synchronous system is considerably faster and easier than for a quasi-synchronous or asynchronous systems • Uppaal´s strength is in the support for real-time capabilities with realtime clocks. • Uppaal seems to be very well suited for modeling concurrent, asynchronous components, particularly if real-time properties are of interest. • Translating AADL models into Uppaal posed several challenges. — Uppaal uses the same construct, the process, for both concurrency and modularity. — Uppaal doesn´t provide separate constructs for nested subcomponents that execute synchronously, with bounded asynchrony at the top-most level. So subcomponents had to be constrained to execute synchronously. • Additional constructs for structuring Uppaal templates would have made this easier. — Many of our safety properties are most easily specified using a pre operator to refer to the previous value of a variable. A next-state operator in Uppaal would address this need.