Search results for: Juergen Markus Lackner

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 1836

Authors: Hermenegilde Nkurunziza, Albrecht Gebhardt, Juergen Pilz

Abstract:

The focus in this work is to assess which method allows a better forecasting of malaria cases in Bujumbura ( Burundi) when taking into account association between climatic factors and the disease. For the period 1996-2007, real monthly data on both malaria epidemiology and climate in Bujumbura are described and analyzed. We propose a hierarchical approach to achieve our objective. We first fit a Generalized Additive Model to malaria cases to obtain an accurate predictor, which is then used to predict future observations. Various well-known forecasting methods are compared leading to different results. Based on in-sample mean average percentage error (MAPE), the multiplicative exponential smoothing state space model with multiplicative error and seasonality performed better.

Keywords: Burundi, Forecasting, Malaria, Regressionmodel, State space model.

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

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 1567

Authors: L. Major, J. M. Lackner, M. Dyner, B. Major

Abstract:

Development of new generation bio-tribological, multilayer coatings opens an avenue for fabrication of future hightech functional surfaces. In the presented work, nano-composite, Cr/CrN+[Cr/ a-C:H implanted by metallic nanocrystals] multilayer coatings have been developed for surface protection of medical tools. Thin films were fabricated by a hybrid Pulsed Laser Deposition technique. Complex microstructure analysis of nanomultilayer coatings, subjected to mechanical and biological tests, were performed by means of transmission electron microscopy (TEM). Microstructure characterization revealed the layered arrangement of Cr23C6 nanoparticles in multilayer structure. Influence of deposition conditions on bio-tribological properties of the coatings was studied. The bio-tests were used as a screening tool for the analyzed nanomultilayer coatings before they could be deposited on medical tools. Bio-medical tests were done using fibroblasts. The mechanical properties of the coatings were investigated by means of a ball-ondisc mechanical test. The micro hardness was done using Berkovich indenter. The scratch adhesion test was done using Rockwell indenter. From the bio-tribological point of view, the optimal properties had the C106_1 material.

Keywords: Bio-tribological coatings, cell-material interaction, hybrid PLD, tribology.

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

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 2015

Authors: Barath Kumar, Oliver Niggemann, Juergen Jasperneite

Abstract:

Model-based approaches have been applied successfully to a wide range of tasks such as specification, simulation, testing, and diagnosis. But one bottleneck often prevents the introduction of these ideas: Manual modeling is a non-trivial, time-consuming task. Automatically deriving models by observing and analyzing running systems is one possible way to amend this bottleneck. To derive a model automatically, some a-priori knowledge about the model structure–i.e. about the system–must exist. Such a model formalism would be used as follows: (i) By observing the network traffic, a model of the long-term system behavior could be generated automatically, (ii) Test vectors can be generated from the model, (iii) While the system is running, the model could be used to diagnose non-normal system behavior. The main contribution of this paper is the introduction of a model formalism called 'probabilistic regression automaton' suitable for the tasks mentioned above.

Keywords: Model-based approach, Probabilistic regression automata, Statistical models and Timed automata.

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

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 3022

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 1559

Authors: Juergen Rossmann, Andre Kupetz, Roland Wischnewski

Abstract:

Mobile robots are used in a large field of scenarios, like exploring contaminated areas, repairing oil rigs under water, finding survivors in collapsed buildings, etc. Currently, there is no unified intuitive user interface (UI) to control such complex mobile robots. As a consequence, some scenarios are done without the exploitation of experience and intuition of human teleoperators. A novel framework has been developed to embed a flexible and modular UI into a complete 3-D virtual reality simulation system. This new approach wants to access maximum benefits of human operators. Sensor information received from the robot is prepared for an intuitive visualization. Virtual reality metaphors support the operator in his decisions. These metaphors are integrated into a real time stereo video stream. This approach is not restricted to any specific type of mobile robot and allows for the operation of different robot types with a consistent concept and user interface.

Keywords: 3-D simulation system, augmented reality, teleoperation of mobile robots, user interface.

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

Authors: AlNPhannee Saengkaew, Armin Dadgar, Juergen Blaesing, Thomas Hempel, Sakuntam Sanorpim, Chanchana Thanachayanont, Visittapong Yordsri, Watcharee Rattanasakulthong, Alois Krost

Abstract:

Group-III nitride material as particularly AlxGa1-xN is one of promising optoelectronic materials to require for shortwavelength devices. To achieve the high-quality AlxGa1-xN films for a high performance of such devices, AlN-nucleation layers are the important factor. To improve the AlN-nucleation layers with a variation of Ga-addition, XRD measurements were conducted to analyze the crystalline quality of the subsequent Al0.1Ga0.9N with the minimum ω-FWHMs of (0002) and (10-10) reflections of 425 arcsec and 750 arcsec, respectively. SEM and AFM measurements were performed to observe the surface morphology and TEM measurements to identify the microstructures and orientations. Results showed that the optimized Ga-atoms in the Al(Ga)Nnucleation layers improved the surface diffusion to form moreuniform crystallites in structure and size, better alignment of each crystallite, and better homogeneity of island distribution. This, hence, improves the orientation of epilayers on the Si-surface and finally improves the crystalline quality and reduces the residual strain of subsequent Al0.1Ga0.9N layers.

Keywords: AlGaN, UV-LEDs, seed layers, AFM, TEM

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

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 1695

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 1523

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 6326

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 2338

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 2834

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 1665

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 1777

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 2267

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 1590

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 160

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 2056

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 2465

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 201

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 2247

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 2002

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 1535

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 1469

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 2180

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 3254

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 1894