Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “Methods”

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 1,585 records · Page 88
All sourcesNASA NTRSDOE OSTI
NASA NTRS2002

New Method Developed to Measure Contact Angles of a Sessile Drop

The spreading of an evaporating liquid on a solid surface occurs in many practical processes and is of importance in a number of practical situations such as painting, textile dyeing, coating, gluing, and thermal engineering. Typical processes involving heat transfer where the contact angle plays an important role are film cooling, boiling, and the heat transfer through heat pipes. The biological phenomenon of cell spreading also is analogous to a drop spreading (ref. 1). In the study of spreading, the dynamic contact angle describes the interfacial properties on solid substrates and, therefore, has been studied by physicists and fluid mechanics investigators. The dynamic contact angle of a spreading nonvolatile liquid drop provides a simple tool in the study of the free-boundary problem, but the study of the spreading of a volatile liquid drop is of more practical interest because the evaporation of common liquids is inevitable in practical processes. The most common method to measure the contact angle, the contact radius, and the height of a sessile drop on a solid surface is to view the drop from its edge through an optical microscope. However, this method gives only local information in the view direction. Zhang and Yang (ref. 2) developed a laser shadowgraphy method to investigate the evaporation of sessile drop on a glass plate. As described here, Zhang and Chao (refs. 3 and 4) improved the method and suggested a new optical arrangement to measure the dynamic contact angle and the instant evaporation rate of a sessile drop with much higher accuracy (less than 1 percent). With this method, any fluid motion in the evaporating drop can be visualized through shadowgraphy without using a tracer, which often affects the field under investigation.

Chao, David F.↗
NASA NTRS2004

Computation of Gust-Cascade Interaction Using the CE/SE Method

The problem 2 in Category 3 of the 4th Computational Aeroacoustic(CAA) Workshop is solved using the space-time conservation element and solution element (CE/SE) method. This problem models rotor-stator interaction in a 2D cascade. It involves complex geometries and flow physics including vortex shedding and acoustic radiation. The parallel version of the 2D nonlinear Euler solver is used with an unstructured triangular mesh to solve this problem. The Giles approach is incorporated with the CE/SE method to handle non-equal pitches of the rotor and stator. Validation on the Giles approach is performed using Problem 3.1 in the 2nd CAA Workshop. The space-time CE/SE method is a finite volume method with second-order accuracy in both space and time. The flux conservation is enforced in both space and time instead of space only. It has low numerical dissipation and dispersion errors. It uses simple non-reflecting boundary conditions and is compatible with unstructured meshes. It is simple, flexible, and generate reasonably accurate solutions. The CE/SE method has been successfully applied to solve numerous practical problems, especially aeroacoustic problems. Some preliminary numerical results of the benchmark problem 3.2 of the 4th CAA Workshop are shown. The steady-state pressure contour is plotted. The mean pressure distribution on the blade surface is compared with Turbo solution showing a good agreement. The sound pressure level versus the rotor harmonic n at the six designated positions on the blade surface, three locations at inlet plane, and three locations at the outlet plane are plotted. It can be seen that the acoustic response exists only at the excitation frequencies (n = 1,2,3). On the blade surface, the acoustic wave at n = 1 is dominant, while at the inlet and outlet planes, the sound pressure level at n = 2 becomes the largest, which is similar to the results presented. The distribution of sound pressure level at different spatial modes along the z- direction is plotted for n = 1,2,3, respectively. It shows that the spatial modes m = -32 and 22 at n = 1 exponentially decay, and the spatial modes m = 10 at n = 2, m = -42 and 12 at n = 3 propagate both upstream and downstream, which agrees with the prediction based on the linearized theory. Some oscillations are observed, which needs to be investigated further. In the final paper, the numerical results will be compared with a frequency-domain solver LINFLUX solution if it is available.

Wang, X.-Y.↗
NASA NTRS2005

Generic Sensor Modeling Using Pulse Method

