# Presentation: 519048

## Practical Model Checking to Enforce Domain-Specific Interfaces and Requirements

- NASA OSMA SAS '04

***SAIC***			Mike Beims (Michael.A.Beims@ivv.nasa.gov) ***GrammaTech***Mark Zarins (mzarins@grammatech.com)David Melski (melski@grammatech.com)David Chandler (chandler@grammatech.com)

## Problem

- Verifying that software adheres to interface requirements is tedious, time consuming, and error prone
- Analysts need to check:
- Use of project-specific interfaces
- Use of APIs to commercial-off-the-shelf (COTS) components (e.g., VxWorks)
- Current Approach
- Analysis is done manually with tools that ease the tracing of code from unit to unit
- Experience shows ~80K of code takes weeks to analyze in an IV&V setting

## Approach

- Automate the examination of many interface requirements using model-checking technology that works directly on the source code
- Model-checking system
- Built on GrammaTech’s CodeSurfer static-analysis platform
- Operates on the program’s interprocedural control-flow graph
- Based on weighted pushdown systems
- Fidelity is not 100%, but technology is scalable to real projects
- IV&V experience suggests that this is a reasonable trade-off
- Examines one thread at a time, but still catches many concurrency-related bugs
- Many concurrency-related bugs are caused by the failure to adhere consistently to coding requirements
- Already implemented for C (and most of C++)

## Key Organizations and People

- IV&V Facility

- Ken McGill
- Research Lead

- Mike Beims
- Principal Investigator (PI)

- Jerry Sims
- NASA PM

- Raju Raymond
- Code S COTR

- SAICPrime Contractor

- GrammaTechSubcontractor

- David Melski, Mark Zarins, David Chandler

- Supplies NASA with relevant problems and evaluates solutions

- Supplies Model Checking technology and Code Surfer Scripting expertise

## Importance and Benefits

- Benefits
- Potential to significantly reduce the amount of labor needed to inspect the implementation of some requirements compared to current IV&V inspection methodology
- Better inspection coverage and/or reduced cost
- Projects likely to realize benefits
- Mission-critical software projects where source code interface requirements have been formally defined (e.g., Principal Investigator Mode missions)
- Significant part of the effort is focused on transitioning approach to NASA IV&V center to ensure that benefits are realized by a broad base of IV&V practitioners.

## Relevance to NASA

- Many NASA interface requirements can be verified easily using push-down model checking
- Examples
- Proper use of COTS operating system calls
- Calls to operating system functions can be dangerous in certain contexts; queries can flag dangerous usage
- Proper sequencing of events within a single thread
- Queries can check that all required steps are done in the proper order
- Proper synchronization
- Queries can identify improper use of synchronization, which is common, serious, and difficult to debug
- Proper use of hardware
- Queries can ensure that all required hardware commands are issued in the correct order

## Accomplishments

- Selected project (CM1) and set it up on CodeSurfer
- Studied requirements, including VxWorks interface/API
- Identified and implemented 13 queries
- Ran queries and reviewed results
- Results of most queries consistent with a correct implementation
- However, four potential issues were discovered
- Further investigation is needed to determine if these are real problems
- We are in contact with the development team and in the process of investigating these potential issues in more depth

## Next Steps

- Year 1
- Investigate potential issues discovered by queries in more depth
- Refine approach/tool based on feedback from NASA IV&V and the development team
- Explore the implementation of more queries
- Year 2
- Explore options for additional candidate projects
- Identify and run challenge queries
- New project-specific queries
- VxWorks queries
- Refine approach/tool based on feedback from NASA IV&V and development team
- Year 3
- Abstract queries to easily support new projects
- Develop plan to transition the approach to IV&V practitioners
- Train IV&V practitioners
- Support practitioners on projects