• 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.
Verification of quasi-synchronous systems with Uppaal
2014-10-01
366507 byte
Conference paper
Electronic Resource
English
Verification of quasi-synchronous systems with Uppaal
IEEE | 2014
|Online and Proactive Vehicle Rerouting with Uppaal Stratego
Transportation Research Record | 2021
|Formal Development of Multi-vessel Navigation of Maritime Autonomous Systems using UPPAAL STRATEGO
BASE | 2021
|