Recent development of high spatial resolution satellites such as IKONOS, Quickbird and Orbview enable observation of the Earth's surface with sub-meter resolution. Compared to the 30 meter resolution of Landsat 5 TM, the amount of information in the output image was dramatically increased. In this era of high spatial resolution, the estimation of spatial quality of images is gaining attention. Historically, the Modulation Transfer Function (MTF) concept has been used to estimate an imaging system's spatial quality. Sometimes classified by target shapes, various methods were developed in laboratory environment utilizing sinusoidal inputs, periodic bar patterns and narrow slits. On-orbit sensor MTF estimation was performed on 30-meter GSD Landsat4 Thematic Mapper (TM) data from the bridge pulse target as a pulse input . Because of a high resolution sensor s small Ground Sampling Distance (GSD), reasonably sized man-made edge, pulse, and impulse targets can be deployed on a uniform grassy area with accurate control of ground targets using tarps and convex mirrors. All the previous work cited calculated MTF without testing the MTF estimator's performance. In previous report, a numerical generic sensor model had been developed to simulate and improve the performance of on-orbit MTF estimating techniques. Results from the previous sensor modeling report that have been incorporated into standard MTF estimation work include Fermi edge detection and the newly developed 4th order modified Savitzky-Golay (MSG) interpolation technique. Noise sensitivity had been studied by performing simulations on known noise sources and a sensor model. Extensive investigation was done to characterize multi-resolution ground noise. Finally, angle simulation was tested by using synthetic pulse targets with angles from 2 to 15 degrees, several brightness levels, and different noise levels from both ground targets and imaging system. As a continuing research activity using the developed sensor model, this report was dedicated to MTF estimation via pulse input method characterization using the Fermi edge detection and 4th order MSG interpolation method. The relationship between pulse width and MTF value at Nyquist was studied including error detection and correction schemes. Pulse target angle sensitivity was studied by using synthetic targets angled from 2 to 12 degrees. In this report, from the ground and system noise simulation, a minimum SNR value was suggested for a stable MTF value at Nyquist for the pulse method. Target width error detection and adjustment technique based on a smooth transition of MTF profile is presented, which is specifically applicable only to the pulse method with 3 pixel wide targets.

Helder, Dennis L.↗
NASA NTRS2005

A Tail Buffet Loads Prediction Method for Aircraft at High Angles of Attack

Aircraft designers commit significant resources to the design of aircraft in meeting performance goals. Despite fulfilling traditional design requirements, many fighter aircraft have encountered buffet loads when demonstrating their high angle-of-attack maneuver capabilities. As a result, during test or initial production phases of fighter development programs, many new designs are impacted, usually in a detrimental way, by resulting in reassessing designs or limiting full mission capability. These troublesome experiences usually stem from overlooking or completely ignoring the effects of buffet during the design phase of aircraft. Perhaps additional requirements are necessary that addresses effects of buffet in achieving best aircraft performance in fulfilling mission goals. This paper describes a reliable, fairly simple, but quite general buffet loads analysis method to use in the initial design phases of fighter-aircraft development. The method is very similar to the random gust load analysis that is now commonly available in a commercial code, which this analysis capability is based, with some key modifications. The paper describes the theory and the implementation of the methodology. The method is demonstrated on a JSF prototype example problem. The demonstration also serves as a validation of the method, since, in the paper, the analysis is shown to nearly match the flight data. In addition, the paper demonstrates how the analysis method can be used to assess candidate design concepts in determining a satisfactory final aircraft configuration.

Pototzky, Anthony S.↗
NASA NTRS2005

Diffuse Attenuation Coefficient of Downwelling Irradiance: An Evaluation of Remote Sensing Methods

