Search results for: Markus Schubert

Authors: Stoyan Nedeltchev, Markus Schubert

Abstract:

The gas holdup fluctuations in a bubble column (0.15 m in ID) have been recorded by means of a conductivity wire-mesh sensor in order to extract information about the main transition velocities. These parameters are very important for bubble column design, operation and scale-up. For this purpose, the classical definition of the Shannon entropy was modified and used to identify both the onset (at U_G=0.034 m/s) of the transition flow regime and the beginning (at U_G=0.089 m/s) of the churn-turbulent flow regime. The results were compared with the Kolmogorov entropy (KE) results. A slight discrepancy was found, namely the transition velocities identified by means of the KE were shifted to somewhat higher (0.045 and 0.101 m/s) superficial gas velocities U_G.

Keywords: Bubble column, gas holdup fluctuations, Modified Shannon entropy, Kolmogorov entropy.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1649

Authors: Stoyan Nedeltchev, Markus Schubert

Abstract:

By means of the ultrafast X-ray tomography facility, data were obtained at different superficial gas velocities U_G in a bubble column (0.1 m in ID) operated with an air-deionized water system at ambient conditions. Raw reconstructed images were treated by both the information entropy (IE) and the reconstruction entropy (RE) algorithms in order to identify the main transition velocities in a bubble column. The IE values exhibited two well-pronounced minima at U_G=0.025 m/s and U_G=0.085 m/s identifying the boundaries of the homogeneous, transition and heterogeneous regimes. The RE extracted from the central region of the column’s cross-section exhibited only one characteristic peak at U_G=0.03 m/s, which was attributed to the transition from the homogeneous to the heterogeneous flow regime. This result implies that the transition regime is non-existent in the core of the column.

Keywords: Bubble column, ultrafast X-ray tomography, information entropy, reconstruction entropy.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1480

Authors: Maria de Fátima Lambert

Abstract:

Following previous studies about Writing and Seeing, this paper focuses on the aesthetic assumptions within the concept of Winter Journey (Voyage d’Hiver/Winterreise) both in Georges Perec’s Saga and the Oulipo Group vis-à-vis with the creations by William Kentridge and Michael Borremans. The aesthetic and artistic connections are widespread. Nevertheless, we can identify common poetical principles shared by these different authors, not only according to the notion of ekphrasis, but also following the procedures of contemporary creation in literature and visual arts. The analysis of the ongoing process of the French writers as individuals and as group and the visual artists’ acting might contribute for another crossed definition of contemporary conception. The same title/theme was a challenge and a goal for them. Let’s wonder how deep the concept encouraged them and which symbolic upbringings were directing their poetical achievements. The idea of an inner journey became the main point, and got “over” and “across” a shared path worth to be followed. The authors were chosen due to the resilient contents of their visual and written images, and looking for the reasons that might had driven their conceptual basis to be. In Pérec’s “Winter Journey” as for the following fictions by Jacques Roubaud, Hervé le Tellier, Jacques Jouet and Hugo Vernier (that emerges from Perec’s fiction and becomes a real author) powerful aesthetic and enigmatic reflections grow connected with a poetic (and aesthetic) understanding of Walkscapes. They might be assumed as ironic fictions and poetical drifts. Outstanding from different logics, the overwhelming impact of Winterreise Lied by Schubert after Wilhelm Müller’s poems is a major reference in present authorship creations. Both Perec and Oulipo’s author’s texts are powerfully ekphrastic, although we should not forget they follow goals, frameworks and identities. When acting as a reader, they induce powerful imageries - cinematic or cinematographic - that flow in our minds. It was well-matched with William Kentridge animated video Winter Journey (2014) and the creations (sharing the same title) of Michael Borremans (2014) for the KlaraFestival, Bozar, Cité de la musique, in Belgium. Both were taken by the foremost Schubert’s Winterreise. Several metaphors fulfil new Winter Journeys (or Travels) that were achieved in contemporary art and literature, as it once succeeded in the 19^th century. Maybe the contemporary authors and artists were compelled by the consciousness of nothingness, although outstanding different aesthetics and ontological sources. The unbearable knowledge of the road’s end, and also the urge of fulfilling the void might be a common element to all of them. As Schopenhauer once wrote, after all, Art is the only human subjective power that we can call upon in life. These newer aesthetic meanings, released from these winter journeys are surely open to wider approaches that might happen in other poetic makings to be.

