Engineering PapersSearch

SEARCH · Engineering Papers

Results for “state machine”

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.

At least 55 records · Page 3

Investigation of automated task learning, decomposition and scheduling

The details and results of research conducted in the application of neural networks to task planning and decomposition are presented. Task planning and decomposition are operations that humans perform in a reasonably efficient manner. Without the use of good heuristics and usually much human interaction, automatic planners and decomposers generally do not perform well due to the intractable nature of the problems under consideration. The human-like performance of neural networks has shown promise for generating acceptable solutions to intractable problems such as planning and decomposition. This was the primary reasoning behind attempting the study. The basis for the work is the use of state machines to model tasks. State machine models provide a useful means for examining the structure of tasks since many formal techniques have been developed for their analysis and synthesis. It is the approach to integrate the strong algebraic foundations of state machines with the heretofore trial-and-error approach to neural network synthesis.

Livingston, David L.

VML 3.0 Reactive Sequencing Objects and Matrix Math Operations for Attitude Profiling

VML (Virtual Machine Language) has been used as the sequencing flight software on over a dozen JPL deep-space missions, most recently flying on GRAIL and JUNO. In conjunction with the NASA SBIR entitled "Reactive Rendezvous and Docking Sequencer", VML version 3.0 has been enhanced to include object-oriented element organization, built-in queuing operations, and sophisticated matrix / vector operations. These improvements allow VML scripts to easily perform much of the work that formerly would have required a great deal of expensive flight software development to realize. Autonomous turning and tracking makes considerable use of new VML features. Profiles generated by flight software are managed using object-oriented VML data constructs executed in discrete time by the VML flight software. VML vector and matrix operations provide the ability to calculate and supply quaternions to the attitude controller flight software which produces torque requests. Using VML-based attitude planning components eliminates flight software development effort, and reduces corresponding costs. In addition, the direct management of the quaternions allows turning and tracking to be tied in with sophisticated high-level VML state machines. These state machines provide autonomous management of spacecraft operations during critical tasks like a hypothetic Mars sample return rendezvous and docking. State machines created for autonomous science observations can also use this sort of attitude planning system, allowing heightened autonomy levels to reduce operations costs. VML state machines cannot be considered merely sequences - they are reactive logic constructs capable of autonomous decision making within a well-defined domain. The state machine approach enabled by VML 3.0 is progressing toward flight capability with a wide array of applicable mission activities.

VML (Virtual Machine Language)

Satellite antenna management system and method

The antenna management system and method allow a satellite to communicate with a ground station either directly or by an intermediary of a second satellite, thus permitting communication even when the satellite is not within range of the ground station. The system and method employ five major software components, which are the control and initialization module, the command and telemetry handler module, the contact schedule processor module, the contact state machining module, and the telemetry state machine module. The control and initialization module initializes the system and operates the main control cycle, in which the other modules are called. The command and telemetry handler module handles communication to and from the ground station. The contact scheduler processor module handles the contact entry schedules to allow scheduling of contacts with the second satellite. The contact and telemetry state machine modules handle the various states of the satellite in beginning, maintaining and ending contact with the second satellite and in beginning, maintaining and ending communication with the satellite.

Leath, Timothy T

Generating local addresses and communication sets for data-parallel programs

Generating local addresses and communication sets is an important issue in distributed-memory implementations of data-parallel languages such as High Performance FORTRAN. We show that, for an array A affinely aligned to a template that is distributed across p processors with a cyclic(k) distribution and a computation involving the regular section A(l:h:s), the local memory access sequence for any processor is characterized by a finite state machine of at most k states. We present fast algorithms for computing the essential information about these state machines, and extend the framework to handle multidimensional arrays. We also show how to generate communication sets using the state machine approach. Performance results show that this solution requires very little run-time overhead and acceptable preprocessing time.

Chatterjee, Siddhartha

Generating local addresses and communication sets for data-parallel programs

Generating local addresses and communication sets is an important issue in distributed-memory implementations of data-parallel languages such as High Performance Fortran. We show that for an array A affinely aligned to a template that is distributed across p processors with a cyclic(k) distribution, and a computation involving the regular section A, the local memory access sequence for any processor is characterized by a finite state machine of at most k states. We present fast algorithms for computing the essential information about these state machines, and extend the framework to handle multidimensional arrays. We also show how to generate communication sets using the state machine approach. Performance results show that this solution requires very little runtime overhead and acceptable preprocessing time.

