| Topological Patterns for Scalable Representation and Analysis of Dataflow Graphs |
Nov 2011 |
24 pages |
| Authors:
Nimish Sane; Hojin Kee; Gunasekaran Seetharaman; Shuvra S Bhattacharyya; MARYLAND UNIV COLLEGE PARK INST FOR ADVANCED COMPUTER STUDIES
|
 | Tools for designing signal processing systems with their semantic foundation in dataflow modeling often use high-level graphical user interfaces (GUIs) or text based languages that allow specifying applications as directed graphs. Such graphical representations serve as an initial reference point for further analysis and optimizations that lead to platform-specific implementations. For large-scale applications the underlying graphs often consist of smaller substructures that repeat multiple times. To enable more concise representation ... |
|
| Simulating the Detachment of Leading Edge Vortices on Drosophila Melanogaster Using CFD |
13 Sep 2010 |
7 pages |
| Authors:
Alex Sabbatini; Gabriel Smith; Jeffrey S Pulskamp; Ronald G Polcawich; STANFORD UNIV CA DEPT OF MECHANICAL ENGINEERING
|
| Initial CFD simulations of quasi-steady hovering flight of the Drosophila sp. have studied the effects of delayed rotation of the wings at the end of each stroke and it s effect on the resulting unsteady aerodynamic forces found throughout the wing [8]. Further studies were carried out using the same CFD model as before to determine the lift and power requirements for Drosophila Virilis [7]. To verify the validity of ... |
|
| Adapting the Dynamic Allocation of Fires and Sensors (DAFS) Model for Use in Maritime Combat Analysis |
MAR 2008 |
143 pages |
| Authors:
Scott B. Hattaway; NAVAL POSTGRADUATE SCHOOL MONTEREY CA
|
| The U.S. Navy employs several models of maritime combat to provide analytical rigor to force structure and weapon system procurement policies. All of the models currently used are high resolution and deterministic, providing very detailed results but without any measurement of variance or any statistical manner of evaluating risk. This thesis provides the initial groundwork for a low resolution stochastic maritime combat model that may provide an initial evaluation and ... |
|
| Spatial Hearing, Attention and Informational Masking in Speech Identification |
28 FEB 2008 |
7 pages |
| Authors:
Jr. Kidd Gerald; Nathaniel Durlach; Douglas Brungart; TRUSTEES OF BOSTON UNIV MA
|
| The specific aims of this research grant included examining how and how well listeners could treat the two ears as independent channels, the role of a priori knowledge in multisource listening, and the evaluation of the Listener Max-Min observer models in multiple talker environments (Durlach et al., J. Acoust. Soc. Am., 2003). The general approach was empirical using humans subjects as observers in masked speech identification experiments when multiple sources ... |
|
| Reconfigurable Computing: Experiences and Methodologies |
JAN 2008 |
34 pages |
| Authors:
Song-Jun Park; Dale Shires; Brian Henz; ARMY RESEARCH LAB ABERDEEN PROVING GROUND MD COMPUTATIONAL AND INFORMATION SCIENCES DIR
|
| Reconfigurable computing refers to computations done with flexible fabrics where the data path and control flow can be customized to the application. Unlike traditional computing using the fetch, execute, and store model that is highly sequential, reconfigurable computing allows developers to program their applications both spatially and temporally. This allows for potentially great speed-ups with applications that might be well-suited for such approaches. However, programming in this style requires specialized ... |
|
| Using Mitrion-C to Implement Floating-Point Arithmetic on a Cray XD1 Supercomputer |
2008 |
6 pages |
| Authors:
Kevin K. Liu; Charles B. Cameron; Antal A. Sarkady; NAVAL ACADEMY ANNAPOLIS MD ELECTRICAL AND COMPUTER ENGINEERING
|
| Field-Programmable Gate Arrays (FPGAs) are of interest to the high performance computing (HPC) computing community because they offer lower power consumption and higher throughput compared to traditional processors. Recently, the implementation of floating-point operations on FPGAs has become possible as the amount of memory available on FGPAs has increased. Unfortunately, advances in technology have also increased the complexity of creating hardware designs for FPGAs. In this project, we describe our ... |
|
| Rapid Prototyping of Robotic Systems |
JUN 2007 |
251 pages |
| Authors:
William J. Smuda; NAVAL POSTGRADUATE SCHOOL MONTEREY CA DEPT OF COMPUTER SCIENCE
|
| This effort describes a systems engineering approach to the design and implementation of software for prototyping robotic systems. Developing networked robotic systems of diverse physical assets is a continuing challenge to developers. Problems often multiply when adding new hardware/software artifacts or when reconfiguring existing systems. This work describes a method to create model-based, graphical domain-specific languages. Domain-specific languages use terms understandable to domain engineers as well as abstract software engineering ... |
|
| 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. |
|
| Prescription Based Maintenance Management System |
Jan-2007 |
16 pages |
| Authors:
Thomas Galie; G S Valentine; John Scharschan; IMPACT TECHNOLOGIES LLC ROCHESTER NY
|
| In recent years, significant focus has been placed on the development and implementation of advanced prognostic and health management (PHM) technologies in military and industrial applications. The term PHM encompasses anomaly, diagnostic and prognostic algorithms as well as higher level reasoning algorithms for isolating root causes of faults/failures and directing optimal operational or maintenance actions. In such systems, two current deficiencies exist. First, for a variety of reasons, component and ... |
|
| Ocean Dynamics from Float Pairs |
18 OCT 2006 |
5 pages |
| Authors:
Andrew F. Bennett; OREGON STATE UNIV CORVALLIS COLL OF OCEANIC AND ATMOSPHERIC SCIENCES
|
| Regularly-spaced Eulerian arrays of current meters are becoming rare, while logarithmic arrays are all but unknown. A global subsurface ocean observing system is only a vision at this time. Subsurface floats are increasingly being deployed, albeit sparingly, in many ocean current systems. It is therefore imperative to be able to make dynamically sound estimates of current shears and pressure gradients from float data. It is obvious that a pair of ... |
|
| Analyzing Memory Accesses in x86 Executables |
2006 |
19 pages |
| Authors:
Gogul Balakrishnan; Thomas Reps; WISCONSIN UNIV-MADISON DEPT OF COMPUTER SCIENCES
|
| This paper concerns static-analysis algorithms for analyzing x86 executables. The aim of the work is to recover intermediate representations that are similar to those that can be created for a program written in a high-level language. Our goal is to perform this task for programs such as plugins, mobile code, worms, and virus-infected code. For such programs, symbol-table and debugging information is either entirely absent, or cannot be relied upon ... |
|
| Reusable and Extensible High Level Data Distributions |
28 SEP 2005 |
11 pages |
| Authors:
Roxana E. Diaconescu; Bradford Chamberlain; Mark L. James; Hans P. Zima; CALIFORNIA INST OF TECH PASADENA CENTER FOR ADVANCED COMPUTING RESEARCH
|
| This paper presents a reusable design of a data distribution framework for data parallel high performance applications. Distributions are a means to express locality in systems composed of large numbers of processor and memory components connected by a network. Since distributions have a great effect on the performance of applications, it is important that the distribution strategy is flexible, so its behavior can change depending on the needs of the ... |
|
| The Impact of SOA Policy-Based Computing on C2 Interoperation and Computing |
JUN 2005 |
44 pages |
| Authors:
Raymond Paul; W. T. Tsai; Jay Bayne; OFFICE OF THE SECRETARY OF DEFENSE WASHINGTON DC
|
| DoD is moving into GIG-based service-oriented network-centric policy-based enterprise computing. Specifically, network-centric operation means that each C2 system must be network ready, and must be able to interconnect and interoperate with other C2 systems. This paper presents issues related to policy-based computing in a service-oriented architecture (SOA) for network-centric warfare. Service-oriented computing and its associated architecture represent a new paradigm of computing and numerous issues need to be addressed. One ... |
|
| Herbal Tutorial |
09 MAY 2005 |
42 pages |
| Authors:
Mark A. Cohen; Frank E. Ritter; PENNSYLVANIA STATE UNIV UNIVERSITY PARK SCHOOL OF INFORMATION SCIENCES AND TECHNOLOGY
|
| To accommodate this wide range of users, and to promote the use of cognitive systems, it is essential that tools such as high-level languages and development environments are created to allow the modeler to focus more on the problem domain, and less on the nuances of a particular architecture. This tutorial introduces an integrated development environment and high-level behavior representation language called Herbal that represents a step towards creating tools ... |
|
| Uniframe: A Unified Framework for Developing Service-Oriented, Component-Based Distributed Software Systems |
Jan-2005 |
21 pages |
| Authors:
Rajeev R Raje; Andrew M Olson; Barrett R Bryant; Carol C Burt; Makhail Auguston; INDIANA UNIV-PURDUE UNIV AT INDIANAPOLIS
|
| This chapter introduces the UniFrame approach to creating high quality computing systems from heterogeneous components distributed over a network. It describes how this approach employs a unifying framework for specifying such systems to unite the concepts of service-oriented architectures, a component-based software engineering methodology and a mechanism for automatically finding components on a network in order to assemble a specified system. UniFrame employs a formal specification language to define the ... |
|
| Building Software Tools for Combat Modeling and Analysis |
DEC 2004 |
201 pages |
| Authors:
Chen Yuanxin; NAVAL POSTGRADUATE SCHOOL MONTEREY CA
|
| The focus of this thesis is to use and leverage the strengths of dynamic computer program analysis methodologies in software engineering testing and debugging such as program behavior modeling and event grammars to automate the building and analysis of combat simulations. An original high level language METALS (Meta-Language for Combat Simulations) and its associated parser and C++ code generator were designed to reduce the amount of time and developmental efforts ... |
|
| Scalable Trust of Next-Generation Management (STRONGMAN) |
OCT 2004 |
39 pages |
| Authors:
Jonathan M. Smith; PENNSYLVANIA UNIV PHILADELPHIA PA RESEARCH SERVICES
|
| STRONGMAN focused on advanced boundary controls and risk management with the key goal of increasing automation of the management of boundary controllers such as gateways and firewalls, in the Internet. Automated management would translate high-level security policy into actions which support that policy at every rele |
|
| Simulating Clouds with Procedural Texturing Techniques Using the GPU |
SEP 2004 |
69 pages |
| Authors:
Georgios E. Tarantilis; NAVAL POSTGRADUATE SCHOOL MONTEREY CA
|
| Many 3D training simulations employ static, and to some extent, simplistic natural phenomena representation that often leaves much to be desired. Taking advantage of the latest advancements in computer graphics hardware allows modeling dynamic natural phenomena such as clouds. Specifically, utilizing procedural techniques and high-level shading languages, it is possible to produce considerably more realistic simulations. This thesis designed and implemented a visual simulation component, which renders convincing clouds using ... |
|
| An Analysis of the Feasibility and Applicability of IEEE 802.x Wireless Mesh Networks within the Global Information Grid |
SEP 2004 |
115 pages |
| Authors:
Eric J. Bach; Mark G. Fickel; NAVAL POSTGRADUATE SCHOOL MONTEREY CA
|
| This thesis analyzes the feasibility, functionality, efficacy and usability of IEEE 802.x wireless mesh networks in multiple DoD contexts. Through multiple field and lab experiments and hardware investigations, an assessment is performed on the realistic implementation issues of wireless mesh networks and their possible applications. A detailed examination is conducted of the variable elements, operational constraints, and possible decision points for developing a usable, robust, self-organizing, wireless mesh network that ... |
|
| High Performance Embedded Computing Software Initiative (HPEC-SI) |
20 AUG 2004 |
|
| Authors:
Jeremy Kepner; MASSACHUSETTS INST OF TECH LEXINGTON LINCOLN LAB
|
 | The High Performance Embedded Computing Software Initiative is addressing the military's need to advance the state of embedded software development tools, libraries, and methodologies to retain the nation's military technology advantage in increasingly software-based systems. Key accomplishments include the completion of the first demonstration and the development of the Parallel VSIPL++ standard. Currently, the HPEC-SI effort is on track towards its goal of changing the state-of-the-practice in programming DoD HPEC ... |