Keywords: Aesthetic, Voyage d’Hiver, Georges Perec & Oulipo, Schubert's Winterreise, William Kentridge & Michael Borremans.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 386

Authors: M. Liebherr, P. Schubert, S. Kersten, C. Dietz, L. Franz, C. T. Haas

Abstract:

With a long history, dual-task has become one of the most intriguing research fields regarding human brain functioning and cognition. However, findings considering effects of taskinterrelations are limited (especially, in combined motor and cognitive tasks). Therefore, we aimed at developing a measurement system in order to analyse interrelation effects of cognitive and motor tasks. On the one hand, the present study demonstrates the applicability of the measurement system and on the other hand first results regarding a systematisation of different task combinations are shown. Future investigations should combine imagine technologies and this developed measurement system.

Keywords: Dual-task, interference, cognition, measurement.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2041

Authors: Markus Siepermann, Christoph Siepermann

Abstract:

This paper presents the concept and realisation of an e-learning tool that provides predefined or automatically generated exercises concerning logistics cost accounting. Students may practise where and whenever they like to via the Internet. Their solutions are marked automatically by the tool while considering consecutive faults and without any intervention of lecturers.

Keywords: Automatic marking, e-learning environment, onlinepracticing, randomly-generated exercises.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1521

Authors: Jindong Gu, Matthias Schubert, Volker Tresp

Abstract:

In many outlier detection tasks, only training data belonging to one class, i.e., the positive class, is available. The task is then to predict a new data point as belonging either to the positive class or to the negative class, in which case the data point is considered an outlier. For this task, we propose a novel corrupted Generative Adversarial Network (CorGAN). In the adversarial process of training CorGAN, the Generator generates outlier samples for the negative class, and the Discriminator is trained to distinguish the positive training data from the generated negative data. The proposed framework is evaluated using an image dataset and a real-world network intrusion dataset. Our outlier-detection method achieves state-of-the-art performance on both tasks.

Keywords: Outlier detection, generative adversary networks, semi-supervised learning.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1010

Authors: Markus Reichhartinger, Martin Horn

Abstract:

In this paper, the position control of an electronic throttle actuator is outlined. The dynamic behavior of the actuator is described with the help of an uncertain plant model. This motivates the controller design based on the ideas of higher-order slidingmodes. As a consequence anti-chattering techniques can be omitted. It is shown that the same concept is applicable to estimate unmeasureable signals. The control law and the observer are implemented on an electronic control unit. Results achieved by numerical simulations and real world experiments are presented and discussed.

Keywords: higher order sliding-mode, throttle actuator, electromechanicalsystem, robust and nonlinear control.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1967

Authors: Loralee P. Potter, Peter J. Schubert

Abstract:

Solid-state hydrogen storage using catalytically-modified porous silicon can be rapidly charged at moderate pressures (8 bar) without exothermic runaway. Discharge requires temperatures of approximately 110oC, so for larger storage vessels a means is required for thermal energy to penetrate bulk storage media. This can be realized with low-density metal foams, such as Celmet™. This study explores several material and dimensional choices of the metal foam to produce rapid heating of bulk silicon particulates. Experiments run under vacuum and in a pressurized hydrogen environment bracket conditions of empty and full hydrogen storage vessels, respectively. Curve-fitting of the heating profiles at various distances from an external heat source is used to derive both a time delay and a characteristic time constant. System performance metrics of a hydrogen storage subsystem are derived from the experimental results. A techno-economic analysis of the silicon and metal foam provides comparison with other methods of storing hydrogen for mobile and portable applications. 

Keywords: conduction, convection, kinetics, fuel cell

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 596

Authors: Tero Halme, Juho Kanniainen, Markus Nordberg

Abstract:

According to the existing literature, companies manage analysts’ expectations of their future earnings by issuing pessimistic earnings guidance to meet the expectations. Consequently, one could expect that markets price this pessimistic bias in advance and penalize companies more for lowering the guidance than reward for beating the guidance. In this paper we confirm this empirically. In addition we show that although guidance revisions have a statistically significant relation to stock returns, that is not the case with the actual earnings surprise. Reason for this could be that, after the annual earnings report also information on future earnings power is given at the same time.