Chatterjee, Siddhartha

Virtual Machine Language 2.1

VML (Virtual Machine Language) is an advanced computing environment that allows spacecraft to operate using mechanisms ranging from simple, time-oriented sequencing to advanced, multicomponent reactive systems. VML has developed in four evolutionary stages. VML 0 is a core execution capability providing multi-threaded command execution, integer data types, and rudimentary branching. VML 1 added named parameterized procedures, extensive polymorphism, data typing, branching, looping issuance of commands using run-time parameters, and named global variables. VML 2 added for loops, data verification, telemetry reaction, and an open flight adaptation architecture. VML 2.1 contains major advances in control flow capabilities for executable state machines. On the resource requirements front, VML 2.1 features a reduced memory footprint in order to fit more capability into modestly sized flight processors, and endian-neutral data access for compatibility with Intel little-endian processors. Sequence packaging has been improved with object-oriented programming constructs and the use of implicit (rather than explicit) time tags on statements. Sequence event detection has been significantly enhanced with multi-variable waiting, which allows a sequence to detect and react to conditions defined by complex expressions with multiple global variables. This multi-variable waiting serves as the basis for implementing parallel rule checking, which in turn, makes possible executable state machines. The new state machine feature in VML 2.1 allows the creation of sophisticated autonomous reactive systems without the need to develop expensive flight software. Users specify named states and transitions, along with the truth conditions required, before taking transitions. Transitions with the same signal name allow separate state machines to coordinate actions: the conditions distributed across all state machines necessary to arm a particular signal are evaluated, and once found true, that signal is raised. The selected signal then causes all identically named transitions in all present state machines to be taken simultaneously. VML 2.1 has relevance to all potential space missions, both manned and unmanned. It was under consideration for use on Orion.

Riedel, Joseph E.

Shorter function summaries for finite state machine-based high consequence systems using logic synthesis and tautologies (Final Report LDRD 24-1302)

Computer programs are often viewed as collections of functions – each function has parameters (inputs) and computes a return value, and each has potential side effects that modify program state (outputs). In this research, a Sandia symbolic execution tool designed to support “human-in-the-loop” analysis was modified to automatically create “function summaries,” and a new tool, “diaboolical,” was created to support enhancing readability of the summary using a novel approach to bit-vector simplification that leverages logic synthesis and tautologies. For this effort, students at Auburn University created several finite state machines (FSMs) to serve as exemplars for high-consequence systems. Function summaries for each of the machines were obtained, and then portions of the summaries were simplified using both diaboolical and the simplification procedure of a popular SMT solver. A comparison of the results shows that diaboolical can often produce smaller function summaries, with expression length improvements over the unsimplified function summaries ranging from 0% to 90% for diaboolical and 0% to 65% for the SMT solver, though diaboolical had a significantly greater cost in time. Diaboolical was evaluated against a collection of “arbitrary” C-code as well as FSM exemplars, and for both datasets it achieved an approximately 10% improvement in expression length compared to simplifications that could be obtained using existing techniques. Function summaries can assist assurance efforts that evaluate existing systems and their executable code. A smaller function summary is likely easier for humans to understand and could thus increase the ability and efficacy of assurance practices centered around the analysis of executable artifacts.

97 MATHEMATICS AND COMPUTING

Trellises and Trellis-Based Decoding Algorithms for Linear Block Codes

