| Mobility Capabilities and Requirements Study 2016 Accreditation Report. Volume 1: Summary |
Jul-2009 |
|
| Authors:
Jack Jackson; INSTITUTE FOR DEFENSE ANALYSES ALEXANDRIA VA
|
 | The effort described in this document is part of a proof of concept application of a new set of Validation, Verification, and Accreditation (VV&A) guidelines for analytic models and simulations developed for OSD/CAPE by the Institute of Defense Analyses. In concert with CAPE and building upon extensive information available through subject matter experts and the military, a set of eight criteria were developed and applied to all mobility and logistics ... |
|
| An Integrated Specification and Verification Environment for Component-Based Architectures of Large-Scale Distributed Systems |
26-May-2009 |
55 pages |
| Authors:
Torben Amtoft; Anindya Banerjee; John Hatcliff; KANSAS STATE UNIV MANHATTAN DEPT OF COMPUTING AND INFORMATION SCIENCES
|
 | The objectives of this project are to address challenges of constructing large-scale DoD software intensive systems by constructing an integrated modeling and specification framework that can support software product-line development based on widely-used component middleware frameworks that will likely form the basis of future DoD systems. This document provides the final performance report on this project. |
|
| Extracting Formal Models from Informal Requirements and Using Them for Validation |
Jan-2009 |
9 pages |
| Authors:
Insup Lee; PENNSYLVANIA UNIV PHILADELPHIA BOARD OF TRUSTEES
|
| The goal of the project is to study formalization of regulations and regulatory compliance. Technical objectives involve addressing two verification problems: 1. Consistency of regulation / Compliance can be achieved only if the regulation is internally consistent. This verification problem answers the question whether any organization is capable of complying with the regulation. 2. Compliance of organizations / This verification problem answers the question whether the operation of an organization ... |
|
| NORM: A Decentralized Location Verification Mechanism for Wireless Sensor Networks |
Dec-2008 |
8 pages |
| Authors:
Jie Yang; Yingying Chen; Xiuyuan Zheng; Venkataraman Swaminathan; STEVENS INST OF TECH HOBOKEN NJ DEPT OF ELECTRICAL ENGINEERING AND COMPUTER SCIENCE
|
| The location of wireless devices and sensor nodes is a critical input for many location-aware applications. Particularly, important tasks in tactical fields, such as monitoring the status of soldiers and tracking the equipment, all rely on the location information. However, adversaries may falsify the location information and undermine the activities supported by location. In this work, we propose NORM, a decentralized location verification mechanism for wireless sensor networks. To perform ... |
|
| Controls Over the Contractor Common Access Card Life Cycle |
10-Oct-2008 |
104 pages |
| Authors:
Paul J Granetto; Anthony M Torres; David M Staley; Thomas T Nguyen; Hanh T Nguyen; Michael D Durda; Dewayne J Jr; McOsker; Melinda M Oleksa; Carol N Gorman; Donald A Bloomer; Christopher S Groubert; OFFICE OF THE DEPUTY INSPECTOR GENERAL FOR AUDITING OF THE DEPARTMENT OF DEFENSE ARLINGTON VA
|
| The overall objective of this audit was to determine whether controls over Common Access Cards (CACs) provided to contractors were in place and worked as intended. Specifically, we determined whether DoD officials issued CACs to contractors, verified the continued need for contractors to possess CACs, and revoked and recovered CACs from contractors in accordance with DoD policies and procedures. |
|
| Demonstration of Helicopter Multi-Towed Array Detection System (MTADS) Magnetometry Technology at Pueblo Precision Bombing Range #2, Colorado |
28-Aug-2008 |
59 pages |
| Authors:
Jack Foley; David Wright; SKY RESEARCH ASHLAND OR
|
| The Pueblo Precision Bombing Range is located in Otero County, Colorado. This site is classified by the United States Government as a Formerly Used Defense Site (FUDS) and was a World War II-era military training facility. This demonstration utilized Helicopter Multi-Sensor Towed Array Detection System (MTADS) Magnetometry (HeliMag) technology, a wide area assessment technology. A data collection survey was conducted in September of 2005 and resulted in the survey of ... |
|
| OneSAF Objective System (OOS) Behavior Model Verification |
15-Aug-2008 |
108 pages |
| Authors:
Eric Tollefson; Michael S Martin; Andrew Fletcher; ARMY TRADOC ANALYSIS CENTER MONTEREY CA
|
| The Army's One Semi-Automated Forces (OneSAF) Objective System (OOS) is a composable, next-generation computer generated forces (CGF) that has been designed to represent a full range of operations, systems, and control processes from the entity level to brigade level. Its development has leveraged the ever-increasing computing power available today to represent highly-complex battlefield phenomena, particularly entity and unit behaviors. In the fall of 2005, the Product Manager (PM) OneSAF asked ... |
|
| Verification and Validation of DTRA's Unified EM Design (Briefing Charts) |
09-Apr-2008 |
13 pages |
| Authors:
Robert F Gray; DEFENSE THREAT REDUCTION AGENCY FORT BELVOIR VA
|
|
| Verification, Validation, and Accreditation (VV&A) of Federations (Verification, validation et accreditation (VV&A) des federations) |
01-Apr-2008 |
|
| Authors:
NATO RESEARCH AND TECHNOLOGY ORGANIZATION NEUILLY-SUR-SEINE (FRANCE)
|
|
| Applying Formal Methods to a Certifiably Secure Software System |
FEB 2008 |
18 pages |
| Authors:
Constance L. Heitmeyer; Myla M. Archer; Elizabeth I. Leonard; John D. McLean; NAVAL RESEARCH LAB WASHINGTON DC INFORMATION TECHNOLOGY DIV
|
| A major problem in verifying the security of code is that the code's large size makes it much too costly to verify in its entirety. This paper describes a novel and practical approach to verifying the security of code which substantially reduces the cost of verification. In this approach, a compact security model containing only information needed to reason about the security properties of interest is constructed and the security ... |
|
| Face Verification across Age Progression using Discriminative Methods |
Jan-2008 |
10 pages |
| Authors:
Haibin Ling; Stefano Soatto; Narayanan Ramanathan; David W Jacobs; TEMPLE UNIV PHILADELPHIA PA DEPT OF COMPUTER AND INFORMATION SCIENCES
|
| Face verification in the presence of age progression is an important problem that has not been widely addressed. In this paper, we study the problem by designing and evaluating discriminative approaches. These directly tackle verification tasks without explicit age modeling, which is a hard problem by itself. First, we find that the gradient orientation (GO), after discarding magnitude information, provides a simple but effective representation for this problem. This representation ... |
|
| Survey Results for the Development of the Academic Class Composite Tool for the Academic Instructors and Supervisors |
OCT 2007 |
39 pages |
| Authors:
Carita A. DeVilbiss; Valerie B. Rice; ARMY RESEARCH LAB ABERDEEN PROVING GROUND MD HUMAN RESEARCH AND ENGINEERING DIRECTORATE
|
| The ability to maintain unit readiness and mission effectiveness in the midst of the increasing demands of warfare ultimately depends on the performance of the Soldier. The retention and overall performance of Soldiers can be affected by a variety of personal, situational, and organizational factors, particularly in dynamic and stressful environments. Throughout the U.S. Army, following basic training, Soldiers are prepared for challenging Advanced Individual Training (AIT) programs. Although AIT ... |
|
| Formal Methods for Specifying, Validating, and Verifying Requirements |
28-May-2007 |
13 pages |
| Authors:
Constance L Heitmeyer; NAVAL RESEARCH LAB WASHINGTON DC INFORMATION TECHNOLOGY DIV
|
| This paper describes the specification, validation and verification of system and software requirements using the SCR tabular method and tools. An example is presented to illustrate the SCR tabular notation, and an overview of each of the ten tools in the SCR toolset is presented. |
|
| Modular Typestate Verification of Aliased Objects |
MAR 2007 |
51 pages |
| Authors:
Kevin Bierhoff; Jonathan Aldrich; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| A number of type systems have used typestates to specify and statically verify protocol compliance. Aliasing is a major challenge for these systems. This paper proposes a modular type system for a core object-oriented language that leverages linear logic for verifying compliance to more expressive protocol specifications than previously supported. The system improves reasoning about aliased objects by associating references with access permissions that systematically capture what aliases know about ... |
|
| Abstraction Techniques for Parameterized Verification |
NOV 2006 |
278 pages |
| Authors:
Muralidhar Talupur; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Model checking is a well known formal verification technique that has been particularly successful for finite state systems such as hardware systems. Model checking essentially works by a thorough exploration of the state space of a given system. As such, model checking is not directly applicable to systems with unbounded state spaces like parameterized systems. The standard approach for applying model checking to unbounded systems is to extract finite state ... |
|
| Environmental Technology Verification Coatings and Coating Equipment Program (ETV CCEP). High Transfer Efficiency Spray Equipment - Generic Verification Protocol (Revision 0) |
30 SEP 2006 |
59 pages |
| Authors:
Robert J. Fisher; CONCURRENT TECHNOLOGIES CORP JOHNSTOWN PA
|
| The Environmental Technology Verification (ETV) Program has been established by the U.S. Environmental Protection Agency (EPA) to verify the performance characteristics of innovative environmental technologies across all media and report this objective information to the states, buyers, and users of environmental technology; thus, accelerating the entrance of these new technologies into the marketplace. Verification organizations oversee and report verification activities based on testing and quality assurance protocols developed with input ... |
|
| Verification, Validation and Accreditation (VV&A) - Leveraging International Initiatives |
01 SEP 2006 |
|
| Authors:
A. J. Masys; M. L. van Emmerik; Pierre Bouc; DEPARTMENT OF NATIONAL DEFENCE OTTAWA (ONTARIO)
|
| With the advent of complex coupled systems and the evolutionary introduction of new technology, the application of Modelling and Simulation (M&S) activities has increased throughout industry, academia and military domains. M&S has flourished as an enabling technology facilitating effective training opportunities from procedural training to full mission rehearsal and has been instrumental in helping decision makers take better account of the complexity, dynamics and uncertainties that pervade modern warfare. The ... |
|
| Testing Template and Testing Concept of Operations for Speaker Authentication Technology |
SEP 2006 |
119 pages |
| Authors:
Marek M. Sipko; NAVAL POSTGRADUATE SCHOOL MONTEREY CA
|
| This thesis documents the findings of developing a generic testing template and supporting concept of operations for speaker verification technology as part of the Iraqi Enrollment via Voice Authentication Project (IEVAP). The IEVAP is an Office of the Secretary of Defense sponsored research project commissioned to study the feasibility of speaker verification technology in support of the Global War on Terrorism security requirements. The intent of this project is to ... |
|
| Estimating the Density of Blainville's Beaked Whale (Mesoplodon densirostris) in the Tongue of the Ocean (TOTO) Using Passive Acoustics |
Sep-2006 |
6 pages |
| Authors:
D Moretti; N DiMarzio; R Morrissey; J Ward; S Jarvis; NAVAL UNDERSEA WARFARE CENTER DIV NEWPORT RI
|
| Techniques to detect and localize marine mammals including Blainville's beaked whales (Mesoplodon densirostris) using the bottom-mounted hydrophones of the Atlantic Undersea Test and Evaluation Center have been developed. A series of verification tests using these passive acoustics techniques to determine the presence and position of vocalizing animals are being conducted. These acoustic 'sightings' are verified by a team of surface observers. Based on Woods Hole Oceanographic Institution tag data and ... |
|
| An Analysis of Specware and Its Usefulness in the Verification of High Assurance Systems |
JUN 2006 |
111 pages |
| Authors:
Daniel P. DeCloss; NAVAL POSTGRADUATE SCHOOL MONTEREY CA
|
| Formal verification is required for systems that require high assurance. Formal verification can require large and complex proofs that can drastically affect the development life cycle. Through the use of a verification system, such proofs can be managed and completed in an efficient manner. A verification system consists of a specification language that can express formal logic and an automated theorem tool that can be used to verify theorems and ... |
|
| Results of JAUS OPC Experiment 3.0 |
MAY 2006 |
11 pages |
| Authors:
M. N. Clark; Parag Batavia; Jeff Wit; HARRIS CORP MELBOURNE FL
|
| The primary objective of the OCU and Payload Committee (OPC) within the Joint Architecture for Unmanned Systems (JAUS) working group is to assess the JAUS Reference Architecture (RA) specification's ability to address interoperability. The OPC was tasked to evaluate new messages and protocols before accepting them into the RA. To accomplish these objectives, the OPC conducted several experiments for collection of information on current and recommended approaches. The latest experiment, ... |
|
| Verification of a Decision Level Fusion Algorithm Using a Proven ATR System and Measured SAR Data |
MAR 2006 |
80 pages |
| Authors:
James D. Thompson; AIR FORCE INST OF TECHNOLOGY WRIGHT-PATTERSON AFB OH GRADUATE SCHOOL OF ENGINEERING AND MANAGEMENT
|
| Decision level fusion (DLF) algorithms combine outputs of multiple single sensors to make one confident declaration of a target. This research compares performance results of a DLF algorithm using measured data and a proven ATR system with results from simulated data and a modeled ATR system. This comparison indicates that DLF offers significant performance improvements over single sensor looks. However, results based on simulated data and a modeled ATR are ... |
|
| Verifying HLA RTIs |
2006 |
10 pages |
| Authors:
Susan Symington; Joseph Kaplan; Frederick Kuhl; John Tufarolo; Richard Weatherly; Jeff Nielsen; MITRE CORP MCLEAN VA
|
| An RTI Verification Facility has been established by the Defense Modeling and Simulation Office (DMSO) to test the compliance of High Level Architecture (HLA) Run Time Infrastructure (RTI) implementations with the U.S DoD High Level Architecture Interface Specification, version 1.3. Using the custom-built "RTI Verifier" software, the Verification Facility has to date verified two RTI implementations from two different RTI developers. In this paper, we describe our experience with the ... |
|
| Real-Time Data Warehousing and On-Line Analytical Processing at Aberdeen Test Center's Distributed Center |
Dec-2005 |
38 pages |
| Authors:
Michael J Reil; Samuel F Harley; T G Bartlett; ABERDEEN TEST CENTER MD
|
| The purpose of the Aberdeen Test Center is to provide real-time test data verification, analysis and warehousing and to provide OLAP tools for test data analysis and data mining. |
|
| Lithium-Ion Life Expectancy Verification Guidelines for Transformational Communication Satellite System (TSAT) |
25 NOV 2005 |
12 pages |
| Authors:
W. H. Hwang; V. J. Ang; AEROSPACE CORP EL SEGUNDO CA LAB OPERATIONS
|
| Guidelines are provided for the Transformational Communication Satellite System (TSAT) mission relative to life expectancy verification of lithium-ion cells. Conditions and associated risks are presented to facilitate a decision to include or adopt the technology, or a decision to launch before there are sufficient data to conclusively verify life expectancy. |
|
| Verification of Single-Peptide Protein Identifications by the Application of Complementary Database Search Algorithms |
20 OCT 2005 |
29 pages |
| Authors:
James G. Rohrbough; Linda Breci; Nirav Merchant; Susan Miller; Paul A. Haynes; ARIZONA UNIV TUCSON DEPT OF BIOCHEMISTRY
|
| Protein identifications from complex biological mixtures often involve the application of tandem mass spectrometry techniques. One such technique, known as the Multi-Dimensional Protein Identification Technique, or MudPIT, involves the use of computer search algorithms that automate the process of identifying proteins present in the sample mixture based on mass spectrometry analysis. This technique involves digestion of the protein mixture with a protease such as trypsin, followed by liquid chromatography separation ... |
|
| Proof of Concept: Iraqi Enrollment via Voice Authentication Project |
SEP 2005 |
292 pages |
| Authors:
Samuel K. Lee; NAVAL POSTGRADUATE SCHOOL MONTEREY CA
|
| This thesis documents the findings of the Naval Postgraduate School (NPS) research team's efforts on the initial phase of the Iraqi Enrollment via Voice Authentication Project (IEVAP). The IEVAP is an Office of the Secretary of Defense sponsored research project commissioned to study the feasibility of speaker verification technology in support of the Global War on Terrorism security requirements. The intent of this project is to contribute toward the future ... |
|
| Ionospheric Modeling: Development, Verification and Validation |
SEP 2005 |
9 pages |
| Authors:
Patricia H. Doherty; BOSTON COLL CHESTNUT HILL MA INST FOR SCIENTIFIC RESEARCH
|
| Much of the work performed this year has been directly related to the validation of the Global Assimilation of Ionospheric Measurements (GAIM) model. Summaries of these efforts are in 26 reports available within the Air Force Research Laboratory (AFRL) on http://dd175/gaim/. Studies were also initiated to enhance the development of high-quality GPS data products and to validate the ability of the Special Sensor Ultraviolet Spectrographic Imager (SSUSI) onboard the Defense ... |
|
| Typed Regions |
31 AUG 2005 |
21 pages |
| Authors:
Stefan Monnier; Zhong Shao; YALE UNIV NEW HAVEN CT DEPT OF COMPUTER SCIENCE
|
| Standard type systems are not sufficiently expressive when applied to low-level memory-management code. Such code often uses some form of strong update (i.e. assignments that change the type of the affected location) and needs to reason about the relative position of objects in memory. We present a novel type system which, like alias types 20, provides a form of strong update, but with the advantage that it does not require ... |
|
| A Type System for Certified Binaries |
31 AUG 2005 |
47 pages |
| Authors:
Zhong Shao; Valery Trifonov; Bratin Saha; Nikolaos Papaspyrou; YALE UNIV NEW HAVEN CT DEPT OF COMPUTER SCIENCE
|
| A certified binary is a value together with a proof that the value satisfies a given specification. Existing compilers that generate certified code have focused on simple memory and control-flow safety rather than more advanced properties. In this paper, we present a general framework for explicitly representing complex propositions and proofs in typed intermediate and assembly languages. The new framework allows us to reason about certified programs that involve effects ... |
|
| Verification of Safety Properties for Concurrent Assembly Code |
31 AUG 2005 |
15 pages |
| Authors:
Dachuan Yu; Zhong Shao; YALE UNIV NEW HAVEN CT DEPT OF COMPUTER SCIENCE
|
| Concurrency, as a useful feature of many modern programming languages and systems, is generally hard to reason about. Although existing work has explored the verification of concurrent programs using high-level languages and calculi, the verification of concurrent assembly code remains an open problem, largely due to the lack of abstraction at a low-level. Nevertheless, it is sometimes necessary to reason about assembly code or machine executables so as to achieve ... |
|
| Verification and Validation Report: Frequency Selective Surface Simulation Tool |
01-Jun-2005 |
74 pages |
| Authors:
T Q Ho; C A Hewett; D A Zolnick; M Kragalott; D J Taylor; M C Baugher; A K Agrawal; SPACE AND NAVAL WARFARE SYSTEMS CENTER SAN DIEGO CA
|
| To address the shortfall in M&S software capabilities for modeling radomes of various types, PEO-DD(X)/PMS-500 commissioned the development of a plan to satisfy these needs. FSS M&S was identified as one of the most promising FSS simulation approaches, and was selected for further development. This report presents a summary of the verification and validation of the enhanced FSS M&S code over a wide range of electromagnetic test cases, including infinite ... |
|
| Web-Based Dissemination System for the Trusted Computing Exemplar Project |
JUN 2005 |
152 pages |
| Authors:
Douglas R. Kane Jr; NAVAL POSTGRADUATE SCHOOL MONTEREY CA
|
| Open dissemination of the Trusted Computing Exemplar (TCX) project is needed. This dissemination must include methods to provide secure web access to project material, integrity verification of data, and group-based access controls. Because previously developed dissemination systems do not meet these requirements, a hybrid web-based dissemination system is necessary. The development of the TCX Dissemination System requirements involved the analysis of assumptions, threats, policies, and security objectives for the system ... |
|
| Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog |
JUN 2005 |
7 pages |
| Authors:
Himanshu Jain; Natasha Sharygina; Daniel Kroening; Edmund Clarke; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Model checking techniques applied to large industrial circuits suffer from the state space explosion problem. A major technique to address this problem is abstraction. The most commonly used abstraction technique for hardware verification is localization reduction, which removes latches that are not relevant to the property. However, localization reduction fails to reduce the size of the model if the property actually depends on most of the latches. This paper proposes ... |
|
| Verification and Planning for Stochastic Processes with Asynchronous Events |
JAN 2005 |
223 pages |
| Authors:
Hakan L. Younes; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Asynchronous stochastic systems are abundant in the real world. Examples include queuing systems, telephone exchanges, and computer networks. Yet, little attention has been given to such systems in the model checking and planning literature, at least not without making limiting and often unrealistic assumptions regarding the dynamics of the systems. The most common assumption is that of history-independence: the Markov assumption. In this thesis, the author considers the problems of ... |
|
| Tools for Constructing Requirements Specification: The SCR Toolset at the Age of Ten |
JAN 2005 |
18 pages |
| Authors:
Constance Heitmeyer; Myla Archer; Ramesh Bharadwaj; Ralph Jeffords; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| While human effort is critical to creating requirements specifications and human inspection can detect many specification errors, software tools find errors inspections miss and also find certain classes of errors more cheaply. This paper describes a set of tools for constructing and analyzing requirements specifications in the SCR (Software Cost Reduction) tabular notation. The tools include a specification editor, a consistency checker, a simulator, and tools for verifying application properties ... |
|
| Enhancing P3P Framework through Policies and Trust |
2005 |
16 pages |
| Authors:
Pranam Kolari; Li Ding; Lalana Kagal; Shashidhara G. Anupam Joshi; Tim Finin; MARYLAND UNIV BALTIMORE COUNTY BALTIMORE MD
|
| The Platform for Privacy Preferences (P3P) is a W3C standard that web sites can use to describe their privacy practices. The presence of P3P policies enables users to configure web browsers to constrain what they can and cannot do when visiting web sites. It's a good idea that unfortunately is rarely used. The authors identify two reasons for this: (i) the languages available to define a user's privacy preferences are ... |
|
| Concurrency and Complexity in Verifying Dynamic Adaptation: A Case Study |
2005 |
16 pages |
| Authors:
Karun N. Biyani; Sandeep S. Kulkarni; MICHIGAN STATE UNIV EAST LANSING DEPT OF ELECTRICAL AND COMPUTER ENGINEERING
|
| Software systems need to adapt as requirements change, environment conditions vary, and bugs are discovered and fixed. In systems that need to provide continuous operation, it is important that the adaptation be done with minimal interruption in the execution of the system. In context of verification of these adaptive systems, the verification needs to be done for the system before adaptation, for the system during adaptation, and for the system ... |
|
| Test Specification for the Alternate Repair Verification Process of the Finnish Air Force Digital Memory Unit Writer |
30 SEP 2004 |
11 pages |
| Authors:
Michael E. Trenchard; Lancelot Riedlinger; NAVAL RESEARCH LAB STENNIS SPACE CENTER MS MAPPING CHARTING AND GEODESY BRANCH
|
| The Digital Memory Unit Writer (DMU) is a ruggedized optical drive assembly built by Honeywell. The DMU writer is used specifically to write specially formatted map data to militarized Aircraft Optical Disks (AOD) for use in the AN/ASQ-l96 Digital Map System (consisting of both a Digital Map Computer and a DMU reader) of both U.S. and ally AV-8B Harrier and F/A-18 Hornet aircraft. The AN/ASQ-196 and its support equipment (including ... |
|
| "Black-Box" Probabilistic Verification |
SEP 2004 |
18 pages |
| Authors:
Hakan L. Younes; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The authors explore the concept of a "black-box" stochastic system, and propose an algorithm for verifying probabilistic properties of such systems based on very weak assumptions regarding system dynamics. The properties are expressed using a variation of PCTL, the Probabilistic Computation Tree Logic. They present a general model of stochastic discrete event systems that encompasses both discrete-time and continuous-time processes, and also provide a semantics for PCTL interpreted over this ... |
|
| Simulation and Real-Time Verification of Video Algorithms on the TI c6400 Using Simulink |
20 AUG 2004 |
24 pages |
| Authors:
Donald P. Orofino; MATH WORKS INC NATICK MA
|
| This talk will show how the use of system-level design tools, such as MATLAB and Simulink, can greatly enhance an engineer's ability to quickly and effectively translate product-level and algorithm-level specifications into a working TI DSP-based prototype for the consumer electronics market. Specifically, we will show how to efficiently target typical video processing algorithms, with the high bandwidth and algorithmic efficiency they require, to the TI C6400 platform, and the ... |
|
| Reusable PVS Proof Strategies for Proving Abstraction Properties of I/O Automata |
04 JUL 2004 |
15 pages |
| Authors:
Sayan Mitra; Myla Archer; MASSACHUSETTS INST OF TECH CAMBRIDGE ARTIFICIAL INTELLIGENCE LAB
|
| Recent modifications to PVS Support a new technique for defining abstraction properties relating automata in a clean and uniform way. This definition technique employs specification templates that can support development of generic high level PVS strategies that set up the standard subgoals of these abstraction proofs and then execute the standard initial proof steps for these subgoals. In this paper, we describe an abstraction specification technique and associated abstraction proof ... |
|
| A Proposed Standardization of the Navy VV&A Process Through the Application of VVML & the VDT |
Jan-2004 |
10 pages |
| Authors:
David H Broyles; Jennifer Park; Greg Quedenfeld; SPACE AND NAVAL WARFARE SYSTEMS CENTER NORTH CHARLESTON SC
|
| As in the commercial world, modeling and simulation (M&S) is increasingly pervasive throughout the Navy. There is a constant drive to expand the utility of these M&S through distributed M&S, federations, and other combinatorial simulations in the High Level Architecture (HLA), FORCEnet, and other such programs. The DOD and commercial sectors' increased reliance on M&S has necessitated a method to provide documented proof of M&S' credibility. Although the Navy has ... |
|
| Verification of an Autonomous Reliable Wingman Using CCL |
2004 |
9 pages |
| Authors:
Stephen Waydo; Eric Klavins; CALIFORNIA INST OF TECH PASADENA CONTROL AND DYNAMICAL SYSTEMS
|
| We present a system of two aircraft, one human piloted and one autonomous, that must coordinate to achieve tasks. The vehicles communicate over two data channels, one high rate link for state data transfer and one low rate link for command messages. We analyze the operation of the system when the high rate link fails and the aircraft must use the low rate link to execute a safe lost wingman ... |
|
| Towards a Hierarchy of Cryptographic Protocol Models |
30 OCT 2003 |
3 pages |
| Authors:
Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| Recently there has been an increasing amount of research on the introduction of cryptographic ideas into discrete methods for cryptographic protocol analysis. This is often done by developing a discrete model and a cryptographic model such that the discrete model can be shown sound with respect to the cryptographic model. In this position paper, the author presents a brief outline of a strategy for rendering the analysis of cryptographic protocols ... |
|
| Session 4: LCCA, Measuring and Verification. Cost Effective M&V for the Department of Defense |
07 OCT 2003 |
30 pages |
| Authors:
Charles Culp; Jeff Haberl; David Claridge; W. D. Turner; TEXAS A AND M UNIV COLLEGE STATION
|
| M&V History: (1) In the past, most USAF ESCO contracts were stipulated. This means that the USAF installation agreed that the savings were met for the 20+ year contract at the time of contract signing. The USAF then assumed all risk for achieving savings. Finding many problems with accuracy of guarantees. If savings were not met, no budget existed to make up short-fall. (2) Projects in the DoD today are ... |
|
| Validation & Verification of Intelligent and Adaptive Control Systems |
OCT 2003 |
12 pages |
| Authors:
James M. Buffington; Vince Crum; Bruce Krogh; Clinton Plaisted; Ravi Prasanth; LOCKHEED MARTIN AERONAUTICS CO FORT WORTH TX
|
| Emerging military aerospace system operational goals, such as autonomy, will require advanced safety-critical control systems consisting of unconventional requirements, system architectures, software algorithms, and hardware implementations. These emerging control systems will significantly challenge current verification and validation (V&V) processes, tools, and methods for flight certification. Ultimately, transition of advanced control systems that enable transformational military operations will be decided by affordable V&V strategies that reduce costs and compress schedules for ... |
|
| Analytical Support in Aircraft Certification |
27 AUG 2003 |
10 pages |
| Authors:
Jakub Kaczkowski; Wojciech Potkanski; INSTITUTE OF AVIATION WARSAW (POLAND)
|
| The high cost of designing a new airplane enforced engineers to look for new cheaper methods. One method for the cost reduction is wide use of computer simulations in designing and certification process. From many different methods of analysis, FEM appears to be the best, but in spite of all improvements, present level of fidelity is still too low to completely eliminate experiments in the designing process. This explains why ... |
|
| Comparing Techniques for Proving Unsatisfiability |
11 JUN 2003 |
3 pages |
| Authors:
Olga Tveretina; Hans Zantema; TECHNICAL UNIV OF EINDHOVEN (NETHERLANDS) DEPT OF COMPUTER SCIENCE
|
| We compare two standard techniques for satisfiability (SAT), which are basic for verification of microprocessor systems. We propose an approach for construction of shorter resolution refutations based on a standard approach called DPLL. |
|
| Convergence Testing in Term-Level Bounded Model Checking |
JUN 2003 |
22 pages |
| Authors:
Randal E. Bryant; Shuvendu K. Lahiri; Sanjit A. Seshia; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We consider the problem of bounded model checking of systems expressed in a decidable fragment of first-order logic. While model checking is not guaranteed to terminate for an arbitrary system, it converges for many practical examples, including pipelined processors. We give a new formal definition of convergence that generalizes previously stated criteria. We also give a sound semi-decision procedure to check this criterion based on a translation to quantified separation ... |
|
Reports by Keyword(s)
*VERIFICATION