Keywords: Management guidance, earnings guidance, pessimistic bias

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2963

Authors: Sebastian Kusch, Markus Kaiser

Abstract:

In this paper we analyze the application of a formal proof system to the discrete logarithm problem used in publickey cryptography. That means, we explore a computer verification of the ElGamal encryption scheme with the formal proof system Isabelle/HOL. More precisely, the functional correctness of this algorithm is formally verified with computer support. Besides, we present a formalization of the DSA signature scheme in the Isabelle/HOL system. We show that this scheme is correct what is a necessary condition for the usefulness of any cryptographic signature scheme.

Keywords: Formal proof system, higher-order logic, formal verification, cryptographic signature scheme.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1514

Authors: Sarah E. Stief, Anne Theresa Eidhoff, Markus Voeth

Abstract:

Despite all progress firms are facing the increasing need to adapt and assimilate digital technologies to transform their business activities in order to pursue business development. By using new digital technologies, firms can implement major business improvements in order to stay competitive and foster new growth potentials. The corresponding phenomenon of digital transformation has received some attention in previous literature in respect to industries such as media and publishing. Nevertheless, there is a lack of understanding of the concept and its organization within firms. With the help of twenty-three in-depth field interviews with German experts responsible for their company’s digital transformation, we examined what digital transformation encompasses, how it is organized and which opportunities and challenges arise within firms. Our results indicate that digital transformation is an inevitable task for all firms, as it bears the potential to comprehensively optimize and reshape established business activities and can thus be seen as a strategy of business development.

Keywords: Business development, digitalization, digital strategies, digital transformation.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 6170

Authors: Markus Reichhartinger, Martin Horn

Abstract:

In this paper, the application of sliding-mode control to a permanent-magnet synchronous motor (PMSM) is presented. The control design is based on a generic mathematical model of the motor. Some dynamics of the motor and of the power amplification stage remain unmodelled. This model uncertainty is estimated in realtime. The estimation is based on the differentiation of measured signals using the ideas of robust exact differentiator (RED). The control law is implemented on an industrial servo drive. Simulations and experimental results are presented and compared to the same control strategy without uncertainty estimation. It turns out that the proposed concept is superior to the same control strategy without uncertainty estimation especially in the case of non-smooth reference signals.

Keywords: sliding-mode control, Permanent-magnet synchronous motor, uncertainty estimation, robust exact differentiator.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2284

Authors: Markus Mazzola, Gunther Schaaf

Abstract:

A vehicle driving with an Adaptive Cruise Control System (ACC) is usually controlled decentrally, based on the information of radar systems and in some publications based on C2X-Communication (CACC) to guarantee stable platoons. In this paper we present a Model Predictive Control (MPC) design of a centralized, server-based ACC-System, whereby the vehicular platoon is modeled and controlled as a whole. It is then proven that the proposed MPC design guarantees asymptotic stability and hence string stability of the platoon. The Networked MPC design is chosen to be able to integrate system constraints optimally as well as to reduce the effects of communication delay and packet loss. The performance of the proposed controller is then simulated and analyzed in an LTE communication scenario using the LTE/EPC Network Simulator LENA, which is based on the ns-3 network simulator.

Keywords: Adaptive Cruise Control, Centralized Server, Networked Model Predictive Control, String Stability.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2786

Authors: Sannikumar Patel, Brian Nolan, Markus Hofmann, Philip Owende, Kunjan Patel

Abstract:

Sentiment analysis and opinion mining have become emerging topics of research in recent years but most of the work is focused on data in the English language. A comprehensive research and analysis are essential which considers multiple languages, machine translation techniques, and different classifiers. This paper presents, a comparative analysis of different approaches for multilingual sentiment analysis. These approaches are divided into two parts: one using classification of text without language translation and second using the translation of testing data to a target language, such as English, before classification. The presented research and results are useful for understanding whether machine translation should be used for multilingual sentiment analysis or building language specific sentiment classification systems is a better approach. The effects of language translation techniques, features, and accuracy of various classifiers for multilingual sentiment analysis is also discussed in this study.

Keywords: Cross-language analysis, machine learning, machine translation, sentiment analysis.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1601

Authors: Lars Laußat, Manfred Helmus, Kamil Szczesny, Markus König

Abstract:

