Reusable formal architectures for networked systems

Today's networked systems are becoming increasingly complex and diverse. The current simulation and runtime verification techniques do not provide support for developing such systems efficiently; moreover, the reliability of the simulated/verified systems is not thoroughly ensured. To address these challenges, the use of formal techniques to reason about network system development is growing, while at the same time, the mathematical background necessary for using formal techniques is a barrier for network designers to efficiently employ them. Thus, these techniques are not vastly used for developing networked systems. The objective of this thesis is to propose formal approaches for the development of reliable networked systems, by taking efficiency into account. With respect to reliability, we propose the architectural development of correct-by-construction networked system models. With respect to efficiency, we propose reusable network architectures as well as network development. At the core of our development methodology, we employ the abstraction and refinement techniques for the development and analysis of networked systems. We evaluate our proposal by employing the proposed architectures to a pervasive class of dynamic networks, i.e., wireless sensor network architectures as well as to a pervasive class of static networks, i.e., network-on-chip architectures. The ultimate goal of our research is to put forward the idea of building libraries of pre-proved rules for the efficient modelling, development, and analysis of networked systems. We take into account both qualitative and quantitative analysis of networks via varied formal tool support, using a theorem prover the Rodin platform and a statistical model checker the SMC-Uppaal.

A simulation model of the optimal maintenance strategy: conceptual agent-based approach

In this Master’s thesis agent-based modeling has been used to analyze maintenance strategy related phenomena. The main research question that has been answered was: what does the agent-based model made for this study tell us about how different maintenance strategy decisions affect profitability of equipment owners and maintenance service providers? Thus, the main outcome of this study is an analysis of how profitability can be increased in industrial maintenance context. To answer that question, first, a literature review of maintenance strategy, agent-based modeling and maintenance modeling and optimization was conducted. This review provided the basis for making the agent-based model. Making the model followed a standard simulation modeling procedure. With the simulation results from the agent-based model the research question was answered. Specifically, the results of the modeling and this study are: (1) optimizing the point in which a machine is maintained increases profitability for the owner of the machine and also the maintainer with certain conditions; (2) time-based pricing of maintenance services leads to a zero-sum game between the parties; (3) value-based pricing of maintenance services leads to a win-win game between the parties, if the owners of the machines share a substantial amount of their value to the maintainers; and (4) error in machine condition measurement is a critical parameter to optimizing maintenance strategy, and there is real systemic value in having more accurate machine condition measurement systems.

Kinematic analysis and modelling of biped locomotion systems

This paper presents the kinematic study of robotic biped locomotion systems. The main purpose is to determine the kinematic characteristics and the system performance during walking. For that objective, the prescribed motion of the biped is completely characterised in terms of five locomotion variables: step length, hip height, maximum hip ripple, maximum foot clearance and link lengths. In this work, we propose four methods to quantitatively measure the performance of the walking robot: energy analysis, perturbation analysis, lowpass frequency response and locomobility measure. These performance measures are discussed and compared in determining the robustness and effectiveness of the resulting locomotion.

Advances in modelling of mechatronic systems: the toolset FASIM_C++ for the simulation of vehicle dynamics

The increasing complexity of controller systems, applied in modern passenger cars, requires adequate simulation tools. The toolset FASIM_C++, described in the following, uses complex vehicle models in three-dimensional vehicle dynamics simulation. The structure of the implemented dynamic models and the generation of the equations of motion applying the method of kinematic differentials is explained briefly. After a short introduction in methods of event handling, several vehicle models and applications like controller development, roll-over simulation and real-time-simulation are explained. Finally some simulation results are presented.

A frequency-domain pseudo-force method for dynamic structural analysis nonlinear systems and nonproportional damping

A frequency-domain method for nonlinear analysis of structural systems with viscous, hysteretic, nonproportional and frequency-dependent damping is presented. The nonlinear effects and nonproportional damping are considered through pseudo-force terms. The modal coordinates uncoupled equations are iteratively solved. The treatment of initial conditions in the frequency domain which is necessary for the treatment of the uncoupled equations is initially adressed.

Object-oriented Programming Applied to the Development of Structural Analysis and Optimization Software

