More Scalable LTL Model Checking via Discovering Design-Space Dependencies (D3)

Thumbnail Image
Date
2018-04-12
Authors
Dureja, Rohit
Rozier, Kristin Yvonne
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Authors
Person
Rozier, Kristin Yvonne
Associate Professor
Research Projects
Organizational Units
Organizational Unit
Organizational Unit
Organizational Unit
Journal Issue
Is Version Of
Versions
Series
Department
Aerospace EngineeringComputer ScienceElectrical and Computer Engineering
Abstract

Modern system design often requires comparing several models over a large design space. Different models arise out of a need to weigh different design choices, to check core capabilities of versions with varying features, or to analyze a future version against previous ones. Model checking can compare different models; however, applying model checking off-the-shelf may not scale due to the large size of the design space for today’s complex systems. We exploit relationships between different models of the same (or related) systems to optimize the model-checking search. Our algorithm, D3 , preprocesses the design space and checks fewer model-checking instances, e.g., using nuXmv. It automatically prunes the search space by reducing both the number of models to check, and the number of LTL properties that need to be checked for each model in order to provide the complete model-checking verdict for every individual model-property pair. We formalize heuristics that improve the performance of D3 . We demonstrate the scalability of D3 by extensive experimental evaluation, e.g., by checking 1,620 real-life models for NASA’s NextGen air traffic control system. Compared to checking each model-property pair individually, D3 is up to 9.4 × faster.

Comments

This is proceeding is published as Dureja R., Rozier K.Y. "More Scalable LTL Model Checking via Discovering Design-Space Dependencies (D3)." In: Beyer D., Huisman M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2018. Lecture Notes in Computer Science 10805 (2018): 309-327. DOI: 10.1007/978-3-319-89960-2_17. Posted with permission.

Description
Keywords
Citation
DOI
Copyright
Mon Jan 01 00:00:00 UTC 2018