As one result of the project “Reactive Construction Project Scheduling using Real Time Construction Logistic Data and Simulation”, a procedure for using data about uncertain resource availability assumptions in reactive scheduling processes has been developed. Prediction data about resource availability is generated in a formalized way using real-time monitoring data e.g. from auto-ID systems on the construction site and in the supply chains. The paper focusses on the formalization of the procedure for monitoring construction logistic processes, for the detection of disturbance and for generating of new and uncertain scheduling assumptions for the reactive resource constrained simulation procedure that is and will be further described in other papers.

Keywords: Auto-ID, Construction Logistic, Fuzzy, Monitoring, RFID, Scheduling.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1728

Authors: Tomas Duranik, Juraj Ruzbarsky, Markus Stopper

Abstract:

CONWIP (constant work-in-process) as a pull production system have been widely studied by researchers to date. The CONWIP pull production system is an alternative to pure push and pure pull production systems. It lowers and controls inventory levels which make the throughput better, reduces production lead time, delivery reliability and utilization of work. In this article a CONWIP pull production system was simulated. It was simulated push and pull planning system. To compare these systems via a production planning system (PPS) game were adjusted parameters of each production planning system. The main target was to reduce the total WIP and achieve throughput and delivery reliability to minimum values. Data was recorded and evaluated. A future state was made for real production of plastic components and the setup of the two indicators with CONWIP pull production system which can greatly help the company to be more competitive on the market.

Keywords: CONWIP, constant work in process, delivery reliability, hybrid production planning, PPS.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2218

Authors: Johannes Buchmann, Markus Kaiser

Abstract:

We decribe a formal specification and verification of the Rabin public-key scheme in the formal proof system Is-abelle/HOL. The idea is to use the two views of cryptographic verification: the computational approach relying on the vocabulary of probability theory and complexity theory and the formal approach based on ideas and techniques from logic and programming languages. The analysis presented uses a given database to prove formal properties of our implemented functions with computer support. Thema in task in designing a practical formalization of correctness as well as security properties is to cope with the complexity of cryptographic proving. We reduce this complexity by exploring a light-weight formalization that enables both appropriate formal definitions as well as eficient formal proofs. This yields the first computer-proved implementation of the Rabin public-key scheme in Isabelle/HOL. Consequently, we get reliable proofs with a minimal error rate augmenting the used database. This provides a formal basis for more computer proof constructions in this area.

Keywords: public-key encryption, Rabin public-key scheme, formalproof system, higher-order logic, formal verification.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1546

Authors: Clemens Pizzinini, Philipp Rosner, David Ziegler, Markus Lienkamp

Abstract:

Transportation is a constitutional part of most supply and value chains in modern economies. Smallholder farmers in rural Ethiopia face severe challenges along their supply and value chains. In particular, suitable, affordable, and available transport services are in high demand. To develop context-specific technical solutions, a problem-to-solution methodology based on the interaction with technology is developed. With this approach, we fill the gap between proven transportation assessment frameworks and general user-centered techniques. Central to our approach is an electric test vehicle that is implemented in rural supply and value chains for research, development, and testing. Based on our objective and the derived methodological requirements, a set of existing methods is  selected. Local partners are integrated in an organizational framework that executes major parts of this research endeavour in Arsi Zone, Oromia Region, Ethiopia.

Keywords: Agricultural value chain, participatory methods, agile methods, sub-Saharan Africa, Ethiopia, electric vehicle, transport service.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 86

Authors: Anne Theresa Eidhoff, Sarah E. Stief, Markus Voeth, Sarah Gundlach

Abstract:

With digitalization increasingly changing the rules of competition, firms face the need to adapt and assimilate digital technologies in order to remain competitive. Firms can choose from various possibilities to integrate digital technologies including the option to embed digital technologies aiming to innovate products or to develop digital products. However, the question of which specific factors influence a firm’s decision to pursue digital product innovation remains unanswered in research. By adopting the Technology-Organization-Environment (TOE)-framework we have designed a qualitative exploratory study including eleven German practitioners to investigate relevant contingency factors. Our results indicate that the most critical factors for a company’s decision to pursue digital product innovation can be found in the technological and environmental dimensions, namely customers, competitive pressure, technological change, as well as digitalization fit. 

