Sharif Digital Repository

The prevalence of complex Cyber-Physical Systems (CPS) as an increasingly ubiquitous technology, necessitates the incorporation of component based and compositional design methods for the development and deployment of such systems. In this paper, we introduce a hybrid coordination framework to specify CPSs with components and use the resulting models to simulate, validate and verify those systems, using UPPAAL statistical model checker (SMC). We use SMC because with a level of uncertainty and unpredictability (e.g., the physical environment with which a CPS interacts), simulation-based verification approaches, where properties are guaranteed with a degree of confidence, produce more... 

Software architectures and architectural styles are increasingly used for designing large-scale software systems. Alfa is a framework for the composition of style-based software architectures from a small set of primitives. It models the behavior of architectural components and connectors as orderings among events at their inputs and outputs. Formalizing such behavior is useful for checking conformance of architectures to their styles. We therefore propose a formal approach that uses data-abstract constraint automata to model the behavior of Alfa's compositions, and to verify their behavioral style conformance. We have also developed an automated conformance analyzer for Alfa. © 2004 IEEE  

Composition of a concurrent system out of components involves coordination of their mutual interactions. In component-based construction, this coordination becomes the responsibility of the glue-code language and its underlying run-time middle-ware. Reo offers an expressive glue-language for construction of coordinating component connectors out of primitive channels. In this paper we consider the problem of synthesizing Reo coordination code from a specification of a behavior as a relation on scheduled-data streams. The specification is given as a constraint automaton that describes the desired input/output behavior at the ports of the components. The main contribution in this paper is an... 

Continuous habitability of a planet is a critical condition for advanced forms of life to appear, but it can be endangered by astronomical events such as stellar encounters. The purpose of this study is to analyze close stellar encounters able to change planetary orbits initially in circumstellar habitable zones and to investigate the expected encounter rates in a variety of stellar environments. Using gravitational simulations for three-body systems, this study analyzed the dependencies of encounter impact-parameters with kinematic, geometric, and habitability parameters of the system. We also used kinematic properties of various stellar regions and estimated encounter rates of the events.... 

Reo is an exogenous coordination language for compositional construction of component connectors based on a calculus of channels. Building automated tools to address such concerns as equivalence or containment of the behavior of two given connectors, verification of the behavior of a connector, etc. requires an operational semantic model suitable for model checking. In this paper we introduce constraint automata and propose them as a semantic model for Reo. © 2004 Elsevier B.V. All rights reserved  

In recent years, the fabrication of nanoparticles and exploration of their properties have attracted the attention of physicists, chemists, biologists and engineers. Interest in nanoparticles arise from the fact that the mechanical, chemical, electrical, optical, magnetic, electro-optical and magneto-optical properties of these particles are different from their bulk properties and depend on the particle size. There are numerous areas where nanoparticulate systems are of scientific and technological interest. This new book reviews research on the various components of superparamagnetic iron oxide nanoparticles  

Comparison of the traditional linear heating method of TPD with an original stepwise heating scheme was reported for the first time. Stepwise heating TPD was carried out by keeping the temperature constant as soon as ammonia desorption signal rises until the signal returns to the baseline. More ammonia desorption peaks on a SAPO-34 catalyst were identified using TPD with stepwise heating. The effect of temperature ramp on desorption peak broadening in TPD curve was also addressed. The more distinct ammonia desorption peaks in stepwise TPD indicates that ammonia adsorbs in about five or six different ways on SAPO-34, and attribution of different adsorptions may be explained considering some... 

Most part of Iran is dominated by arid and semi-arid areas due to low annual rainfall. The need for production of fresh water from brackish water is considerably high, especially in dry regions. In this study 1 month daily-based experimental data from a solar still site has been reported. The technical and operational problems of this site which finally contributed to the total cease of the site are described. Then a detailed analysis is investigated on progress of a prototype which constructed in order to solve the site's problems. The results of 1 month of experimental data of the final design showed that the last prototype could be used to solve the current problems of the site. The... 