A code trellis is a graphical representation of a code, block or convolutional, in which every path represents a codeword (or a code sequence for a convolutional code). This representation makes it possible to implement Maximum Likelihood Decoding (MLD) of a code with reduced decoding complexity. The most well known trellis-based MLD algorithm is the Viterbi algorithm. The trellis representation was first introduced and used for convolutional codes [23]. This representation, together with the Viterbi decoding algorithm, has resulted in a wide range of applications of convolutional codes for error control in digital communications over the last two decades. There are two major reasons for this inactive period of research in this area. First, most coding theorists at that time believed that block codes did not have simple trellis structure like convolutional codes and maximum likelihood decoding of linear block codes using the Viterbi algorithm was practically impossible, except for very short block codes. Second, since almost all of the linear block codes are constructed algebraically or based on finite geometries, it was the belief of many coding theorists that algebraic decoding was the only way to decode these codes. These two reasons seriously hindered the development of efficient soft-decision decoding methods for linear block codes and their applications to error control in digital communications. This led to a general belief that block codes are inferior to convolutional codes and hence, that they were not useful. Chapter 2 gives a brief review of linear block codes. The goal is to provide the essential background material for the development of trellis structure and trellis-based decoding algorithms for linear block codes in the later chapters. Chapters 3 through 6 present the fundamental concepts, finite-state machine model, state space formulation, basic structural properties, state labeling, construction procedures, complexity, minimality, and sectionalization of trellises. Chapter 7 discusses trellis decomposition and subtrellises for low-weight codewords. Chapter 8 first presents well known methods for constructing long powerful codes from short component codes or component codes of smaller dimensions, and then provides methods for constructing their trellises which include Shannon and Cartesian product techniques. Chapter 9 deals with convolutional codes, puncturing, zero-tail termination and tail-biting.Chapters 10 through 13 present various trellis-based decoding algorithms, old and new. Chapter 10 first discusses the application of the well known Viterbi decoding algorithm to linear block codes, optimum sectionalization of a code trellis to minimize computation complexity, and design issues for IC (integrated circuit) implementation of a Viterbi decoder. Then it presents a new decoding algorithm for convolutional codes, named Differential Trellis Decoding (DTD) algorithm. Chapter 12 presents a suboptimum reliability-based iterative decoding algorithm with a low-weight trellis search for the most likely codeword. This decoding algorithm provides a good trade-off between error performance and decoding complexity. All the decoding algorithms presented in Chapters 10 through 12 are devised to minimize word error probability. Chapter 13 presents decoding algorithms that minimize bit error probability and provide the corresponding soft (reliability) information at the output of the decoder. Decoding algorithms presented are the MAP (maximum a posteriori probability) decoding algorithm and the Soft-Output Viterbi Algorithm (SOVA) algorithm. Finally, the minimization of bit error probability in trellis-based MLD is discussed.

Lin, Shu

Runtime Verification of C Programs

We present in this paper a framework, RMOR, for monitoring the execution of C programs against state machines, expressed in a textual (nongraphical) format in files separate from the program. The state machine language has been inspired by a graphical state machine language RCAT recently developed at the Jet Propulsion Laboratory, as an alternative to using Linear Temporal Logic (LTL) for requirements capture. Transitions between states are labeled with abstract event names and Boolean expressions over such. The abstract events are connected to code fragments using an aspect-oriented pointcut language similar to ASPECTJ's or ASPECTC's pointcut language. The system is implemented in the C analysis and transformation package CIL, and is programmed in OCAML, the implementation language of CIL. The work is closely related to the notion of stateful aspects within aspect-oriented programming, where pointcut languages are extended with temporal assertions over the execution trace.

RMOR

Proceedings of the Second NASA Formal Methods Symposium

This publication contains the proceedings of the Second NASA Formal Methods Symposium sponsored by the National Aeronautics and Space Administration and held in Washington D.C. April 13-15, 2010. Topics covered include: Decision Engines for Software Analysis using Satisfiability Modulo Theories Solvers; Verification and Validation of Flight-Critical Systems; Formal Methods at Intel -- An Overview; Automatic Review of Abstract State Machines by Meta Property Verification; Hardware-independent Proofs of Numerical Programs; Slice-based Formal Specification Measures -- Mapping Coupling and Cohesion Measures to Formal Z; How Formal Methods Impels Discovery: A Short History of an Air Traffic Management Project; A Machine-Checked Proof of A State-Space Construction Algorithm; Automated Assume-Guarantee Reasoning for Omega-Regular Systems and Specifications; Modeling Regular Replacement for String Constraint Solving; Using Integer Clocks to Verify the Timing-Sync Sensor Network Protocol; Can Regulatory Bodies Expect Efficient Help from Formal Methods?; Synthesis of Greedy Algorithms Using Dominance Relations; A New Method for Incremental Testing of Finite State Machines; Verification of Faulty Message Passing Systems with Continuous State Space in PVS; Phase Two Feasibility Study for Software Safety Requirements Analysis Using Model Checking; A Prototype Embedding of Bluespec System Verilog in the PVS Theorem Prover; SimCheck: An Expressive Type System for Simulink; Coverage Metrics for Requirements-Based Testing: Evaluation of Effectiveness; Software Model Checking of ARINC-653 Flight Code with MCP; Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B; Formal Verification of Large Software Systems; Symbolic Computation of Strongly Connected Components Using Saturation; Towards the Formal Verification of a Distributed Real-Time Automotive System; Slicing AADL Specifications for Model Checking; Model Checking with Edge-valued Decision Diagrams; and Data-flow based Model Analysis.