This paper presents the development of a two-dimensional interactive software environment for structural analysis and optimization based on object-oriented programming using the C++ language. The main feature of the software is the effective integration of several computational tools into graphical user interfaces implemented in the Windows-98 and Windows-NT operating systems. The interfaces simplify data specification in the simulation and optimization of two-dimensional linear elastic problems. NURBS have been used in the software modules to represent geometric and graphical data. Extensions to the analysis of three-dimensional problems have been implemented and are also discussed in this paper.

Testing and simulation of fractionary electromechanical rotative drives

This paper concerns the development of drives that use electromechanical rotative motor systems. It is proposed an experimental drive test structure integrated to simulation softwares. The objective of this work is to show that an affordable model validation procedure can be obtained by combining a precision data acquisition with well tuned state-of-the-art simulation packages. This is required for fitting, in the best way, a drive to its load or, inversely, to adapt loads to given drive characteristics.

Dynamic Analysis Model of Spherical Roller Bearings with Defects

Rolling element bearings are essential components of rotating machinery. The spherical roller bearing (SRB) is one variant seeing increasing use, because it is self-aligning and can support high loads. It is becoming increasingly important to understand how the SRB responds dynamically under a variety of conditions. This doctoral dissertation introduces a computationally efficient, three-degree-of-freedom, SRB model that was developed to predict the transient dynamic behaviors of a rotor-SRB system. In the model, bearing forces and deflections were calculated as a function of contact deformation and bearing geometry parameters according to nonlinear Hertzian contact theory. The results reveal how some of the more important parameters; such as diametral clearance, the number of rollers, and osculation number; influence ultimate bearing performance. Distributed defects, such as the waviness of the inner and outer ring, and localized defects, such as inner and outer ring defects, are taken into consideration in the proposed model. Simulation results were verified with results obtained by applying the formula for the spherical roller bearing radial deflection and the commercial bearing analysis software. Following model verification, a numerical simulation was carried out successfully for a full rotor-bearing system to demonstrate the application of this newly developed SRB model in a typical real world analysis. Accuracy of the model was verified by comparing measured to predicted behaviors for equivalent systems.

Further analysis of open-respirometry systems: an a-compartmental mechanistic approach

A system is said to be "instantaneous" when for a given constant input an equilibrium output is obtained after a while. In the meantime, the output is changing from its initial value towards the equilibrium one. This is the transient period of the system and transients are important features of open-respirometry systems. During transients, one cannot compute the input amplitude directly from the output. The existing models (e.g., first or second order dynamics) cannot account for many of the features observed in real open-respirometry systems, such as time lag. Also, these models do not explain what should be expected when a system is speeded up or slowed down. The purpose of the present study was to develop a mechanistic approach to the dynamics of open-respirometry systems, employing basic thermodynamic concepts. It is demonstrated that all the main relevant features of the output dynamics are due to and can be adequately explained by a distribution of apparent velocities within the set of molecules travelling along the system. The importance of the rate at which the molecules leave the sensor is explored for the first time. The study approaches the difference in calibrating a system with a continuous input and with a "unit impulse": the former truly reveals the dynamics of the system while the latter represents the first derivative (in time) of the former and, thus, cannot adequately be employed in the apparent time-constant determination. Also, we demonstrate why the apparent order of the output changes with volume or flow.

Analysis and modelling of chemical looping combustion process with and without oxygen uncoupling