Hydrocracking is one of the most versatile petroleum refining processes for production of valuable products including gasoline, gas oil, and jet fuel. In this paper, a five-parameter continuous lumping model was used for kinetic modeling of hydrocracking of vacuum gas oil (VGO). The model parameters were estimated from industrial data obtained from a fixed bed reactor operating at an average temperature of 400°C and residence time of 0.3 h. Product distributions were obtained in terms of the weight fraction of various boiling point cuts. The model parameters were estimated using the Nelder-Mead optimization procedure and were correlated with temperature. Comparison of experimental and... 

Purpose - The purpose of this paper is to present an improved methodology for design of custom-made hip prostheses, through integration of advanced image processing, computer aided design (CAD) and additive manufacturing (AM) technologies. Design/methodology/approach - The proposed methodology for design of custom-made hip prostheses is based on an independent design criterion for each of the intra-medullary and extra-medullary portions of the prosthesis. The intra-medullar part of the prosthesis is designed using a more accurate and detailed description of the 3D geometry of the femoral intra-medullary cavity, including the septum calcar ridge, so that an improved fill and fit performance... 

In this letter, we propose a method for real-time high density impulse noise suppression from images. In our method, we first apply an impulse detector to identify the corrupted pixels and then employ an innovative weighted-average filter to restore them. The filter takes the nearest neighboring interpolated image as the initial image and computes the weights according to the relative positions of the corrupted and uncorrupted pixels. Experimental results show that the proposed method outperforms the best existing methods in both PSNR measure and visual quality and is quite suitable for real-time applications  

The disposal of used tires is a major environmental problem. With increasing interest on recovery of wastes, pyrolysis is considered as an alternative process for recovering some of the value in scrap tires. An accurate kinetic model is required to predict product yields during thermal or catalytic pyrolysis of scrap tires. Pyrolysis products contain a variety of hydrocarbons over a wide boiling range. A common approach for kinetic modeling of such complex systems is lumping where each lump is defined by a boiling point range. Available experimental data for thermal and catalytic pyrolysis of scrap tires from the literature were used to evaluate two types of lumping models; discrete and... 

Compared with flat linear structures, tubular linear machines do not face edge effects, making their performance better than their flat counterparts. In this article, a novel linear variable-reluctance resolver with tubular configuration is proposed. To optimize the design of an electromagnetic structure, modeling methods are used. Thus, in this article, an analytical model for the proposed resolver is presented. This model is based on the magnetic equivalent circuit (MEC) method and is considerably less time-consuming than finite element analysis (FEA), yet provides accurate results. A conformal mapping is employed to compute the permeance of the air-gap. The proposed model is then utilized... 

In Brukner and Zeilinger's interpretation of quantum mechanics, information is introduced as the most fundamental notion and the finiteness of information is considered as an essential feature of quantum systems. They also define a new measure of information which is inherently different from the Shannon information and try to show that the latter is not useful in defining the information content in a quantum object. Here, we show that there are serious problems in their approach which make their efforts unsatisfactory. The finiteness of information does not explain how objective results appear in experiments and what an instantaneous change in the so-called information vector (or catalog of... 

Low silicon content SAPO-34 was successfully synthesized using the conventional hydrothermal crystallization in the static condition. Effects of different synthesis conditions including crystallization temperature and the silicon source were investigated through X-ray diffraction patterns. It was concluded that the silicon source had a significant effect on silicon incorporation into the alumino-phosphate building blocks in the course of crystallization. Using precipitated silica instead of silica sol resulted in the formation of impurities of alumino-phosphates phases whose crystalline structures collapse at the high temperature of calcination. For the low silicon SAPO-34 synthesis, the... 

Let R be a left Noetherian ring and ZD(R) be the set of all zero-divisors of R. In this paper, it is shown that if RZD(R) is finite, then R is finite