Munoz, Cesar

Transitioning from Software Requirements Models to Design Models

The Scenario Creation and Simulation Process (SCASP) includes the following steps: 1) Write Requirements; 2) Write Use Cases; 3) Prioritize Use Cases; 4) Write Nominal Scenarios; 5) Identify Relationships; 6) Refine/Generalize Scenarios; 7) Transform to State Machines. SCASP provides thorough simulation of use cases before design/implementation, resulting in: 1) Reduced cost; 2) Fewer misunderstandings; 3) Reuse of executable form of use cases. SCASP gives systematic guidelines on how to 1) Separate concerns in use case descriptions; 2) Elicit non-nominal scenarios (alternatives, exceptions, concurrent scenarios, etc.); 3) Transform those scenarios automatically into a set of concurrent state machines; 4) Execute those state machines, i.e., scenario simulation.

Whittle, Jon

A 2-to-48-MHz Phase-Locked Loop

A 2-to-48-MHz phase-locked loop (PLL), developed for the U.S. space program, meets or exceeds all space shuttle clock electrical interface requirements by taking as its reference a 2-to-48-MHz clock signal and outputting a phaselocked clock signal set at the same frequency as the reference clock with transistor- transistor logic (TTL) voltage levels. Because it is more adaptable than other PLLs, the new PLL can be used in industries that employ signaling devices and as a tool in future space missions. A conventional PLL consists of a phase/frequency detector, loop filter, and voltage-controlled oscillator in which each component exists individually and is integrated into a single device. PLL components phase-lock to a single frequency or to a narrow bandwidth of frequencies. It is this design, however, that prohibits them from maintaining phase lock to a dynamically changing reference clock when a large bandwidth is required a deficiency the new PLL overcomes. Since most PLL components require their voltage-controlled oscillators to operate at greater than 2-MHz frequencies, conventional PLLs often cannot achieve the low-frequency phase lock allowed by the new PLL. The 2-to-48-MHz PLL is built on a wire-wrap board with pins wired to three position jumpers; this makes changing configurations easy. It responds to variations in voltage-controlled oscillator (VCO) ranges, duty cycle, signal-to-noise ratio (SNR), amplitude, and jitter, exceeding design specifications. A consensus state machine, implemented in a VCO range detector which assures the PLL continues to operate in the correct range, is the primary control state machine for the 2-to-48-MHz PLL circuit. By using seven overlapping frequency ranges with hysteresis, the PLL output sets the resulting phase-locked clock signal at a frequency that agrees with the reference clock with TTL voltage levels. As a space-shuttle tool, the new PLL circuit takes the noisy, degraded reference clock signals as input and outputs phase-locked clock signals of the same frequency but with a corrected wave shape. Since its configuration circuit can be easily changed, the new PLL can do the following: readily respond to variations in VCO ranges, duty cycle, SNR, amplitude, and jitter; continuously operate in the correct VCO range because of its consensus state machine; and use its range detector implements to overlap seven frequency ranges with hysteresis, thus giving the current design a flexibility that exceeds anything available at the time of this development. These features will benefit any industry in which safe and timely clock signals are vital to operation.

Koudelka, Robert D.

Generating Real-Time Robotics Control Software from SysML

