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


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Verification of quasi-synchronous systems with Uppaal


    Contributors:


    Publication date :

    2014-10-01


    Size :

    366507 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Verification of quasi-synchronous systems with Uppaal

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


    Schedulability Analysis of Distributed Multicore Avionics Systems with UPPAAL

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


    Online and Proactive Vehicle Rerouting with Uppaal Stratego

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


    Formal Development of Multi-vessel Navigation of Maritime Autonomous Systems using UPPAAL STRATEGO

    Shokri-Manninen, Fatima / Vain, Jüri / Waldén, Marina | BASE | 2021

    Free access