Abstract:

Verifying software in mission-critical Cyber-Physical Systems (CPS) is an important but daunting task with challenges of accuracy and scalability. This paper discusses lessons learned from verifying properties of the Linux kernel. These lessons have raised questions about traditional verification approaches, and have led us to a model-based approach for software verification. These models are high-level models of the software, as opposed to the prevalent formal methods with low-level representations of software. We use models to gain insights into software verification challenges and use those insights to improve software verification. We demonstrate significant advantages of models with a Linux kernel study involving verification of 66;609 Lock instances. We use models to: (a) analyze and find flaws in verification results from LDV, a top-rated Linux verification tool, (b) show significant improvement over LDV by improving accuracy, speed, and by verifying 99.3% instances compared to 65.7% instances by LDV.

Venue: Invited Paper at the 2017 CPS Special Track at Winter Simulation Conference (WSC), Las Vegas, December 3-6, 2017

Authors: Suresh Kothari, Payas Awadhutkar, Ahmed Tamrawi, Jon Mathews

Paper (PDF): WSC.pdf