• 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.


    Zugriff

    Download


    Exportieren, teilen und zitieren



    Titel :

    Verification of quasi-synchronous systems with Uppaal


    Beteiligte:


    Erscheinungsdatum :

    01.10.2014


    Format / Umfang :

    366507 byte




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Verification of quasi-synchronous systems with Uppaal

    Bhattacharyya, S. / Miller, S. / Yang, J. et al. | IEEE | 2014


    Online and Proactive Vehicle Rerouting with Uppaal Stratego

    Bilgram, Alexander / Ernstsen, Emil / Greve, Peter et al. | Transportation Research Record | 2021


    Schedulability Analysis of Distributed Multicore Avionics Systems with UPPAAL

    Han, Pujie / Zhai, Zhengjun / Nielsen, Brian et al. | AIAA | 2019

    Freier Zugriff