The propagation of downwelling irradiance at wavelength lambda from surface to a depth (z) in the ocean is governed by the diffuse attenuation coefficient, K(sup -)(sub d)(lambda). There are two standard methods for the derivation of K(sup -)(sub d)(lambda) in remote sensing, which both are based on empirical relationships involving the blue-to-green ratio of ocean color. Recently, a semianalytical method to derive K(sup -)(sub d)(lambda) from reflectance has also been developed. In this study, using K(sup -)(sub d)(490) and K(sup -)(sub d)(443) as examples, we compare the K(sup -)(sub d)(lambda) values derived from the three methods using data collected in three different regions that cover oceanic and coastal waters, with K(sup -)(sub d)(490) ranging from approximately 0.04 to 4.0 per meter. The derived values are compared with the data calculated from in situ measurements of the vertical profiles of downwelling irradiance. The comparisons show that the two standard methods produced satisfactory estimates of K(sup -)(sub d)(lambda) in oceanic waters where attenuation is relatively low but resulted in significant errors in coastal waters. The newly developed semianalytical method appears to have no such limitation as it performed well for both oceanic and coastal waters. For all data in this study the average of absolute percentage difference between the in situ measured and the semianalytically derived K(sup -)(sub d) is approximately 14% for lambda = 490 nm and approximately 11% for lambda = 443 nm.

Lee, Zhong-Ping↗
NASA NTRS2006

The Equivalence of the Radial Return and Mendelson Methods for Integrating the Classical Plasticity Equations

The radial return and Mendelson methods for integrating the equations of classical plasticity, which appear independently in the literature, are shown to be identical. Both methods are presented in detail as are the specifics of their algorithmic implementation. Results illustrate the methods' equivalence across a range of conditions and address the question of when the methods require iteration in order for the plastic state to remain on the yield surface. FORTRAN code implementations of the radial return and Mendelson methods are provided in the appendix.

Bednarcyk, Brett A.↗
NASA NTRS2006

Application of the Bootstrap Statistical Method in Deriving Vibroacoustic Specifications

This paper discusses the Bootstrap Method for specification of vibroacoustic test specifications. Vibroacoustic test specifications are necessary to properly accept or qualify a spacecraft and its components for the expected acoustic, random vibration and shock environments seen on an expendable launch vehicle. Traditionally, NASA and the U.S. Air Force have employed methods of Normal Tolerance Limits to derive these test levels based upon the amount of data available, and the probability and confidence levels desired. The Normal Tolerance Limit method contains inherent assumptions about the distribution of the data. The Bootstrap is a distribution-free statistical subsampling method which uses the measured data themselves to establish estimates of statistical measures of random sources. This is achieved through the computation of large numbers of Bootstrap replicates of a data measure of interest and the use of these replicates to derive test levels consistent with the probability and confidence desired. The comparison of the results of these two methods is illustrated via an example utilizing actual spacecraft vibroacoustic data.

Hughes, William O.↗
NASA NTRS2007

Comparison of Fixed and Variable Time Step Trajectory Integration Methods for Cislunar Trajectories

Due to the nonlinear nature of the Earth-Moon-Sun three-body problem and non-spherical gravity, CEV cislunar targeting algorithms will require many propagations in their search for a desired trajectory. For on-board targeting especially, the algorithm must have a simple, fast, and accurate propagator to calculate a trajectory with reasonable computation time, and still be robust enough to remain stable in the various flight regimes that the CEV will experience. This paper compares Cowell s method with a fourth-order Runge- Kutta integrator (RK4), Encke s method with a fourth-order Runge-Kutta- Nystr m integrator (RKN4), and a method known as Multi-Conic. Additionally, the study includes the Bond-Gottlieb 14-element method (BG14) and extends the investigation of Encke-Nystrom methods to integrators of higher order and with variable step size.

Weeks, ichael W.↗
NASA NTRS2007

A Statistical Approach for the Concurrent Coupling of Molecular Dynamics and Finite Element Methods