|
| A High-Level Symbolic Representation for Intelligent Agents Across Multiple Architectures |
JUL 2004 |
186 pages |
| Authors:
Jacob Crossman; Robert Wray; Paul Nielson; Randolph M. Jones; Al Wallace; Christian Lebiere; AIR FORCE RESEARCH LAB WRIGHT-PATTERSON AFB OH HUMAN EFFECTIVENESS DIRECTORATE
|
| This report describes the High-bevel Symbolic Representation (HLSR) project for the U.S. Air Force PRDA 03-01-HE: Human Performance in Modeling and Simulation, Technical Area 2: Opposing Force Behaviors. This report summarizes the work done on Defense Modeling Simulation contract F33615-03-C-6343 to develop a high level symbolic representation (HLSR) for behavior modeling. This effort seeks to increase development efficiency and reuse in behavior modeling. The report describes the development of a ... |
|
| Heterogeneous Embedded Real-Time Systems Environment |
DEC 2003 |
74 pages |
| Authors:
Cosmo Castellano; James Graham; INTEGRATED SENSORS INC UTICA NY
|
| The primary objective of the H-RTExpress effort is to provide enabling technology and domain specific tools that will quickly and effectively move systems targeted for heterogeneous architectures containing adaptive and embedded computing nodes from concept to implementation. The approach to accomplishing this objective is to build an integrated graphical development environment that will provide the capability to allow direct mapping and execution of sequential MATLAB code into heterogeneous embedded parallel ... |
|
| Software Defined Radio Datalink Implementation Using PC-Type Computers |
SEP 2003 |
211 pages |
| Authors:
Georgios Zafeiropoulos; NAVAL POSTGRADUATE SCHOOL MONTEREY CA
|
| The objective of this thesis was to examine the feasibility of implementation and the performance of a Software Defined Radio datalink, using a common PC type host computer and a high level programming language. Dedicated transceivers were used, plugged on the PCI bus of host PCs running Windows 2000. Most of the functionality was programmed using the Microsoft Visual C++ language. The tasks to be performed included the channels configuration ... |
|
| Design Tools for Integrated Asynchronous Electronic Circuits |
19 JUN 2003 |
17 pages |
| Authors:
Alain J. Martin; Mika Nystroem; Catherine G. Wong; SITUS LOGIC PASADENA CA
|
| The objective of this Phase-I study was to demonstrate the feasibility of a suite of industrial CAD tools for the design of high- performance, energy-efficient, asynchronous VLSI circuits based on the Caltech technology. Situs Logic's general strategy in the EDA-tools market is to develop and commercialize a complete suite of CAD tools for the design of asynchronous, QDI, VLSI systems including synthesis, analysis, simulation, verification, at the logical and physical ... |
|
| A Generative and Model Driven Framework for Automated Software Product Generation |
01-May-2003 |
7 pages |
| Authors:
Wei Zhao; Mikhail Auguston; Barrett R Bryant; Carol C Burt; Rajeev R Raje; Andrew M Olson; Jeffrey G Gray; ALABAMA UNIV IN BIRMINGHAM DEPT OF COMPUTER AND INFORMATION SCIENCES
|
| Component-based Software Engineering (CBSE) and related technologies have demonstrated their strength in recent years by increasing development productivity and parts reuse. Recently, the Model Driven Architecture (MDA) has raised the abstraction level of programming languages to modeling languages that can be compiled by downward model transformations. Correspondingly, the goal of Generative Programming (GP) is to automate concrete software product generation from a domain-specification and reusable components. This paper describes the ... |
|
| Interoperability and a Standard Joint Logistics Data Exchange with the Department of Defense |
07 APR 2003 |
35 pages |
| Authors:
Edward L. Kirkpatrick; ARMY WAR COLL CARLISLE BARRACKS PA
|
| As the Department of Defense (DoD) continues to transform into a more efficient and coordinated fighting force, the elements of logistics support will continue to become more complex and will require more efficient ways of communication. The component Services currently have a myriad of logistics systems available to support their individual Service members. Many of these systems are not interoperable even within the same Service. The DoD has initiated the ... |
|
| An Event-Trace Language for Software Decoys |
SEP 2002 |
|
| Authors:
Georgios Fragkos; NAVAL POSTGRADUATE SCHOOL MONTEREY CA
|
| Cyberspace is becoming the battlespace of the future, and military practices, like deception, seem to be suitable for defending information systems from attacks, In this thesis, we explore the concept of intelligent software decoys, which employ a form of software-based military deception. We developed a prototype of a high-level language for specifying intelligent software decoys. Our approach involves two stages. The specification language is intended to be part of a ... |
|
| Taskable Reactive Agent Communities |
AUG 2002 |
56 pages |
| Authors:
Karen L. Myers; David L. Martin; David N. Morley; SRI INTERNATIONAL MENLO PARK CA
|
| The focus of Taskable Reactive Agent Communities (TRAC) project was to develop mixed-initiative technology to enable humans to supervise and manage teams of agents as they perform tasks in dynamic environments. TRAC technology would enable users to task agent communities in a high-level language that provides both descriptions of goals to be satisfied and boundaries on agent behavior. The TRAC approach can be viewed as providing a form of high-level ... |
|
| A MATLAB Compilation Environment for Adaptive Computing Systems |
JUN 2002 |
20 pages |
| Authors:
Prithviraj Banerjee; NORTHWESTERN UNIV EVANSTON IL
|
| This report provides a brief summary of the research and development of a compiler for a mix of general purpose processors and adaptive computing processors from MATLAB. It incorporates a list of publications resulting from this research. |
|
| NATO HLA Certification |
JUN 2002 |
|
| Authors:
Jean-Louis Igarza; Pascal Cantot; Mark Crooks; Hans-Peter Menzler; Andrzej Najgebauer; NATO RESEARCH AND TECHNOLOGY ORGANIZATION NEUILLY-SUR-SEINE (FRANCE)
|
| The Report from the NATO Modelling and Simulation Steering Group approved by the North Atlantic Council establishes the need for a common (open standard) technical framework (CTF) to promote the interoperability and reuse of models and simulations across the Alliance. MSMP Sub-objective 1.1, "Adopt the High Level Architecture (HLA) as the NATO standard technical architecture for simulation applications," provides the best available technical architecture to satisfy this need. HLA is ... |
|
| A COTS-Based Replacement Strategy for Aging Avionics Computers |
01-Dec-2001 |
5 pages |
| Authors:
Jahn A Luke; Douglas G Haldeman; William J Cannon; AIR FORCE RESEARCH LAB WRIGHT-PATTERSON AFB OH EMBEDDED INFORMATION SYSTEMS BRANCH
|
| This article describes a commercial off-the-shelf (COTS)-based form, fit, function, and interface replacement strategy for legacy avionics computers and embedded information systems that can reuse existing software code while providing a flexible framework for incremental upgrades and managed change. It is based on a real-time embedded software technology that executes legacy binary code on the latest generation COTS microprocessors. This scalable technology, developed by TRW and sponsored in part by ... |
|
| CHAMPION: A Software Design Environment for Adaptive Computing Systems and Application Specific Integrated Circuits (ASICs) |
JUL 2001 |
32 pages |
| Authors:
Don Bouldin; TENNESSEE UNIV KNOXVILLE DEPT OF ELECTRICAL ENGINEERING
|
| Adaptive Computing Systems (ACSs) can serve as flexible hardware accelerators for applications in domains such as image and signal processing. However, the mapping of applications onto ACSs using traditional methods can take months to develop and debug. To enable application designers to map their applications automatically, CHAMPION was developed to permit high-level design entry using the Khoros Cantata graphical programming environment and hide low- level details of the hardware architecture. ... |
|
| 3D Visualization of Tactical Communications for Planning and Operations Using Virtual Reality Modeling Language (VRML) and Extensible 3D (X3D) |
JUN 2001 |
289 pages |
| Authors:
Michael G. Hunsberger; NAVAL POSTGRADUATE SCHOOL MONTEREY CA
|
| The military is increasingly reliant on communication networks for day-to-day tasks as well as large-scale military operations. Tactical communications networks are growing progressively more complex as the amount of information required on the battlefield increases. Communication planners require more advanced tools to perform and manage signal-planning activities. This work examines the use of 3D visualizations to assist in tactical signal planning. These visualizations are developed using Virtual Reality Modeling Language ... |
|
| An Enterprise Identifier Strategy for Global Naming Across Arbitrary C4I Systems |
JUN 2001 |
16 pages |
| Authors:
Sam Chamberlain; ARMY RESEARCH LAB ABERDEEN PROVING GROUND MD
|
| In any information system, a critical feature is the ability to link together disparate pieces of data and information via relationships. One way to greatly facilitate this task is to provide a common identification technique that allows data and information items be conveniently and uniformly referenced. This can be accomplished by standardizing one field across disparate data sources. Perhaps no simpler enhancement can produce such a huge benefit with as ... |
|
| Systems Software for Irregular Parallel Applications |
24 MAY 2001 |
11 pages |
| Authors:
Katherine Yelick; CALIFORNIA UNIV BERKELEY COMPUTER SCIENCE DIV
|
| The long-term objective of this project was to improve programmability of parallel machines for irregular applications with unpredictable computational costs, pointer-based data structures, dynamically allocated data structures, Or asynchronous communications. Example applications include sparse matrix algorithms, adaptive mesh refinement algorithms, and symbolic algorithms. The trend in recent years toward deeper memory hierarchies, including several levels of cache, DRAM, network, and disk, has meant that the more irregular applications have not ... |
|
| Automating the Meta Theory of Deductive Systems |
16 OCT 2000 |
330 pages |
| Authors:
Carsten Schuermann; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| This thesis describes the design of a meta-logical framework that supports the representation and verification of deductive systems, its implementation as an automated theorem prover, and experimental results related to the areas of programming languages, type theory, and logics. Design: The meta-logical framework extends the logical framework LF HHP93 by a meta-logic M(2)(+). This design is novel and unique since it allows higher-order encodings of deductive systems and induction principles ... |
|
| Avoiding Obsolescence with a Low Cost Scalable Fault-Tolerant Computer Architecture |
OCT 2000 |
6 pages |
| Authors:
Josef Schaff; NAVAL AIR SYSTEMS COMMAND PATUXENT RIVER MD
|
| This new computer architecture can use anything from COTS (Commercial Off-The-Shelf) microcontrollers to the latest high-end processors. It is a distributed fault-tolerant architecture that is dynamically reconfigurable in the event of device failures and is fully programmable in conventional high level languages. By using a simple two-level hierarchy with redundant control processors that configure the I/O (Input/Output) processor arrangement even the failure of several processors will have no effect on ... |
|
| Flexible Software Composition CHAIMS |
01 SEP 2000 |
3 pages |
| Authors:
Gio Wiederhold; Neal Sample; STANFORD UNIV CA SPONSORED PROJECTS OFFICE
|
| The CHAIMS effort is developing and refining a very high level programming language for software module composition. In the last two years, that language has been codified and is known as CLAM, the Composition Language for Autonomous Megamodules. The language is currently supported by the CPAM (CHAIMS Protocols for Autonomous Megamodules) runtime system. CPAM is the interface between the compiled megaprogram (client) and the megamodules ... |
|
| The Intuitionism Behind Statecharts Steps |
JUL 2000 |
41 pages |
| Authors:
Gerald Luettgen; Michael Mendler; INSTITUTE FOR COMPUTER APPLICATIONS IN SCIENCE AND ENGINEERING HAMPTON VA
|
| The semantics of Statecharts macro steps, as introduced by Pnueli and Shalev, lacks compositionality. This report first analyzes the compositionality problem and traces it back to the invalidity of the Law of the Excluded Middle. It then characterizes the semantics via a particular class of linear, intuitionistic Kripke models, namely stabilization sequences. This yields, for the first time in the literature, a simple fully-abstract semantics ... |
|
| Automatically Generating a Distributed 3D Virtual Battlespace Using USMTF and XML-MTF Air Tasking Orders, Extensible Markup Language (XML) and Virtual Reality Modeling Language (VRML) |
JUN 2000 |
391 pages |
| Authors:
Mark W. Murray; Jason M. Quigley; NAVAL POSTGRADUATE SCHOOL MONTEREY CA
|
| For the past three decades, the Department of Defense (DoD) has used the U.S. Message Text Format (USMTF) as the primary means to exchange information and to achieve interoperability between joint and coalition forces. To more effectively exchange and share data, the Defense Information Systems Agency (DISA), the lead agency for the USMTF, is actively engaged in extending the USMTF standard with a new ... |
|
| Towards a Customizable PVS |
JAN 2000 |
15 pages |
| Authors:
Gerald Luttgen; Cesar Munoz; Ricky Butler; Ben DiVito; Paul Miner; INSTITUTE FOR COMPUTER APPLICATIONS IN SCIENCE AND ENGINEERING HAMPTON VA
|
| PVS is a state-of-the-art theorem-proving tool developed by SRI international. It is used in a variety of academic and real-world applications by NASA and ICASE researchers, for whom tool customization and extensibility are becoming increasingly important issues. This paper shows by referring to past experiences with several projects and case studies, that the customization features currently offered by PVS are often insufficient. It also suggests ... |
|
| Representing Java Classes in a Typed Intermediate Language |
SEP 1999 |
15 pages |
| Authors:
Christopher League; Zhong Shao; Valery Trifonov; YALE UNIV NEW HAVEN CT DEPT OF COMPUTER SCIENCE
|
| We propose a conservative extension of the polymorphic lambda calculus F(omega) as an intermediate language for compiling languages with name-based class and interface hierarchies. Our extension enriches standard F(omega) with recursive types, existential types, and row polymorphism, but only ordered records with no subtyping. Basing our language on F(omega) makes it also a suitable target for translation from other higher-order languages; this enables the safe interoperation between class-based and higher-order ... |
|
| Structural Embedding: Mechanization with Method |
JUL 1999 |
22 pages |
| Authors:
Cesar Munoz; John Rushby; INSTITUTE FOR COMPUTER APPLICATIONS IN SCIENCE AND ENGINEERING HAMPTON VA
|
| The most powerful tools for analysis of formal specifications are general purpose theorem provers and model checkers, but these tools provide scant methodological support. Conversely, those approaches that do provide a well developed method generally have less powerful automation. It is natural, therefore, to try to combine the better developed methods with the more powerful general purpose tools. An obstacle is that the methods and the tools often employ very ... |
|
| Behavioral Fault Modeling in a VHDL Synthesis Environment |
MAY 1999 |
306 pages |
| Authors:
Ronald J. Hayne; VIRGINIA UNIV CHARLOTTESVILLE SCHOOL OF ENGINEERING AND APPLIED SCIENCE
|
| Integrated circuit designs continue to increase in both size and complexity, making fault simulation and testing more difficult and costly. Computer aided design tools and hardware description languages are now commonly used to represent designs at higher levels of abstraction. However, fault simulation and testing of digital circuits have been historically done using fault models at the gate level or below. A design methodology is needed for performing fault simulation ... |
|
| Combination and Interoperation of Logical Systems Research in Formal Interoperability |
30 APR 1999 |
10 pages |
| Authors:
John McCarthy; Carolyn Talcott; STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
|
| This project involved investigation of both interpretations of the phrase formal interoperability: (1) formal semantics of the interoperation of components and their combination into complex systems; and (2) the interoperation of formal systems and their combined use to specify the many aspects of complex systems. (1) scientific foundations for sensible, correct and secure interaction between components; (2) formalizing different aspects of complex systems and ... |
|
| Parallel Very High Speed Integrated Circuits (VHSIC) Hardware Description Language (VHDL) Simulation for Performance Modeling |
MAR 1999 |
131 pages |
| Authors:
Moon Jung Chung; MICHIGAN STATE UNIV EAST LANSING DEPT OF COMPUTER SCIENCE
|
| As the complexity of microelectronic systems continuously increases, it becomes critical to develop effective tools that can cut the design time and improve the quality of design. DoD needs to develop new tools to be able to simulate large complex systems, and to fully maximize the rapid progress in high performance computing technology occurring today. The goal of this project was to develop and implement efficient ... |
|
| Transforming Cobol Legacy Software to a Generic Imperative Model |
MAR 1999 |
91 pages |
| Authors:
DinaL. Moraes; AIR FORCE INST OF TECH WRIGHT-PATTERSONAFB OH
|
| Legacy COBOL code presents challenges for organizations wishing to increase their effectiveness and improve their efficiency. The systems that utilize this code are vital to enterprise operations, yet maintenance of code is expensive. This research presents an alternative that overcomes some of the problems of legacy COBOL code through the use of software reengineering techniques. This research develops a transformation system to convert COBOL code into a generic imperative model, ... |
|
| CAPSL Interface for the NRL Protocol Analyzer |
1999 |
11 pages |
| Authors:
Stephen Brackin; Catherine Meadows; Jonathan Millen; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| The Common Authentication Protocol Specification Language (CAPSL) is a high-level language for applying formal methods to the security analysis of cryptographic protocols. Its goal is to permit a protocol to be specified once in a form that is usable as an interface to any type of analysis tool or technique, given appropriate translation software. This paper describes the first operational CAPSL translator to the language used by the NRL Protocol ... |
|
| A Halter and A Lead Rope. A Warning to New Government Software Development Managers of Experiences of Those Who Have Gone Before Them |
1999 |
44 pages |
| Authors:
Roy J. Jensen; ARMY WAR COLL CARLISLE BARRACKS PA
|
| This paper will scrutinize the present state of both commercial and military software development where failure of new projects and programming for poor performance is the norm. In addition to scrutinizing the current state of software development, this study will investigate commercial experiences, the Best Practice's methodology and their applicability to military projects. The fundamental approach to this investigation will be to analyze current management of commercial and Department of ... |
|
| Stack-Based Typed Assembly Language |
NOV 1998 |
33 pages |
| Authors:
Greg Morrisett; Karl Crary; David Walker; Neal Glew; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| In previous work, we presented Typed Assembly Language (TAL). TAL is sufficiently expressive to serve as a target language for compilers of high level languages such as ML. That work assumed such a compiler would perform a continuation passing style transform and eliminate the control stack by heap allocating activation records. However, most compilers are based on stack allocation. This paper presents STAL, an extension of TAL with stack constructs ... |
|
Reports by Keyword(s)
HIGH LEVEL LANGUAGES
