Engineering topics

Lan, Sonie

Publications and source records attributed to Lan, Sonie.

3 records

NASA NTRS2001

Automata-Based Verification of Temporal Properties on Running Programs

This paper presents an approach to checking a running program against its Linear Temporal Logic (LTL) specifications. LTL is a widely used logic for expressing properties of programs viewed as sets of executions. Our approach consists of translating LTL formulae to finite-state automata, which are used as observers of the program behavior. The translation algorithm we propose modifies standard LTL to Buchi automata conversion techniques to generate automata that check finite program traces. The algorithm has been implemented in a tool, which has been integrated with the generic JPaX framework for runtime analysis of Java programs.

Giannakopoulou, Dimitra↗

NASA NTRS2001

Monitoring Programs Using Rewriting

We present a rewriting algorithm for efficiently testing future time Linear Temporal Logic (LTL) formulae on finite execution traces, The standard models of LTL are infinite traces, reflecting the behavior of reactive and concurrent systems which conceptually may be continuously alive in most past applications of LTL, theorem provers and model checkers have been used to formally prove that down-scaled models satisfy such LTL specifications. Our goal is instead to use LTL for up-scaled testing of real software applications, corresponding to analyzing the conformance of finite traces against LTL formulae. We first describe what it means for a finite trace to satisfy an LTL property end then suggest an optimized algorithm based on transforming LTL formulae. We use the Maude rewriting logic, which turns out to be a good notation and being supported by an efficient rewriting engine for performing these experiments. The work constitutes part of the Java PathExplorer (JPAX) project, the purpose of which is to develop a flexible tool for monitoring Java program executions.

Havelund, Klaus↗

NASA NTRS1998

Bacteriorhodopsin Material and Film Fabrication Issues for Holographic Applications

We discuss issues associated with bacteriorhodopsin (BR) materials and films that affect optical performance in holographic applications. For the D85N variant, some critical parameters include degree of hydration and recording wavelength. The quantum efficiency of the molecular state transition is observed to be apparently dependent on the illumination wavelength. We explain this effect by modeling the photo-activity of the D85N variant as two competing photocycles between the 9-cis and 13-cis retinal configurations. We are able to determine the pure excited P-state absorbance spectrum from the ground state spectrum and mixed population spectra obtained by bleaching to steady-state conditions.

Downie, John D.↗