Applying software model checking to PALS systems

Min Young Nam, Lui Raymond Sha, Sagar Chaki, Cheolgi Kim

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publication2014 IEEE/AIAA 33rd Digital Avionics Systems Conference, DASC
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages5B41-5B414
ISBN (Electronic)9781479950010
DOIs
StatePublished - Dec 8 2014
Event33rd Digital Avionics Systems Conference, DASC 2014 - Colorado Springs, United States
Duration: Oct 5 2014Oct 9 2014

Publication series

NameAIAA/IEEE Digital Avionics Systems Conference - Proceedings
ISSN (Print)2155-7195
ISSN (Electronic)2155-7209

Other

Other33rd Digital Avionics Systems Conference, DASC 2014
CountryUnited States
CityColorado Springs
Period10/5/1410/9/14

ASJC Scopus subject areas

  • Aerospace Engineering
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Applying software model checking to PALS systems'. Together they form a unique fingerprint.

Cite this