Molecular dynamics (MD) methods are opening new opportunities for simulating the fundamental processes of material behavior at the atomistic level. However, increasing the size of the MD domain quickly presents intractable computational demands. A robust approach to surmount this computational limitation has been to unite continuum modeling procedures such as the finite element method (FEM) with MD analyses thereby reducing the region of atomic scale refinement. The challenging problem is to seamlessly connect the two inherently different simulation techniques at their interface. In the present work, a new approach to MD-FEM coupling is developed based on a restatement of the typical boundary value problem used to define a coupled domain. The method uses statistical averaging of the atomistic MD domain to provide displacement interface boundary conditions to the surrounding continuum FEM region, which, in return, generates interface reaction forces applied as piecewise constant traction boundary conditions to the MD domain. The two systems are computationally disconnected and communicate only through a continuous update of their boundary conditions. With the use of statistical averages of the atomistic quantities to couple the two computational schemes, the developed approach is referred to as an embedded statistical coupling method (ESCM) as opposed to a direct coupling method where interface atoms and FEM nodes are individually related. The methodology is inherently applicable to three-dimensional domains, avoids discretization of the continuum model down to atomic scales, and permits arbitrary temperatures to be applied.

Saether, E.↗
NASA NTRS2002

Method and system for training dynamic nonlinear adaptive filters which have embedded memory

Described herein is a method and system for training nonlinear adaptive filters (or neural networks) which have embedded memory. Such memory can arise in a multi-layer finite impulse response (FIR) architecture, or an infinite impulse response (IIR) architecture. We focus on filter architectures with separate linear dynamic components and static nonlinear components. Such filters can be structured so as to restrict their degrees of computational freedom based on a priori knowledge about the dynamic operation to be emulated. The method is detailed for an FIR architecture which consists of linear FIR filters together with nonlinear generalized single layer subnets. For the IIR case, we extend the methodology to a general nonlinear architecture which uses feedback. For these dynamic architectures, we describe how one can apply optimization techniques which make updates closer to the Newton direction than those of a steepest descent method, such as backpropagation. We detail a novel adaptive modified Gauss-Newton optimization technique, which uses an adaptive learning rate to determine both the magnitude and direction of update steps. For a wide range of adaptive filtering applications, the new training algorithm converges faster and to a smaller value of cost than both steepest-descent methods such as backpropagation-through-time, and standard quasi-Newton methods. We apply the algorithm to modeling the inverse of a nonlinear dynamic tracking system 5, as well as a nonlinear amplifier 6.

Rabinowitz, Matthew↗
NASA NTRS2008

Intravenous Fluid Mixing in Normal Gravity, Partial Gravity, and Microgravity: Down-Selection of Mixing Methods

The missions envisioned under the Vision for Space Exploration will require development of new methods to handle crew medical care. Medications and intravenous (IV) fluids have been identified as one area needing development. Storing certain medications and solutions as powders or concentrates can both increase the shelf life and reduce the overall mass and volume of medical supplies. The powders or concentrates would then be mixed in an IV bag with Sterile Water for Injection produced in situ from the potable water supply. Fluid handling in microgravity is different than terrestrial settings, and requires special consideration in the design of equipment. This document describes the analyses and down-select activities used to identify the IV mixing method to be developed that is suitable for ISS and exploration missions. The chosen method is compatible with both normal gravity and microgravity, maintains sterility of the solution, and has low mass and power requirements. The method will undergo further development, including reduced gravity aircraft experiments and computations, in order to fully develop the mixing method and associated operational parameters.

Niederhaus, Charles E.↗
NASA NTRS2006

Increased Fidelity in Prediction Methods For Landing Gear Noise

An aeroacoustic prediction scheme has been developed for landing gear noise. The method is designed to handle the complex landing gear geometry of current and future aircraft. The gear is represented by a collection of subassemblies and simple components that are modeled using acoustic elements. These acoustic elements are generic, but generate noise representative of the physical components on a landing gear. The method sums the noise radiation from each component of the undercarriage in isolation accounting for interference with adjacent components through an estimate of the local upstream and downstream flows and turbulence intensities. The acoustic calculations are made in the code LGMAP, which computes the sound pressure levels at various observer locations. The method can calculate the noise from the undercarriage in isolation or installed on an aircraft for both main and nose landing gear. Comparisons with wind tunnel and flight data are used to initially calibrate the method, then it may be used to predict the noise of any landing gear. In this paper, noise predictions are compared with wind tunnel data for model landing gears of various scales and levels of fidelity, as well as with flight data on fullscale undercarriages. The present agreement between the calculations and measurements suggests the method has promise for future application in the prediction of airframe noise.

