Physically Asynchronous/Logically Synchronous (PALS) is an architecture pattern that allows developers to design and verify a system as though all nodes executed synchronously. The correctness of PALS protocol was formally verified. However, the implementation of PALS adds additional code that is otherwise not needed. In our case, we have a middleware (PALSWare) that supports PALS systems. In this paper, we introduce a verification framework that shows how we can apply Software Model Checking (SMC) to verify a PALS system at the source code level. SMC is an automated and exhaustive source code checking technology. Compared to verifying (hardware or software) models, verifying the actual source code is more useful because it minimizes any chance of false interpretation and eliminates the possibility of missing software bugs that were absent in the model but introduced during implementation. In other words, SMC reduces the semantic gap between what is verified and what is executed. Our approach is compositional, i.e., the verification of PALSWare is done separately from applications. Since PALSWare is inherently concurrent, to verify it via SMC we must overcome the statespace explosion problem, which arises from concurrency and asynchrony. To this end, we develop novel simplification abstractions, prove their soundness, and then use these abstractions to reduce the verification of a system with many threads to verifying a system with a relatively small number of threads. When verifying an application, we leverage the (already verified) synchronicity guarantees provided by the PALSWare to reduce the verification complexity significantly. Thus, our approach uses both “abstraction” and “composition”, the two main techniques to reduce statespace explosion. This separation between verification of PALSWare and applications also provides better management against upgrades to either. We validate our approach by verifying the current PALSWare implementation, and several PALSWare-based distributed real time applications.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Applying software model checking to PALS systems


    Contributors:
    Nam, Min-Young (author) / Sha, Lui (author) / Chaki, Sagar (author) / Kim, Cheolgi (author)


    Publication date :

    2014-10-01


    Size :

    3203621 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Applying software model checking to PALS systems

    Nam, Min Young / Chaki, Sagar / Sha, Lui et al. | IEEE | 2014

    Free access

    Parking pals

    Blake,T. / Bosch,Stuttgart,DE | Automotive engineering | 2016


    Software model checking for avionics systems

    Cofer, Darren / Whalen, Michael / Miller, Steven | IEEE | 2008


    PALS observations of soil moisture in SMEX02

    Njoku, E. / Wilson, W. / Yueh, S. et al. | NTRS | 2003


    Applying model checking to an automotive microcontroller application

    Schlich, B. / Salewski, F. / Kowalewski, S. | Tema Archive | 2007