Keywords: Digital innovation, digitalization, product innovation, TOE-framework.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2000

Authors: Markus G. Ortner, Christian Magele, Klaus Krischan

Abstract:

Knowledge about the magnetic quantities in a magnetic circuit is always of great interest. On the one hand, this information is needed for the simulation of a transformer. On the other hand, parameter studies are more reliable, if the magnetic quantities are derived from a well established model. One possibility to model the 3-phase transformer is by using a magnetic equivalent circuit (MEC). Though this is a well known system, it is often not an easy task to set up such a model for a large number of lumped elements which additionally includes the nonlinear characteristic of the magnetic material. Here we show the setup of a solver for a MEC and the results of the calculation in comparison to measurements taken. The equations of the MEC are based on a rearranged system of the nodal analysis. Thus it is possible to achieve a minimum number of equations, and a clear and simple structure. Hence, it is uncomplicated in its handling and it supports the iteration process. Additional helpful tasks are implemented within the solver to enhance the performance. The electric circuit is described by an electric equivalent circuit (EEC). Our results for the 3-phase transformer demonstrate the computational efficiency of the solver, and show the benefit of the application of a MEC.

Keywords: Inrush current, magnetic equivalent circuit, nonlinear behavior, transformer.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2417

Authors: Philip Rose, Markus Linke, David Busquets

Abstract:

The distinction between interlaminar and intralaminar fracture toughness is challenging. For loading mode I, the double cantilever beam specimens were often used for the interlaminar fracture toughness and the compact tension specimen for the intralaminar fracture toughness. For the analysis of interlaminar properties regarding energy release under different loading modes, the geometry of the DCB specimen can also be tested under three-point bending for Mode II characteristics. The same specimen can also be tested with defined superimposed loading conditions (mixed mode) using the Mixed Mode Bending test apparatus. However, this approach has not been applicable for intralaminar characteristics, as crack initiation in a single layer for laminates made out of prepreg, has not been feasible. The method presented in this work enables differentiation of interlaminar and intralaminar energy release rates in Mode II loading with nearly identical specimen geometry. With this, a practically identical energy release rate is observed in Mode II for the investigated material IM7/8552.

Keywords: Fibre reinforced plastics, end-notched flexure, energy release rate, fracture toughness, intralaminar, interlaminar.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 94

Authors: Roman Major, Klaudia Trembecka-Wojciga, Juergen Markus Lackner, Boguslaw Major

Abstract:

The future and the development of science is therefore seen in interdisciplinary areas such as biomedical engineering. Selfassembled structures, similar to stem cell niches would inhibit fast division process and subsequently capture the stem cells from the blood flow. By means of surface topography and the stiffness as well as microstructure progenitor cells should be differentiated towards the formation of endothelial cells monolayer which effectively will inhibit activation of the coagulation cascade. The idea of the material surface development met the interest of the clinical institutions, which support the development of science in this area and are waiting for scientific solutions that could contribute to the development of heart assist systems. This would improve the efficiency of the treatment of patients with myocardial failure, supported with artificial heart assist systems. Innovative materials would enable the redesign, in the post project activity, construction of ventricular heart assist.

Keywords: Bio-inspired materials, electron microscopy, haemocompatibility, niche-like structures, thin coatings.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1790

Authors: Markus Link, Manfred Spraul, Hartmut Schaefer, Fang Fang, Birk Schuetz

Abstract:

High Resolution NMR Spectroscopy offers unique screening capabilities for food quality and safety by combining non-targeted and targeted screening in one analysis.

The objective is to demonstrate, that due to its extreme reproducibility NMR can detect smallest changes in concentrations of many components in a mixture, which is best monitored by statistical evaluation however also delivers reliable quantification results.

The methodology typically uses a 400 MHz high resolution instrument under full automation after minimized sample preparation.

For example one fruit juice analysis in a push button operation takes at maximum 15 minutes and delivers a multitude of results, which are automatically summarized in a PDF report.