Lopes, Leonard V.↗
NASA NTRS2008

NASA Langley's Formal Methods Research in Support of the Next Generation Air Transportation System

This talk will provide a brief introduction to the formal methods developed at NASA Langley and the National Institute for Aerospace (NIA) for air traffic management applications. NASA Langley's formal methods research supports the Interagency Joint Planning and Development Office (JPDO) effort to define and develop the 2025 Next Generation Air Transportation System (NGATS). The JPDO was created by the passage of the Vision 100 Century of Aviation Reauthorization Act in Dec 2003. The NGATS vision calls for a major transformation of the nation s air transportation system that will enable growth to 3 times the traffic of the current system. The transformation will require an unprecedented level of safety-critical automation used in complex procedural operations based on 4-dimensional (4D) trajectories that enable dynamic reconfiguration of airspace scalable to geographic and temporal demand. The goal of our formal methods research is to provide verification methods that can be used to insure the safety of the NGATS system. Our work has focused on the safety assessment of concepts of operation and fundamental algorithms for conflict detection and resolution (CD&R) and self- spacing in the terminal area. Formal analysis of a concept of operations is a novel area of application of formal methods. Here one must establish that a system concept involving aircraft, pilots, and ground resources is safe. The formal analysis of algorithms is a more traditional endeavor. However, the formal analysis of ATM algorithms involves reasoning about the interaction of algorithmic logic and aircraft trajectories defined over an airspace. These trajectories are described using 2D and 3D vectors and are often constrained by trigonometric relations. Thus, in many cases it has been necessary to unload the full power of an advanced theorem prover. The verification challenge is to establish that the safety-critical algorithms produce valid solutions that are guaranteed to maintain separation under all possible scenarios. Current research has assumed perfect knowledge of the location of other aircraft in the vicinity so absolute guarantees are possible, but increasingly we are relaxing the assumptions to allow incomplete, inaccurate, and/or faulty information from communication sources.

Butler, Ricky W.↗
NASA NTRS2006

An Improved Flow Cytometry Method For Precise Quantitation Of Natural-Killer Cell Activity

The ability to assess NK cell cytotoxicity using flow cytometry has been previously described and can serve as a powerful tool to evaluate effector immune function in the clinical setting. Previous methods used membrane permeable dyes to identify target cells. The use of these dyes requires great care to achieve optimal staining and results in a broad spectral emission that can make multicolor cytometry difficult. Previous methods have also used negative staining (the elimination of target cells) to identify effector cells. This makes a precise quantitation of effector NK cells impossible due to the interfering presence of T and B lymphocytes, and the data highly subjective to the variable levels of NK cells normally found in human peripheral blood. In this study an improved version of the standard flow cytometry assay for NK activity is described that has several advantages of previous methods. Fluorescent antibody staining (CD45FITC) is used to positively identify target cells in place of membranepermeable dyes. Fluorescent antibody staining of target cells is less labor intensive and more easily reproducible than membrane dyes. NK cells (true effector lymphocytes) are also positively identified by fluorescent antibody staining (CD56PE) allowing a simultaneous absolute count assessment of both NK cells and target cells. Dead cells are identified by membrane disruption using the DNA intercalating dye PI. Using this method, an exact NK:target ratio may be determined for each assessment, including quantitation of NK target complexes. Backimmunoscatter gating may be used to track live vs. dead Target cells via scatter properties. If desired, NK activity may then be normalized to standardized ratios for clinical comparisons between patients, making the determination of PBMC counts or NK cell percentages prior to testing unnecessary. This method provides an exact cytometric determination of NK activity that highly reproducible and may be suitable for routine use in the clinical setting.

Crucian, Brian↗
NASA NTRS2008

