154 research outputs found
Dynamic analysis of Cyber-Physical Systems
No full textWith the recent advances in communication and computation technologies, integration of software into the sensing, actuation, and control is common. This has lead to a new branch of study called Cyber-Physical Systems (CPS). Avionics, automotives, power grid, medical devices, and robotics are a few examples of such systems. As these systems are part of critical infrastructure, it is very important to ensure that these systems function reliably without any failures. While testing improves confidence in these systems, it does not establish the absence of scenarios where the system fails. The focus of this thesis is on formal verification techniques for cyber-physical systems that prove the absence of errors in a given system. In particular, this thesis focuses on {\em dynamic analysis} techniques that bridge the gap between testing and verification.
This thesis uses the framework of hybrid input output automata for modeling CPS. Formal verification of hybrid automata is undecidable in general.
Because of the undecidability result, no algorithm is guaranteed to terminate for all models.
This thesis focuses on developing heuristics for verification that exploit sample executions of the system. Moreover, the goal of the dynamic analysis techniques proposed in this thesis is to ensure that the techniques are sound, i.e., they always return the right answer, and they are relatively complete, i.e., the techniques terminate when the system satisfies certain special conditions. For undecidable problems, such theoretical guarantees are the strongest that can be expected out of any automatic procedure. This thesis focuses on safety properties, which require that nothing bad happens. In particular we consider invariant and temporal precedence properties; temporal precedence properties ensure that the temporal ordering of certain events in every execution satisfy a given specification.
This thesis introduces the notion of a discrepancy function that aids in dynamic analysis of CPS. Informally, these discrepancy functions capture the convergence or divergence of continuous behaviors in CPS systems. In control theory, several proof certificates such as contraction metric and incremental stability have been proposed to capture the convergence and divergence of solutions of ordinary differential equations. This thesis establishes that discrepancy functions generalize such proof certificates. Further, this thesis also proposes a new technique to compute discrepancy functions for continuous systems with linear ODEs from sample executions.
One of the main contributions of this thesis is a technique to compute an over-approximation of the set of reachable states using sample executions and discrepancy functions. Using the reachability computation technique, this thesis proposes a safety verification algorithm which is proved to be sound and relatively complete. This technique is implemented in a tool called, Compare-Execute-Check-Engine (C2E2) and experimental results show that it is scalable.
To demonstrate the applicability of the algorithms presented, two challenging case studies are analyzed as a part of this thesis. The first case study is about an alerting mechanism in parallel aircraft landing. For performing this case study, the dynamic analysis presented for invariant verification is extended to handle temporal properties. The second case study is about verifying key specification of powertrain control system. New algorithms for computing discrepancy function were implemented in C2E2 for performing this case study. Both these case studies demonstrate that dynamic analysis technique gives promising results and can be applied to realistic CPS.
For distributed CPS implementations, where message passing, and clocks skews between agents make formal verification difficult to scale, this thesis presents a dynamic analysis algorithm for inferring global predicates. Such global predicates include assertions about the physical state and the software state of all the agents involved in distributed CPS. This algorithm is applied to coordinated robotic maneuvers for inferring safety and detecting deadlock.Submission published under a 24 month embargo labeled 'U of I Access', the embargo will last until 2017-12-01The student, Parasara Duggirala, accepted the attached license on 2015-08-20 at 10:16.The student, Parasara Duggirala, submitted this Dissertation for approval on 2015-08-20 at 10:54.This Dissertation was approved for publication on 2015-08-21 at 13:11.DSpace SAF Submission Ingestion Package generated from Vireo submission #8666 on 2016-03-02 at 14:04:58Made available in DSpace on 2016-03-02T20:23:09Z (GMT). No. of bitstreams: 2
DUGGIRALA-DISSERTATION-2015.pdf: 2270763 bytes, checksum: 63944415a1f1fed543c62474d21590db (MD5)
LICENSE.txt: 4215 bytes, checksum: 29986d33485b5c4e13f44edf60ca57ef (MD5)
Previous issue date: 2015-08-21Embargo set by: Seth Robbins for item 91306
Lift date: 2018-03-02T20:24:31Z
Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD systemU of I Only Restriction Lifted for Item 91306 on 2018-03-03T10:15:18Z
Computational Fluid Dynamics Simulation Of Chemically Reacting Gas Flows Through Microfibrous Materials
No full textThis dissertation presents results of research efforts to propose a design space for new microfibrous materials with enhanced chemical
reactivity with optimum pressure gradient. These microfibrous materials material are a new class of patented materials, consisting of catalytic particles (50-300 micron in size) entrapped in a matrix of microfibers (2-10 micron in size), which show enhanced chemical reactivity compared to packed beds. Computational Fluid Dynamics
(CFD) was used as a design tool to analyze the flow through microfibrous materials and to investigate the underlying mechanisms behind the enhancement in chemical reactivity. Numerical experiments were performed using different materials such as packed beds, frozen beds (particles frozen in space), and microfibrous materials with different geometric properties for two gas phase applications: (1) desulfurization, where a challenge gas of 2 vol.% H2S in H2
is used at a temperature of 400 0C and ZnO/SiO2 is used for desulfurization, and (2) removal of trace amounts of hexane (100 ppmv of C6H14) from air.
Pressure drops were predicted using CFD and are in good agreement with experiments, even with significant geometric approximations. The effects of residence time, dilution with void, clustering, fiber diameter, and fibers loading on chemical conversion are studied. Dilution with void and clustering showed a negative effect on chemical conversion compared with packed bed. Adding fibers enhanced the chemical reactivity by providing more uniform, plug flow like conditions, even in the presence of dilution. Microfibrous materials with more numerous smaller diameter fibers are required to have enhanced chemical conversion when pressure drop is not important with a maximum factor of increase in chemical reactivity for these cases (60-80%). Another design criteria is investigated by comparing the ratio of log reduction to pressure drop (using the same amount of catalyst) for different materials. This work suggests that new microfibrous materials with enhanced chemical reactivity for a given pressure drop should be designed with fewer, larger diameter fibers. Maxima increases in chemical reactivity per pressure drop of 8 and 6 were found for H2S and hexane, respectively, using 8 micron diameter fibers at 3% volume fraction with a total voidage of 80%
Multivariate Cryptography with Mappings of Discrete Logarithms and Polynomials
No full textIn this paper, algorithms for multivariate public key cryptography and digital signature are described. Plain messages and encrypted messages are arrays, consisting of elements from a fixed finite ring or field. The encryption and decryption algorithms are based on multivariate mappings. The security of the private key depends on the difficulty of solving a system of parametric simultaneous multivariate equations involving polynomial or exponential mappings. The method is a general purpose utility for most data encryption, digital certificate or digital signature applications. For security protocols of the application layer level in the OSI model, the methods described in this paper are useful
Double diffusive convection during solidification of ammonium chloride - water (NH4CL-H20) mixture in a trapezoidal cavity
No full textThe effect of the initial concentration of ammonium chloride (sub eutectic: C \u3c 19.8 wt. % and eutectic Ce= 19.8 wt. %) and boundary temperatures (Tcold = -30 0C to -10 0C) on the solidification process is examined. Particle Image Velocimetry (PIV) is used in this study to measure the velocity fields in the melt during the solidification process. The distributions of temperatures at discrete locations in the solution and the boundary walls were measured. This study focuses on the solidification of an ammonium chloride-water (NH4Cl- H2O) solution in a trapezoidal cavity with one and two inclined cooling walls.
The thermosolutal convective flow strongly influenced the rate of freezing. An increase in thermal driving force increased the rate of freezing. Increased initial concentration retarded the freezing process and primarily affected the structure of the solid and mush regions.
The results of this study will contribute in understanding the phenomena and bridge the gap between the engineering aspect and physics background for the dynamics of solid phase formation during castings, ingots, and polymerization
Double diffusive convection during solidification of ammonium chloride - water (NH4CL-H20) mixture in a trapezoidal cavity
No full textMultivariate Polynomial and Exponential Mappings based Password Authentication Protocol
No full textIn this paper, a multivariate polynomial and exponential mappings based password protocol is presented. The method can be utilized in public domains. The key generator generates a vector, intended to be used as a password by the authentication protocol subsequently, such that when the vector is substituted and evaluated in certain fixed multivariate polynomials -- that may be listed in a public domain -- the value is found as a result of proper authentication. The public domain in this context could be internal to a large, and possibly distributed, system. The key generator can take hints from the owner of the password to generate the particular zero vector to suit the user. It may take into consideration biometric and any other user specific information at the time of key generation. The information collected by the key generator can be saved by the owner of the password for its possible retrieval upon requisition by the user, during the period of its validity, in case it is forgotten by the user
A Knowledge-Based Engineering Method to Integrate Metal Forming Process Design and Simulation
No full text
- …