The method has been proven on fruit juices, where so far unknown frauds could be detected. In addition conventional targeted parameters are obtained in the same analysis. This technology has the advantage that NMR is completely quantitative and concentration calibration only has to be done once for all compounds. Since NMR is so reproducible, it is also transferable between different instruments (with same field strength) and laboratories. Based on strict SOP`s, statistical models developed once can be used on multiple instruments and strategies for compound identification and quantification are applicable as well across labs.

Keywords: Automated solution, NMR, non-targeted screening, targeted screening.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2205

Authors: Harald Rojacz, Markus Varga, Horst Winkelmann

Abstract:

Within this work High Temperature Single Impact Studies were performed to evaluate deformation mechanisms at different energy and momentum levels. To show the influence of different microstructures and hardness levels and their response to single impacts four different materials were tested at various temperatures up to 700°C. One carbide reinforced NiCrBSi based Metal Matrix Composite and three different steels were tested. The aim of this work is to determine critical energies for fracture appearance and the materials response at different energy and momenta levels. Critical impact loadings were examined at elevated temperatures to limit operating conditions in impact dominated regimes at elevated temperatures. The investigations on the mechanisms were performed using different means of microscopy at the surface and in metallographic cross sections. Results indicate temperature dependence of the occurrence of cracks in hardphase rich materials, such as Metal Matrix Composites High Speed Steels and the influence of different impact momenta at constant energies on the deformation of different steels.

Keywords: Deformation, High Temperature, Metal Matrix Composite, Single Impact Test, Steel.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1961

Authors: Markus Kaiser, Johannes Buchmann

Abstract:

In this article, a formal specification and verification of the Rabin public-key scheme in a formal proof system is presented. The idea is to use the two views of cryptographic verification: the computational approach relying on the vocabulary of probability theory and complexity theory and the formal approach based on ideas and techniques from logic and programming languages. A major objective of this article is the presentation of the first computer-proved implementation of the Rabin public-key scheme in Isabelle/HOL. Moreover, we explicate a (computer-proven) formalization of correctness as well as a computer verification of security properties using a straight-forward computation model in Isabelle/HOL. The analysis uses a given database to prove formal properties of our implemented functions with computer support. The main task in designing a practical formalization of correctness as well as efficient computer proofs of security properties is to cope with the complexity of cryptographic proving. We reduce this complexity by exploring a light-weight formalization that enables both appropriate formal definitions as well as efficient formal proofs. Consequently, we get reliable proofs with a minimal error rate augmenting the used database, what provides a formal basis for more computer proof constructions in this area.

Keywords: public-key encryption, Rabin public-key scheme, formalproof system, higher-order logic, formal verification.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1491

Authors: Markus Kaiser, Johannes Buchmann

Abstract:

In this article we explore the application of a formal proof system to verification problems in cryptography. Cryptographic properties concerning correctness or security of some cryptographic algorithms are of great interest. Beside some basic lemmata, we explore an implementation of a complex function that is used in cryptography. More precisely, we describe formal properties of this implementation that we computer prove. We describe formalized probability distributions (σ-algebras, probability spaces and conditional probabilities). These are given in the formal language of the formal proof system Isabelle/HOL. Moreover, we computer prove Bayes- Formula. Besides, we describe an application of the presented formalized probability distributions to cryptography. Furthermore, this article shows that computer proofs of complex cryptographic functions are possible by presenting an implementation of the Miller- Rabin primality test that admits formal verification. Our achievements are a step towards computer verification of cryptographic primitives. They describe a basis for computer verification in cryptography. Computer verification can be applied to further problems in cryptographic research, if the corresponding basic mathematical knowledge is available in a database.

Keywords: prime numbers, primality tests, (conditional) probabilitydistributions, formal proof system, higher-order logic, formalverification, Bayes' Formula, Miller-Rabin primality test.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1418

Authors: Markus Kaiser, Johannes Buchmann

Abstract:

In this paper we explore the application of a formal proof system to verification problems in cryptography. Cryptographic properties concerning correctness or security of some cryptographic algorithms are of great interest. Beside some basic lemmata, we explore an implementation of a complex function that is used in cryptography. More precisely, we describe formal properties of this implementation that we computer prove. We describe formalized probability distributions (o--algebras, probability spaces and condi¬tional probabilities). These are given in the formal language of the formal proof system Isabelle/HOL. Moreover, we computer prove Bayes' Formula. Besides we describe an application of the presented formalized probability distributions to cryptography. Furthermore, this paper shows that computer proofs of complex cryptographic functions are possible by presenting an implementation of the Miller- Rabin primality test that admits formal verification. Our achievements are a step towards computer verification of cryptographic primitives. They describe a basis for computer verification in cryptography. Computer verification can be applied to further problems in crypto-graphic research, if the corresponding basic mathematical knowledge is available in a database.

Keywords: prime numbers, primality tests, (conditional) proba¬bility distributions, formal proof system, higher-order logic, formal verification, Bayes' Formula, Miller-Rabin primality test.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2136

Authors: Guenther Schuh, Christina Koenig, Nico Schoen, Markus Wellensiek

Abstract:

Identification and selection of appropriate product and manufacturing technologies are key factors for competitiveness and market success of technology-based companies. Therefore, many companies perform technology intelligence (TI) activities to ensure the identification of evolving technologies at the right time. Technology monitoring is one of the three base activities of TI, besides scanning and scouting. As the technological progress is accelerating, more and more technologies are being developed. Against the background of limited resources it is therefore necessary to focus TI activities. In this paper we propose a concept for defining appropriate search fields for technology monitoring. This limitation of search space leads to more concentrated monitoring activities. The concept will be introduced and demonstrated through an anonymized case study conducted within an industry project at the Fraunhofer Institute for Production Technology IPT. The described concept provides a customized monitoring approach, which is suitable for use in technology-oriented companies. It is shown in this paper that the definition of search fields and search tasks are suitable methods to define topics of interest and thus to align monitoring activities. Current as well as planned product, production and material technologies and existing skills, capabilities and resources form the basis for derivation of relevant search areas. To further improve the concept of technology monitoring the proposed concept should be extended during future research e.g. by the definition of relevant monitoring parameters.

Keywords: Monitoring radar, search field, technology intelligence, technology monitoring.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 3200

Authors: Tobias Teich, Danny Szendrei, Markus Schrader, Franziska Jahn, Susan Franke

Abstract:

The increasing demand for sufficient and clean energy forces industrial and service companies to align their strategies towards efficient consumption. This trend refers also to the residential building sector. There, large amounts of energy consumption are caused by house and facility heating. Many of the operated hot water heating systems lack hydraulic balanced working conditions for heat distribution and –transmission and lead to inefficient heating. Through hydraulic balancing of heating systems, significant energy savings for primary and secondary energy can be achieved. This paper addresses the use of KNX-technology (Smart Buildings) in residential buildings to ensure a dynamic adaption of hydraulic system's performance, in order to increase the heating system's efficiency. In this paper, the procedure of heating system segmentation into hydraulically independent units (meshes) is presented. Within these meshes, the heating valve are addressed and controlled by a central facility server. Feasibility criteria towards such drivers will be named. The dynamic hydraulic balance is achieved by positioning these valves according to heating loads, that are generated from the temperature settings in the corresponding rooms. The energetic advantages of single room heating control procedures, based on the application FacilityManager, is presented.

Keywords: building automation, dynamic hydraulic balance, energy savings, VPN-networks.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1849

Authors: Branislav Timotijevic, Yves Petremand, Markus Luetzelschwab, Dara Bayat, Laurent Aebi

Abstract:

Optical miniaturized sensors with remote readout are required devices for the monitoring in harsh electromagnetic environments. As an example, in turbo and hydro generators, excessively high vibrations of the end-windings can lead to dramatic damages, imposing very high, additional service costs. A significant change of the generator temperature can also be an indicator of the system failure. Continuous monitoring of vibrations, temperature, humidity, and gases is therefore mandatory. The high electromagnetic fields in the generators impose the use of non-conductive devices in order to prevent electromagnetic interferences and to electrically isolate the sensing element to the electronic readout. Metal-free sensors are good candidates for such systems since they are immune to very strong electromagnetic fields and given the fact that they are non-conductive. We have realized miniature optical accelerometer and temperature sensors for a remote sensing of the harsh environments using the common, inexpensive silicon Micro Electro-Mechanical System (MEMS) platform. Both devices show highly linear response. The accelerometer has a deviation within 1% from the linear fit when tested in a range 0 – 40 g. The temperature sensor can provide the measurement accuracy better than 1 °C in a range 20 – 150 °C. The design of other type of sensors for the environments with high electromagnetic interferences has also been discussed.

Keywords: Accelerometer, harsh environment, optical MEMS, pressure sensor, remote sensing, temperature sensor.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1079