An Embedded Statistical Method for Coupling Molecular Dynamics and Finite Element Analyses

The coupling of molecular dynamics (MD) simulations with finite element methods (FEM) yields computationally efficient models that link fundamental material processes at the atomistic level with continuum field responses at higher length scales. The theoretical challenge involves developing a seamless connection along an interface between two inherently different simulation frameworks. Various specialized methods have been developed to solve particular classes of problems. Many of these methods link the kinematics of individual MD atoms with FEM nodes at their common interface, necessarily requiring that the finite element mesh be refined to atomic resolution. Some of these coupling approaches also require simulations to be carried out at 0 K and restrict modeling to two-dimensional material domains due to difficulties in simulating full three-dimensional material processes. In the present work, a new approach to MD-FEM coupling is developed based on a restatement of the standard boundary value problem used to define a coupled domain. The method replaces a direct linkage of individual MD atoms and finite element (FE) nodes with a statistical averaging of atomistic displacements in local atomic volumes associated with each FE node in an interface region. The FEM and MD computational systems are effectively independent and communicate only through an iterative update of their boundary conditions. With the use of statistical averages of the atomistic quantities to couple the two computational schemes, the developed approach is referred to as an embedded statistical coupling method (ESCM). ESCM provides an enhanced coupling methodology that is inherently applicable to three-dimensional domains, avoids discretization of the continuum model to atomic scale resolution, and permits finite temperature states to be applied.

Saether, E.↗
NASA NTRS2010

Method and system for progressive mesh storage and reconstruction using wavelet-encoded height fields

Systems and methods are provided for progressive mesh storage and reconstruction using wavelet-encoded height fields. A method for progressive mesh storage includes reading raster height field data, and processing the raster height field data with a discrete wavelet transform to generate wavelet-encoded height fields. In another embodiment, a method for progressive mesh storage includes reading texture map data, and processing the texture map data with a discrete wavelet transform to generate wavelet-encoded texture map fields. A method for reconstructing a progressive mesh from wavelet-encoded height field data includes determining terrain blocks, and a level of detail required for each terrain block, based upon a viewpoint. Triangle strip constructs are generated from vertices of the terrain blocks, and an image is rendered utilizing the triangle strip constructs. Software products that implement these methods are provided.

Baxes, Gregory A.↗
NASA NTRS2010

Interlaminar Stresses by Refined Beam Theories and the Sinc Method Based on Interpolation of Highest Derivative

Computation of interlaminar stresses from the higher-order shear and normal deformable beam theory and the refined zigzag theory was performed using the Sinc method based on Interpolation of Highest Derivative. The Sinc method based on Interpolation of Highest Derivative was proposed as an efficient method for determining through-the-thickness variations of interlaminar stresses from one- and two-dimensional analysis by integration of the equilibrium equations of three-dimensional elasticity. However, the use of traditional equivalent single layer theories often results in inaccuracies near the boundaries and when the lamina have extremely large differences in material properties. Interlaminar stresses in symmetric cross-ply laminated beams were obtained by solving the higher-order shear and normal deformable beam theory and the refined zigzag theory with the Sinc method based on Interpolation of Highest Derivative. Interlaminar stresses and bending stresses from the present approach were compared with a detailed finite element solution obtained by ABAQUS/Standard. The results illustrate the ease with which the Sinc method based on Interpolation of Highest Derivative can be used to obtain the through-the-thickness distributions of interlaminar stresses from the beam theories. Moreover, the results indicate that the refined zigzag theory is a substantial improvement over the Timoshenko beam theory due to the piecewise continuous displacement field which more accurately represents interlaminar discontinuities in the strain field. The higher-order shear and normal deformable beam theory more accurately captures the interlaminar stresses at the ends of the beam because it allows transverse normal strain. However, the continuous nature of the displacement field requires a large number of monomial terms before the interlaminar stresses are computed as accurately as the refined zigzag theory.

Slemp, Wesley C. H.↗
NASA NTRS2010

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↗