Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “PENELOPE code system”

Search indexed NASA NTRS and DOE OSTI research on propulsion, heat transfer, battery materials and energy systems. Follow report and document links to the original sources.

Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.

5 records
All sourcesNASA NTRSDOE OSTI
DOE OSTI2021

The PENELOPE Physics Models and Transport Mechanics. Implementation into Geant4

A translation of the PENELOPE physics subroutines to C++, designed as an extension of the GEANT4 toolkit, is presented. The Fortran code system PENELOPE performs Monte Carlo simulation of coupled electron-photon transport in arbitrary materials for a wide energy range, nominally from 50 eV up to 1 GeV. PENELOPE implements the most reliable interaction models that are currently available, limited only by the required generality of the code. In addition, the transport of electrons and positrons is simulated by means of an elaborate class II scheme in which hard interactions (involving deflection angles or energy transfers larger than pre-defined cutoffs) are simulated from the associated restricted differential cross sections. After a brief description of the interaction models adopted for photons and electrons/positrons, we describe the details of the class-II algorithm used for tracking electrons and positrons. The C++ classes are adapted to the specific code structure of GEANT4. They provide a complete description of the interactions and transport mechanics of electrons/positrons and photons in arbitrary materials, which can be activated from the G4ProcessManager to produce simulation results equivalent to those from the original PENELOPE programs. The combined code, named PENG4, benefits from the multi-threading capabilities and advanced geometry and statistical tools of GEANT4.

71 CLASSICAL AND QUANTUM MECHANICS, GENERAL PHYSIC↗
NASA NTRS1991

Integrity and security in an Ada runtime environment

A review is provided of the Formal Methods group discussions. It was stated that integrity is not a pure mathematical dual of security. The input data is part of the integrity domain. The group provided a roadmap for research. One item of the roadmap and the final position statement are closely related to the space shuttle and space station. The group's position is to use a safe subset of Ada. Examples of safe sets include the Army Secure Operating System and the Penelope Ada verification tool. It is recommended that a conservative attitude is required when writing Ada code for life and property critical systems.

Bown, Rodney L.↗
NASA NTRS1995

Introduction to Penelope

A formal program verification is a (mathematical) proof that a program executed according to its intended model meets some specification. This proves that the algorithm defined by the program is correct in the precise technical sense of being consistent with a particular specification. A program correct in this sense is free from a large and important class of errors, even though its behavior may still produce unintended results--either because the implementation of the programming language itself does not match the model of execution, or because the specification does not correctly express the user's intentions. Penelope is a prototype system for interactively developing and verifying programs that are written in a rich subset of sequential Ada. Penelope can be used to develop a program and its correctness proof incrementally, and in concert with one another. Incrementality is used in a number of ways to help make verification more tractable and more productive. For example, if an already-verified program is modified, one can attempt to prove the modified version by replaying and modifying the original verification. Penelope's specification language, Larch/Ada, belongs to the family of Larch interface languages. Larch/Ada scales up properly, in the sense that it is demonstrably sound to decompose a system hierarchically and reason locally about the implementation of each piece. Penelope has been applied in various demonstration projects--for specification (guidance control, distributed operating systems), verification (of off-the-shelf code), and formal development (by non-expert as well as expert users). Some features of Penelope have been embodied in Ada Wise, a lint-like non-interactive tool that warns of the potential for certain dynamic semantic errors in Ada programs.

Guaspari, David↗
NASA NTRS1991

Formal specification and verification of Ada software

The use of formal methods in software development achieves levels of quality assurance unobtainable by other means. The Larch approach to specification is described, and the specification of avionics software designed to implement the logic of a flight control system is given as an example. Penelope is described which is an Ada-verification environment. The Penelope user inputs mathematical definitions, Larch-style specifications and Ada code and performs machine-assisted proofs that the code obeys its specifications. As an example, the verification of a binary search function is considered. Emphasis is given to techniques assisting the reuse of a verification effort on modified code.

Hird, Geoffrey R.↗
NASA NTRS1990

Formally specifying the logic of an automatic guidance controller

The following topics are covered in viewgraph form: (1) the Penelope Project; (2) the logic of an experimental automatic guidance control system for a 737; (3) Larch/Ada specification; (4) some failures of informal description; (5) description of mode changes caused by switches; (6) intuitive description of window status (chosen vs. current); (7) design of the code; (8) and specifying the code.

Guaspari, David↗