In this paper, we outline an approach for autogenerating real-time robotics control code from hierarchical state machines and hardware configurations encoded in Systems Modeling Language (SysML). We propose a software architecture that provides an abstract SysML layer with access to device state information and a set of primitive device commands, such as move actuator and release brake, allowing a user to build up a complete functional state machine directly in SysML. The SysML diagram is then exported to a standard SCXML file format and subsequently used to auto-generate hardware control code. Once this architecture is in place, the only explicit code elements that need to be written are the primitive device commands, which can be easily unit tested and reused across different systems. The motivation for this work was the need for a test bed that enables the rapid prototyping of mechanisms and control algorithms for a spacecraft that could ultimately be used for preparing Martian rock samples for their return to Earth. To this end, our software system was also designed to allow for the run-time specification of the hardware layout in SysML, with the hardware-level control functions kept agnostic to the specific parameters or communication bus of any particular device. Further, we outline a system for specifying both the state machine and hardware configuration in the MagicDraw IDE in such a way that the system can be simulated before any code is generated. The resultant software system is easy to debug, understand, and allows users to choose how much information is encoded as a visual or text-based representation.

Godart, Peter

Programmable Pulse-Position-Modulation Encoder

A programmable pulse-position-modulation (PPM) encoder has been designed for use in testing an optical communication link. The encoder includes a programmable state machine and an electronic code book that can be updated to accommodate different PPM coding schemes. The encoder includes a field-programmable gate array (FPGA) that is programmed to step through the stored state machine and code book and that drives a custom high-speed serializer circuit board that is capable of generating subnanosecond pulses. The stored state machine and code book can be updated by means of a simple text interface through the serial port of a personal computer.

Zhu, David

Intelligent fuzzy controller for event-driven real time systems

Most of the known linguistic models are essentially static, that is, time is not a parameter in describing the behavior of the object's model. In this paper we show a model for synchronous finite state machines based on fuzzy logic. Such finite state machines can be used to build both event-driven, time-varying, rule-based systems and the control unit section of a fuzzy logic computer. The architecture of a pipelined intelligent fuzzy controller is presented, and the linguistic model is represented by an overall fuzzy relation stored in a single rule memory. A VLSI integrated circuit implementation of the fuzzy controller is suggested. At a clock rate of 30 MHz, the controller can perform 3 MFLIPS on multi-dimensional fuzzy data.

Grantner, Janos

A Graphical User Interface for the Deep Underground Neutrino Experiment Robotic Test Stand

In preparation for DUNE, Fermilab along with six other institutions are testing cold electronics for quality control before components placed in the far detector. We test them by using a robotic arm that places these chips into sockets on a computer board that will test their functionality. Up until now, the chips have been tested using a command line script that drives a state machine to conduct tests step-by-step. In order to lower the skill barrier to conduct tests and to speed up the quality control process, I was tasked to create a graphical user interface that would allow users to use buttons, text boxes, and drop-down menus to input information and tell the testing state machine how to operate. I had to learn about the Python package Tkinter to start the process of widget placement. I further developed a pause feature unused in the previous command line script that would allow the user to shut down testing gracefully, bring the robotic arm to go back to ground state, and go forward or backward a step in the testing process. After completing the basic functionality of the GUI, I started testing production chips with the GUI to debug. Some issues were found, which required me to further develop parts of the inherited state machine code. The code for the GUI has now been pushed into the copy the DUNE/FD_CE git repository and will soon be merged with the official DUNE/FD_CE repository so that the other institutions testing DUNE cold electronics can use and expand upon it.

Gutierrez Villanueva, Jaziel [Fermilab]

Decidability for a temporal logic used in discrete-event system analysis

The type of plant considered is one that can be modeled by a nondeterministic finite-state machine P. The regulator is a deterministic finite state machine R. The closed-loop system is formed by connecting P and R in a regulator configuration. Formulas in a propositional temporal language are used to describe the behavior of the closed-loop system. It is shown that there is a mechanical procedure which, for a given P and R, and a temporal formula Psi, will determine in a finite number of steps whether or not Psi must be true. This 'decidability' result could be proven using other known results on temporal logic. The proof given here shows that the behavior of the closed-loop system may safely be assumed to be ultimately periodic. The results are illustrated on two discrete-event system examples.

Knight, J. F.