Effective control and limiting of carbon dioxide (CO₂) emissions in energy production are major challenges of science today. Current research activities include the development of new low-cost carbon capture technologies, and among the proposed concepts, chemical combustion (CLC) and chemical looping with oxygen uncoupling (CLOU) have attracted significant attention allowing intrinsic separation of pure CO₂ from a hydrocarbon fuel combustion process with a comparatively small energy penalty. Both CLC and CLOU utilize the well-established fluidized bed technology, but several technical challenges need to be overcome in order to commercialize the processes. Therefore, development of proper modelling and simulation tools is essential for the design, optimization, and scale-up of chemical looping-based combustion systems. The main objective of this work was to analyze the technological feasibility of CLC and CLOU processes at different scales using a computational modelling approach. A onedimensional fluidized bed model frame was constructed and applied for simulations of CLC and CLOU systems consisting of interconnected fluidized bed reactors. The model is based on the conservation of mass and energy, and semi-empirical correlations are used to describe the hydrodynamics, chemical reactions, and transfer of heat in the reactors. Another objective was to evaluate the viability of chemical looping-based energy production, and a flow sheet model representing a CLC-integrated steam power plant was developed. The 1D model frame was succesfully validated based on the operation of a 150 kWth laboratory-sized CLC unit fed by methane. By following certain scale-up criteria, a conceptual design for a CLC reactor system at a pre-commercial scale of 100 MWth was created, after which the validated model was used to predict the performance of the system. As a result, further understanding of the parameters affecting the operation of a large-scale CLC process was acquired, which will be useful for the practical design work in the future. The integration of the reactor system and steam turbine cycle for power production was studied resulting in a suggested plant layout including a CLC boiler system, a simple heat recovery setup, and an integrated steam cycle with a three pressure level steam turbine. Possible operational regions of a CLOU reactor system fed by bituminous coal were determined via mass, energy, and exergy balance analysis. Finally, the 1D fluidized bed model was modified suitable for CLOU, and the performance of a hypothetical 500 MWth CLOU fuel reactor was evaluated by extensive case simulations.

Formal development of resilient distributed systems

Resilience is the property of a system to remain trustworthy despite changes. Changes of a different nature, whether due to failures of system components or varying operational conditions, significantly increase the complexity of system development. Therefore, advanced development technologies are required to build robust and flexible system architectures capable of adapting to such changes. Moreover, powerful quantitative techniques are needed to assess the impact of these changes on various system characteristics. Architectural flexibility is achieved by embedding into the system design the mechanisms for identifying changes and reacting on them. Hence a resilient system should have both advanced monitoring and error detection capabilities to recognise changes as well as sophisticated reconfiguration mechanisms to adapt to them. The aim of such reconfiguration is to ensure that the system stays operational, i.e., remains capable of achieving its goals. Design, verification and assessment of the system reconfiguration mechanisms is a challenging and error prone engineering task. In this thesis, we propose and validate a formal framework for development and assessment of resilient systems. Such a framework provides us with the means to specify and verify complex component interactions, model their cooperative behaviour in achieving system goals, and analyse the chosen reconfiguration strategies. Due to the variety of properties to be analysed, such a framework should have an integrated nature. To ensure the system functional correctness, it should rely on formal modelling and verification, while, to assess the impact of changes on such properties as performance and reliability, it should be combined with quantitative analysis. To ensure scalability of the proposed framework, we choose Event-B as the basis for reasoning about functional correctness. Event-B is a statebased formal approach that promotes the correct-by-construction development paradigm and formal verification by theorem proving. Event-B has a mature industrial-strength tool support { the Rodin platform. Proof-based verification as well as the reliance on abstraction and decomposition adopted in Event-B provides the designers with a powerful support for the development of complex systems. Moreover, the top-down system development by refinement allows the developers to explicitly express and verify critical system-level properties. Besides ensuring functional correctness, to achieve resilience we also need to analyse a number of non-functional characteristics, such as reliability and performance. Therefore, in this thesis we also demonstrate how formal development in Event-B can be combined with quantitative analysis. Namely, we experiment with integration of such techniques as probabilistic model checking in PRISM and discrete-event simulation in SimPy with formal development in Event-B. Such an integration allows us to assess how changes and di erent recon guration strategies a ect the overall system resilience. The approach proposed in this thesis is validated by a number of case studies from such areas as robotics, space, healthcare and cloud domain.

Sugarcane spirit market share simulation: an application of conjoint analysis

This study evaluated the influence of packaging and labeling attributes of sugarcane spirit on consumers' behavior by applying the results of conjoint analysis in sugarcane spirit market share simulation. Firstly, a conjoint analysis was performed aiming to estimate the part-worths of each consumer for some sugarcane spirit packaging and labeling attributes. These part-worths were used in the market share simulation using the maximum utility model. It was observed that some packaging and labeling attributes affected consumer's purchase intention and that most consumers showed a similar preference pattern regarding these attributes. These consumers showed preference for the Seleta brand, which was bottled in 700 mL clear glass bottles with a metal screw cap that bore a label illustration unrelated to sugarcane spirit production process and had the information "aged 36 months in oak barrels". This study also showed that conjoint analysis and the use of its results in the market share simulation proved important tools to better understand consumer behavior towards intention to purchase sugarcane spirit.