Contracts - AWARD SUMMARY
CARNEGIE MELLON UNIVERSITY
The goal of the Verification and Validation of Flight-Critical Systems (VVFCS)
project is to develop verification and validation tools and algorithms for
complex flight critical systems. A flight critical system (FCS) is one that
directly controls the safe conduct of an aircraft’s flight. This includes air
and ground systems, and concepts of operation as well as technology.
Flight-critical system research includes human performance as a key factor.
In support of the software-intensive systems effort under VVFCS, the
contractor will develop compositional verification technology
for safety properties of FCS, which will allow NASA to perform verification
tasks that are currently beyond the state-of-the-art. Specifically, the contractor
shall develop algorithms for accomplishing the following:
1) Compositional verification: the project will use design information to
decompose verification into local component requirements that together
guarantee complex system-level properties. Such decomposition will be
used throughout the lifecycle to increase confidence in the FCS while
reducing verification costs.
2) Test-case generation: for components that involve complex mathematical
computations, the project will develop and customize advanced test-case
generation techniques in order to build test suites that achieve specified
coverage of the components.
The developed techniques will be combined into an integrated
framework for advanced verification of FCS. The framework will extend the award winning
JavaPathfinder (JPF) open source model checker developed
at NASA Ames (http://babelfish.arc.nasa.gov/trac/jpf/).
| AWARD OVERVIEW |
| Award Number |
NNA10DE60C |
Funding Agency |
National Aeronautics and Space Administration |
| Total Award Amount |
$556,476 |
Project Location - City |
Pittsburgh |
| Award Date |
08/26/2010 |
Project Location - State |
PA |
| Project Status |
Completed |
Project Location - Zip |
15213-3890
|
| Jobs Reported |
1.09 |
Congressional District |
14 |
| Project Location - Country |
US |
|
|
Recipient Information
(Contracts)
| Recipient Information (Contracts) |
|
Recipient Name
|
CARNEGIE MELLON UNIVERSITY |
| Recipient DUNS Number |
052184116
|
| Recipient Address |
5000 FORBES AVE |
| Recipient City |
PITTSBURGH |
| Recipient State |
Pennsylvania |
| Recipient Zip |
15213-3815 |
| Recipient Congressional District |
14 |
| Recipient Country |
USA |
Required to Report Top 5
Highly Compensated Officials |
No |
Projects and Jobs Information
| Projects and Jobs Information |
| Project Title |
Federal Contract |
| Project Status |
Completed |
| Final Project Report Submitted |
Yes |
| Project Activities Description |
Research and Development in the Physical, Engineering, and Life Sciences (except Biotechnology) |
| Quarterly Activities/Project Description |
We have significantly enhanced the JPF extension jpf-jdart. This is the concolic execution framework in JPF. We now support fields of classes that are either of basic types or arrays of basic types. We added support to call jdart within the same process space repeatedly to explore new paths. We made the interface to Yices more robust, enhanced jpf-jdart to be re-entrant and optimized it for speed. For this extension, ongoing work includes supporting bit-wise operators and variables that are class object references.
Towards an automated CV algorithm with automatic alphabet refinement, we designed an algorithm for interface generation with alphabet refinement. We dynamically generate programs in Java that implemented guarded methods. We then call sequences of these guarded methods programatically to answer queries and conjectures within the L* based learning framework. We have added two new JPF extensions for interface generation and CV. The first is called jpf-learn and encapsulates the L* learning algorithm. The second is called jpf-psyco and encapsulates the teacher to learn interface automata. The teacher will eventually be enhanced to support CV. At this point it does interface generation alone.
Given a method, a refined alphabet corresponding to that method consists of both the method and a guard on that method that restricts the space of inputs that the method will accept. The guard on a method can be thought of as an assumption. For automated alphabet refinement, we designed a novel algorithm that uses path constraints generated by jdart to partition the input space of methods and thus generate refined alphabet for learning, representing guarded methods.
We are testing our implementation at this point. The new extensions and the enhanced jpf-jdart reside on bitbucket.org. Once the testing is complete, we expect to move all extensions to babelfish. We prepared a paper based on our implementation. We propose to submit it to CAV. |
| Jobs Created |
1.09 |
| Description of Jobs Created |
A postdoctoral position has been created under this project.
The position involves performing research in compositional
verification and test-case generation techniques based
on model checking.The research is driven by flight-critical
software examples in order to develop solutions appropriate
for this domain. Therefore, the position requires an excellent
research record, with previous experience in formal verification
techniques and tools, in particular model checking.
In addition to making advances at the theoretical level, the
project has a strong practical component. Programming experience
in object oriented languages, capability to develop
and maintain software of several thousands of lines of code,
and the ability to approach and study large complex
software with potentially limited documentation are also
required skills.
The job created was filled by a professional with
previous industrial experience, returning to the job
market after a PhD program and entering a research
and development environment.
|
Purchaser Information
(Contracts)
| Purchaser Information |
| Contracting Office ID |
ARC00 |
| Contracting Office Name |
Not Available |
| Contracting Office Region |
Not Available |
| TAS Major Program |
80-0125 |
| Award Information |
| Award Date |
08/26/2010 |
| Award Number |
NNA10DE60C |
| Order Number |
|
| Award Type |
Contracts |
| Funding Agency ID |
80 |
| Funding Agency Name |
National Aeronautics and Space Administration |
| Funding Office Name |
Not Available |
| Awarding Agency ID |
80 |
| Awarding Agency Name |
National Aeronautics and Space Administration |
| Amount of Award |
$556,476 |
| Funds Invoiced/Received |
$556,476 |
| Expenditure Amount |
$0 |
| Infrastructure Expenditure Amount |
$0 |
| Infrastructure Purpose and Rationale |
Not Reported |
| Infrastructure Point of Contact Name |
Not Reported |
| Infrastructure Point of Contact Email |
Not Reported |
| Infrastructure Point of Contact Phone |
Not Reported |
| Infrastructure Point of Contact Address |
Not Reported |
| Infrastructure Point of Contact City |
Not Reported |
| Infrastructure Point of Contact State |
Not Reported |
| Infrastructure Point of Contact Zip |
Not Reported |
Product or Service Information
(Contracts)
| Product or Service Information |
| Primary Activity Code |
541712 |
| Activity Description |
Research and Development in the Physical, Engineering, and Life Sciences (except Biotechnology) |
| Sub-Awards Information |
| Sub-awards to Organizations |
0 |
| Sub-award Amounts to Organizations |
$0 |
| Sub-Awards to Individuals |
0 |
| Sub-Award Amounts to Individuals |
$0 |
| Number of Sub-awards less than $25,000/award |
0 |
| Amount of Sub-awards less than $25,000/award |
$0 |
| Number of payments to vendors greater than $25,000 |
0 |
| Total Amount of payments to vendors greater than $25,000/award |
$0 |
| Number of payments to vendors less than $25,000/award |
0 |
| Total Amount of payments to vendors less than $25,000/award |
$0 |
| Location Information |
| Latitude, Longitude |
40º 26' 40",
-79º 56' 34" |
| Congressional District |
14 |
| Address 1 |
5000 Forbes Ave |
| Address 2 |
|
| City |
Pittsburgh |
| County |
Allegheny |
| State |
PA |
| Zip |
15213-3890 |
|
|