• 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
01.10.2014
366507 byte
Aufsatz (Konferenz)
Elektronische Ressource
Englisch
Verification of quasi-synchronous systems with Uppaal
IEEE | 2014
|Online and Proactive Vehicle Rerouting with Uppaal Stratego
Transportation Research Record | 2021
|Schedulability Analysis of Distributed Multicore Avionics Systems with UPPAAL
AIAA | 2019
|Introducing Liveness into Multi-lane Spatial Logic lane change controllers using UPPAAL
DOAJ | 2018
|Introducing Liveness into Multi-lane Spatial Logic lane change controllers using UPPAAL
ArXiv | 2018
|