We present studies on squeeze film effects in dynamic MEMS devices with a special emphasis on the development of compact analytical models. First, the efficacy of lumped parameter modelling of dynamic MEMS devices is illustrated in MATLAB/SIMULINK software environment using a MEMS gyroscope and a MEMS microphone as examples. This is followed by a comparative study of equivalent electrical circuit models for a MEMS microphone wherein the importance of accurate extraction of lumped mass, stiffness and damping is brought into focus. In this context, a need for an in depth study of squeeze film behaviour in MEMS structures is highlighted and a strong motivation is drawn for the development of compact squeeze film models. A 2D analytical model for estimating squeeze film damping and spring force in perforated MEMS structures is presented. The governing equations based on isothermal compressible Reynolds equation are derived by considering an approximate circular pressure cell around a hole which is representative of the spatially invariant pressure pattern over the interior of the flow domain. The advantages and limitations of the solution are discussed with relevance to MEMS structures. Next, a comprehensive analytical model for 3D MEMS structures that includes effects of compressibility, inertia, and rarefaction in the flow between two parallel plates forming the squeeze region as well as the flow through perforations is developed. A modified Reynolds equation that includes the unsteady inertial term is derived from the Navier-Stokes equation to model the flow in the circular cell and the losses through the holes are modelled using Poiseuille flow. Rarefaction effects in the flow through the air-gap as well as the holes are accounted for by considering the slip boundary conditions. The analytical results are compared with extensive numerical simulations carried out using full 3-D Navier-Stokes equation solver in a commercial simulation package (ANSYS-CFX). We show that the analytical solution performs very well in tracking the net force up to the first resonant frequency of the entrapped air.

Since the first lines of code were introduced in the automotive domain, vehicles have transitioned from being predominantly mechanical systems to software intensive systems. With the ever-increasing computational power and memory of vehicular embedded systems, a set of new, more powerful and more complex software functions are installed into vehicles to realize core functionalities. This trend impacts all phases of the system development including requirements specification, design and architecture of the system, as well as the integration and testing phases. In such settings, creating and managing different artifacts during the system development process by using traditional, human-intensive techniques becomes increasingly difficult. One problem stems from the high number and intricacy of system requirements that combine functional and possibly timing or other types of constraints. Another problem is related to the fact that industrial development relies on models, e.g. developed in Simulink, from which code may be generated, so the correctness of such models needs to be ensured. A potential way to address of the mentioned problems is by applying computer-aided specification, analysis and verification techniques already at the requirements stage, but also further at later development stages. Despite the high degree of automation, exhaustiveness and rigor of formal specification and analysis techniques, their integration with industrial practice remains a challenge. To address this challenge, in this thesis, we develop the foundation of a framework, tailored for industrial adoption, for formal specification and analysis of system requirements specifications and behavioral system models. First, we study the expressiveness of existing pattern-based techniques for creating formal requirements specifications, on a relevant industrial case study. Next, in order to enable practitioners to create formal system specification by using pattern-based techniques, we propose a tool called SeSAMM Specifier. Further, we provide an automated Satisfiability Modulo Theories (SMT)-based consistency analysis approach for the formally encoded system requirements specifications. The proposed SMT-based approach is suitable for early phases of the development for debugging the specifications. For the formal analysis of behavioral models, we provide an approach for statistical model checking of Simulink models by using the UPPAAL SMC tool. To facilitate the adoption of the approach, we provide the SIMPPAAL tool that automates procedure of generating network of stochastic timed automata for a given Simulink model. For validation, we apply our approach on a complex industrial model, namely the Brake-by-Wire function from Volvo GTT. / VeriSpec

No description available.