WB_Diss_2017

Boussahel, Wassim:
Improving energy efficiency of manufacturing systems through formal analysis of alternative strategies.


Dissertation, Universität des Saarlandes, Saarbrücken, Germany, Febr. 20st, 2017.

Shaker-Verlag, Aachen, April 2017, ISBN: 978-3-8440-5154-4

 

Abstract:

Energy efficiency is a widely discussed topic in in the manufacturing industry due to environmental and economic reasons. Manufacturers are always looking for being more energy-efficient which is a recipe for being more competitive, reducing waste and spending less money on energy than it is necessary. Potentials to save energy are present at every level and a special attention should be given to unused energy during idle times. Switching systems during these times to energy-efficient modes is one of these potentials that is somehow neglected and not very much explored in the literature in terms of formal models. This problem can be reduced to models exhibiting parallel strategies displaying different timing and energetic profiles and dependability between the different systems; the ultimate goal is to find optimal strategies respecting all the manufacturing-related requirements. The objective of the thesis is to formalize such problems by proposing a methodology directly implementable in the model checker PRISM. This model checker imposes high restrictions on continuous variables used in automata-based models; this makes a discrete approach more appropriate for modeling systems for the purpose of evaluation and optimization. Use-case examples are presented in order to illustrate the approach and explain the extent of what could be done with automata-based models in the model checker PRISM.

 

Kurzfassung:

Energieeffizienz ist ein vieldiskutiertes Thema in der Fertigungsindustrie aufgrund von ökologischen sowie ökonomischen Überlegungen. Hersteller sind stetig darum bemüht, ihre Energieeffizienz zu steigern, um sich im Wettbewerb behaupten zu können. Hierzu gehören die Reduzierung von anfallender Energieverschwendung sowie die Minimierung der Energiekosten auf das Nötigste. Einsparpotenziale für Energie gibt es auf jeder Ebene, wobei besonderes Augenmerk auf Energieverbrauch in Produktionpausen und im Leerlauf liegen sollte. Die Umschaltung auf energieeffiziente Zustände wird zu sehr vernachlässigt und nicht ausgiebig in Bezug auf formale Modelle in der Literatur behandelt. Dieses Problem lässt sich in Modellen reduzieren, welche verschiedene Strategien, mit unterschiedlichen Zeit- und Energieprofilen sowie Abhängigkeiten zwischen Systemen, aufweisen. Ziel ist es, die möglichst optimale Lösung zu finden, welche die Voraussetzungen des jeweiligen Anwendungszwecks erfüllt. Das Ziel dieser Dissertation ist eine Methodik zu entwickeln, die eine direkte Implementierungsmöglichkeit im Model Checker PRISM aufweist. PRISM hat starke Restriktionen im Umgang mit kontinuierlichen Variablen, welche in auf Automaten basierenden Modellen benutzt werden. Dies macht eine ereignisdiskrete Herangehensweise geeigneter zum Zweck der Evaluierung und Optimierung. Es werden Anwendungsbeispiele gezeigt, die das Ausmaß dessen aufzeigen, was mit automatenbasierten Modellen im PRISM möglich ist.