During the years, our research lead to a number of publications at conferences and journals. Publishing ideas and results is the main resource for fruitful discussions and feedback from the worldwide research community.
2016 |
Anders, Anton Indoor-Positionsbestimmung mit Hilfe von Bluetooth-Low-Energy-Beacons und Pedestrian Dead Reckoning Abschlussarbeit Otto-von-Guericke-Universität Magdeburg, 2016. Links | BibTeX | Schlagwörter: Augmented Reality, Bluetooth @mastersthesis{Anders2016, title = {Indoor-Positionsbestimmung mit Hilfe von Bluetooth-Low-Energy-Beacons und Pedestrian Dead Reckoning}, author = {Anton Anders}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2016/08/BA_Anton_Anders.pdf}, year = {2016}, date = {2016-03-29}, school = {Otto-von-Guericke-Universit\"{a}t Magdeburg}, type = {Bachelorarbeit}, keywords = {Augmented Reality, Bluetooth}, pubstate = {published}, tppubtype = {mastersthesis} } |
Klockmann, Maximilian Analyse von Crowd-Simulation Algorithmen beim Durchqueren von Engstellen Abschlussarbeit Otto-von-Guericke-Universität Magdeburg, 2016. Links | BibTeX | Schlagwörter: virtual reality @mastersthesis{Klockmann2016, title = {Analyse von Crowd-Simulation Algorithmen beim Durchqueren von Engstellen}, author = {Maximilian Klockmann}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2016/08/BA_Max_Klockmann.pdf}, year = {2016}, date = {2016-03-09}, school = {Otto-von-Guericke-Universit\"{a}t Magdeburg}, type = {Bachelorarbeit}, keywords = {virtual reality}, pubstate = {published}, tppubtype = {mastersthesis} } |
Filax, Marco; Gonschorek, Tim; Hebecker, Tanja; Lipaczewski, Michael; Madalinski, Agnes; Ortmeier, Frank; Fietze, Mario; Schumacher, Rolf Der Eisenbahn Ingenieur, S. 24 -27, 2016. Abstract | Links | BibTeX | Schlagwörter: Formal Modelling Process, Railway System Verification, Requirements Traceability, System Verification, VIP-MoBaSA @article{ei2016, title = {Bringing formal methods “on the rail” - Modellbasierte Systemanalyse in der Sicherheitsnachweisf\"{u}hrung}, author = {Marco Filax and Tim Gonschorek and Tanja Hebecker and Michael Lipaczewski and Agnes Madalinski and Frank Ortmeier and Mario Fietze and Rolf Schumacher}, editor = {Verband Deutscher Eisenbahn-Ingenieure E.V.}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2016/08/Ver\"{o}ffentlichung-Eisenbahningeneur.pdf}, year = {2016}, date = {2016-01-01}, journal = {Der Eisenbahn Ingenieur}, pages = {24 -27}, abstract = {Funktionen sicherheitskritischer Systeme im Eisenbahnsektor werden entsprechend ihrer tolerierbaren Gef\"{a}hrdungsraten in sogenannte Sicherheitsintegrit\"{a}tslevel (SIL 1-4) eingestuft. In der europ\"{a}ischen Norm EN50129 besteht, f\"{u}r die Stufen drei und vier, die dringende Empfehlung, im Entwicklungs- und Spezifikationsprozess, formale Methoden anzuwenden. Die Otto-von-Guericke-Universit\"{a}t Magdeburg hat dazu, begleitet durch das Eisenbahn-Bundesamt (EBA) und Gutachtern des EBA, einen Satz unterst\"{u}tzender Werkzeuge und Verfahren entwickelt, welche in diesem Artikel, am Beispiel der Punktf\"{o}rmigen Zugbeeinflussung (PZB), vorgestellt werden sollen. Diese Werkzeuge erm\"{o}glichen die Portierung einer nat\"{u}rlichsprachlichen Systemanforderungsspezifikation in ein formales Modell, mit dessen Hilfe die Konsistenz und Vollst\"{a}ndigkeit der Systembeschreibung, sowie die definierten Sicherheitsanforderungen formal \"{u}berpr\"{u}ft werden k\"{o}nnen. Bereits in fr\"{u}hen Entwicklungsphasen k\"{o}nnen automatisiert qualitative und quantitative Absch\"{a}tzungen \"{u}ber die Sicherheit und Zuverl\"{a}ssigkeit mit pr\"{a}zisen und aussagekr\"{a}ftigen Resultaten berechnet werden. Gleichzeitig wird der Aufwand zur endg\"{u}ltigen, sicherheitstechnischen Bewertung durch vollst\"{a}ndige Traceability als Teil des Zertifizierungs- und Zulassungsprozesses reduziert.}, keywords = {Formal Modelling Process, Railway System Verification, Requirements Traceability, System Verification, VIP-MoBaSA}, pubstate = {published}, tppubtype = {article} } Funktionen sicherheitskritischer Systeme im Eisenbahnsektor werden entsprechend ihrer tolerierbaren Gefährdungsraten in sogenannte Sicherheitsintegritätslevel (SIL 1-4) eingestuft. In der europäischen Norm EN50129 besteht, für die Stufen drei und vier, die dringende Empfehlung, im Entwicklungs- und Spezifikationsprozess, formale Methoden anzuwenden. Die Otto-von-Guericke-Universität Magdeburg hat dazu, begleitet durch das Eisenbahn-Bundesamt (EBA) und Gutachtern des EBA, einen Satz unterstützender Werkzeuge und Verfahren entwickelt, welche in diesem Artikel, am Beispiel der Punktförmigen Zugbeeinflussung (PZB), vorgestellt werden sollen. Diese Werkzeuge ermöglichen die Portierung einer natürlichsprachlichen Systemanforderungsspezifikation in ein formales Modell, mit dessen Hilfe die Konsistenz und Vollständigkeit der Systembeschreibung, sowie die definierten Sicherheitsanforderungen formal überprüft werden können. Bereits in frühen Entwicklungsphasen können automatisiert qualitative und quantitative Abschätzungen über die Sicherheit und Zuverlässigkeit mit präzisen und aussagekräftigen Resultaten berechnet werden. Gleichzeitig wird der Aufwand zur endgültigen, sicherheitstechnischen Bewertung durch vollständige Traceability als Teil des Zertifizierungs- und Zulassungsprozesses reduziert. |
2015 |
Bahl, Benedikt Konzepte zur Optimierung des Betriebshofmanagements mit pervasiven Assistenzsystemen Abschlussarbeit Otto-von-Guericke-Universität Magdeburg, 2015. Links | BibTeX | Schlagwörter: Augmented Reality @mastersthesis{Bahl2015, title = {Konzepte zur Optimierung des Betriebshofmanagements mit pervasiven Assistenzsystemen}, author = {Benedikt Bahl}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2016/08/MA_Benedikt_Bahl.pdf}, year = {2015}, date = {2015-12-15}, school = {Otto-von-Guericke-Universit\"{a}t Magdeburg}, type = {Masterarbeit}, keywords = {Augmented Reality}, pubstate = {published}, tppubtype = {mastersthesis} } |
Hamannn, Dominik Kopplung formaler Modelle mit realweltlichen Umgebungsmodellen Abschlussarbeit Otto-von-Guericke-Universität Magdeburg, 2015. Abstract | Links | BibTeX | Schlagwörter: co-simulation of system models, model-based verfication @mastersthesis{BAHamann2015, title = {Kopplung formaler Modelle mit realweltlichen Umgebungsmodellen}, author = {Dominik Hamannn}, editor = {Otto-von-Guericke-Universit\"{a}t Magdeburg}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/12/BAHamann2015.pdf}, year = {2015}, date = {2015-12-14}, address = {Universit\"{a}tsplatz 2, 39106 Magdeburg}, school = {Otto-von-Guericke-Universit\"{a}t Magdeburg}, abstract = {Sicherheitskritische technische Systeme werden insbesondere in der Automobilindustrie und der Luftfahrt immer komplexer. Ein Ansatz, um die Sicherheit solcher Systeme zu \"{u}berpr\"{u}fen, besteht darin, ein Modell des Systems zu erstellen und dieses von einem Model Checker auf gef\"{a}hrdende Situationen zu \"{u}berpr\"{u}fen. Die Umgebung eines softwareintensiven Systems muss oft, aufgrund der Funktionsweise von Model Checkern und aufgrund von Restriktionen der verwendeten Sprache, mit einem hohen Abstraktionsgrad modelliert werden. Das betrif t insbesondere Systeme, die nicht nur rein logische Aufgaben ausf\"{u}hren, sondern mittels Sensorik und Aktorik mit der realen Welt interagieren. Herrscht eine zu gro{\ss}e Diskrepanz zwischen der realen Umgebung und dem Modell der Umgebung, tritt in dem Modell Fehlverhalten nicht auf, dass in der realen Welt auftreten w\"{u}rde. Die Ergebnisse eines Model Checkers sind dann f\"{u}r dieses Modell nicht aussagekr\"{a}ftig. In dieser Arbeit wird eine Schnittstelle vorgestellt, mit der formale Modelle mit realweltlichen Umgebungsmodellen gekoppelt werden k\"{o}nnen. Dadurch wird getestet, inwiefern sich das Verhalten des formalen Modells in einer realistischen Umgebung von dem Verhalten einer abstrahierten Umgebung unterscheidet. Dieser Vergleich kann Aufschluss \"{u}ber die Validit\"{a}t des verwendeten Umgebungsmodells bringen.}, howpublished = {Bachelorarbeit}, keywords = {co-simulation of system models, model-based verfication}, pubstate = {published}, tppubtype = {mastersthesis} } Sicherheitskritische technische Systeme werden insbesondere in der Automobilindustrie und der Luftfahrt immer komplexer. Ein Ansatz, um die Sicherheit solcher Systeme zu überprüfen, besteht darin, ein Modell des Systems zu erstellen und dieses von einem Model Checker auf gefährdende Situationen zu überprüfen. Die Umgebung eines softwareintensiven Systems muss oft, aufgrund der Funktionsweise von Model Checkern und aufgrund von Restriktionen der verwendeten Sprache, mit einem hohen Abstraktionsgrad modelliert werden. Das betrif t insbesondere Systeme, die nicht nur rein logische Aufgaben ausführen, sondern mittels Sensorik und Aktorik mit der realen Welt interagieren. Herrscht eine zu große Diskrepanz zwischen der realen Umgebung und dem Modell der Umgebung, tritt in dem Modell Fehlverhalten nicht auf, dass in der realen Welt auftreten würde. Die Ergebnisse eines Model Checkers sind dann für dieses Modell nicht aussagekräftig. In dieser Arbeit wird eine Schnittstelle vorgestellt, mit der formale Modelle mit realweltlichen Umgebungsmodellen gekoppelt werden können. Dadurch wird getestet, inwiefern sich das Verhalten des formalen Modells in einer realistischen Umgebung von dem Verhalten einer abstrahierten Umgebung unterscheidet. Dieser Vergleich kann Aufschluss über die Validität des verwendeten Umgebungsmodells bringen. |
Heumüller, Robert Multi-Abstraction Model Based Software Development for Embedded Low-Cost Applications Abschlussarbeit 2015. Links | BibTeX | Schlagwörter: arm, compiler, embedded, llvm, mdd, mde, model based @mastersthesis{Heum\"{u}ller2015, title = {Multi-Abstraction Model Based Software Development for Embedded Low-Cost Applications}, author = {Robert Heum\"{u}ller}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/01/thesis-1.pdf}, year = {2015}, date = {2015-11-06}, keywords = {arm, compiler, embedded, llvm, mdd, mde, model based}, pubstate = {published}, tppubtype = {mastersthesis} } |
Hebecker, Tanja; Ortmeier, Frank Safe Prediction-Based Local Path Planning using Obstacle Probability Sections Inproceedings Laugier, Christian; Martinet, Philippe; Nunes, Urbano; stiller, Christoph (Hrsg.): Proceedings of the 7th IROS Workshop on Planning, Perception and Navigation for Intelligent Vehicles, S. 183 - 188, 2015. Abstract | Links | BibTeX | Schlagwörter: local path planning, Obstacle probability sections @inproceedings{Hebecker2015, title = {Safe Prediction-Based Local Path Planning using Obstacle Probability Sections}, author = {Tanja Hebecker and Frank Ortmeier}, editor = {Christian Laugier and Philippe Martinet and Urbano Nunes and Christoph stiller }, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2016/02/hebecker2015_SafePrediction-basedLocalPathPlanningUsingObstacleProbability.pdf}, year = {2015}, date = {2015-09-28}, booktitle = {Proceedings of the 7th IROS Workshop on Planning, Perception and Navigation for Intelligent Vehicles}, pages = {183 - 188}, abstract = {Autonomous mobile robots gain more and more importance. In the nearest future they will be a part of everyday life. Therefore, it is critical to make them as reliable and safe as possible. We present a local path planner that shall ensure safety in an environment cluttered with unexpectedly moving obstacles. In this paper, the motion of obstacles is predicted by generating probability sections, and collision risks of path configurations are checked by determining whether these configurations lead inevitably to a collision or not. The presented approach worked efficiently in scenarios with static and dynamic obstacles.}, keywords = {local path planning, Obstacle probability sections}, pubstate = {published}, tppubtype = {inproceedings} } Autonomous mobile robots gain more and more importance. In the nearest future they will be a part of everyday life. Therefore, it is critical to make them as reliable and safe as possible. We present a local path planner that shall ensure safety in an environment cluttered with unexpectedly moving obstacles. In this paper, the motion of obstacles is predicted by generating probability sections, and collision risks of path configurations are checked by determining whether these configurations lead inevitably to a collision or not. The presented approach worked efficiently in scenarios with static and dynamic obstacles. |
Orth, Severin Trace refinement with reduced interpolant automata for binary programs Abschlussarbeit Otto-von-Guericke-Universität Magdeburg, 2015. Links | BibTeX | Schlagwörter: binary programs, trace refinement @mastersthesis{BA-Orth, title = {Trace refinement with reduced interpolant automata for binary programs}, author = {Severin Orth}, url = {/cse/?attachment_id=1937}, year = {2015}, date = {2015-09-14}, school = {Otto-von-Guericke-Universit\"{a}t Magdeburg}, keywords = {binary programs, trace refinement}, pubstate = {published}, tppubtype = {mastersthesis} } |
Nykolaichuk, Mykhaylo; Ortmeier, Frank Coverage Path Re-Planning for Processing Faults Inproceedings Springer, (Hrsg.): The 8th International Conference on Intelligent Robotics and Applications (ICIRA2015) , S. 358-368 , 2015. Abstract | Links | BibTeX | Schlagwörter: coverage path planning, online path planning @inproceedings{Nykolaichuk2015, title = {Coverage Path Re-Planning for Processing Faults}, author = {Mykhaylo Nykolaichuk and Frank Ortmeier}, editor = {Springer}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/07/coveragePathReplanning_final.pdf https://link.springer.com/chapter/10.1007/978-3-319-22876-1_31}, year = {2015}, date = {2015-08-20}, booktitle = {The 8th International Conference on Intelligent Robotics and Applications (ICIRA2015) }, volume = {9245}, pages = {358-368 }, abstract = {Currently, an automated surface treatment or finishing (e.g., abrasive blasting, cleaning or painting) is performed in two consecutive steps: first processing by tool, second quality evaluation by sensor. Often, a finished surface has defects like areas not properly processed. This is caused by path inaccuracy or errors in tool deployment. The defected areas can be detected only during a subsequent quality evaluation. As a result, a complete surface reprocessing is required which is costly and time-consuming. We propose a new approach that is a combination of surface treatment and quality evaluation processes in a single deployment. In our approach, an initial coverage path for surface treatment by a tool is given or calculated using a state-of-the-art coverage path planning algorithm. In fact, we extend an off-line generated initial coverage path with an ability to react to sensor-based defect recognitions during surface processing by a tool.}, keywords = {coverage path planning, online path planning}, pubstate = {published}, tppubtype = {inproceedings} } Currently, an automated surface treatment or finishing (e.g., abrasive blasting, cleaning or painting) is performed in two consecutive steps: first processing by tool, second quality evaluation by sensor. Often, a finished surface has defects like areas not properly processed. This is caused by path inaccuracy or errors in tool deployment. The defected areas can be detected only during a subsequent quality evaluation. As a result, a complete surface reprocessing is required which is costly and time-consuming. We propose a new approach that is a combination of surface treatment and quality evaluation processes in a single deployment. In our approach, an initial coverage path for surface treatment by a tool is given or calculated using a state-of-the-art coverage path planning algorithm. In fact, we extend an off-line generated initial coverage path with an ability to react to sensor-based defect recognitions during surface processing by a tool. |
Alatartsev, Sergey Robot Trajectory Optimization for Relaxed Effective Tasks Promotionsarbeit Otto-von-Guericke University of Magdeburg, 2015. Abstract | Links | BibTeX | Schlagwörter: robotics, travelling salesman problem @phdthesis{Alatartsev2015c, title = {Robot Trajectory Optimization for Relaxed Effective Tasks}, author = {Sergey Alatartsev}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2016/01/Alatartsev_PhD_thesis.pdf}, year = {2015}, date = {2015-07-07}, school = {Otto-von-Guericke University of Magdeburg}, abstract = {Industrial robots are flexible machines that are currently involved in multiple production domains. Mainly their workflow consists of two alternating stages. The first stage is effective movements that are required to perform a task, e.g., welding a seam. The second stage is supporting movements that are needed to move from one effective task to another, e.g., movements between welding seams. Many effective tasks allow a certain freedom during their execution, e.g., the robot’s tool might have a certain deviation during welding. This freedom is often ignored and robots are programmed manually based on the programmer’s intuition. Nonetheless, this freedom can be used as an extra degree of freedom for robot trajectory optimization. In this thesis, we propose a formalization of this freedom for effective tasks. We refer to an effective task with a formalized freedom of execution as a relaxed effective task. Having an infinite number of ways to execute a task raises several research questions: (i) how to optimize a sequence of entry points for relaxed effective tasks? (ii) how to find starting robot configurations for these tasks? (iii) how to optimize a robot trajectory for a certain relaxed task? We propose a solution concept that decomposes a problem containing all three questions into three components that can be applied in combination with each other or with other state-of-the-art approaches. The first component considers the problem of finding a sequence of effective tasks and their entry points. This problem is modeled as the Traveling Salesman Problem with Neighborhoods (TSPN) where a tour has to be found through a set of areas. We propose a Constricting Insertion Heuristic for constructing a tour and a Constricting 3-Opt for improving the tour. In the second component, the problem of adapting a tour for a robot to execute and searching for starting robot configurations is modeled as a Touring-a-sequence-of-Polygons Problem (TPP) where a tour has to be found through a given sequence of areas. We propose a modification of the Rubber-Band Algorithm (RBA). We refer to this extension as a Nested RBA. Optimization of a robot trajectory in the third component is also represented as a TPP. However, in contrast to the classic RBA where areas are constricted with a polyline, we propose an extension of the RBA called Smoothed RBA where areas are constricted with a smooth curve which leads to a minimal cost robot trajectory. }, keywords = {robotics, travelling salesman problem}, pubstate = {published}, tppubtype = {phdthesis} } Industrial robots are flexible machines that are currently involved in multiple production domains. Mainly their workflow consists of two alternating stages. The first stage is effective movements that are required to perform a task, e.g., welding a seam. The second stage is supporting movements that are needed to move from one effective task to another, e.g., movements between welding seams. Many effective tasks allow a certain freedom during their execution, e.g., the robot’s tool might have a certain deviation during welding. This freedom is often ignored and robots are programmed manually based on the programmer’s intuition. Nonetheless, this freedom can be used as an extra degree of freedom for robot trajectory optimization. In this thesis, we propose a formalization of this freedom for effective tasks. We refer to an effective task with a formalized freedom of execution as a relaxed effective task. Having an infinite number of ways to execute a task raises several research questions: (i) how to optimize a sequence of entry points for relaxed effective tasks? (ii) how to find starting robot configurations for these tasks? (iii) how to optimize a robot trajectory for a certain relaxed task? We propose a solution concept that decomposes a problem containing all three questions into three components that can be applied in combination with each other or with other state-of-the-art approaches. The first component considers the problem of finding a sequence of effective tasks and their entry points. This problem is modeled as the Traveling Salesman Problem with Neighborhoods (TSPN) where a tour has to be found through a set of areas. We propose a Constricting Insertion Heuristic for constructing a tour and a Constricting 3-Opt for improving the tour. In the second component, the problem of adapting a tour for a robot to execute and searching for starting robot configurations is modeled as a Touring-a-sequence-of-Polygons Problem (TPP) where a tour has to be found through a given sequence of areas. We propose a modification of the Rubber-Band Algorithm (RBA). We refer to this extension as a Nested RBA. Optimization of a robot trajectory in the third component is also represented as a TPP. However, in contrast to the classic RBA where areas are constricted with a polyline, we propose an extension of the RBA called Smoothed RBA where areas are constricted with a smooth curve which leads to a minimal cost robot trajectory. |
Hühne, Patrick Innenraumlokalisierung von Mobilgeräten mittels Bluetooth LE Abschlussarbeit Otto-von-Guericke-Universität Magdeburg, 2015. Links | BibTeX | Schlagwörter: Augmented Reality, Bluetooth @mastersthesis{Huehne15, title = {Innenraumlokalisierung von Mobilger\"{a}ten mittels Bluetooth LE}, author = {Patrick H\"{u}hne}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2016/08/BA_Patrick_H\"{u}hne.pdf}, year = {2015}, date = {2015-06-22}, school = {Otto-von-Guericke-Universit\"{a}t Magdeburg}, type = {Bachelorarbeit}, keywords = {Augmented Reality, Bluetooth}, pubstate = {published}, tppubtype = {mastersthesis} } |
Gonschorek, Tim; Ortmeier, Frank Slice or Unfold - Experiments on Checking Synchronous Models with Backwards Slicing Inproceedings of Control, International Federation Automatic (Hrsg.): 5th International Workshop on Dependable Control of Discrete Systems (DCDS 2015), 2015, (accepted, will be published this year). Abstract | Links | BibTeX | Schlagwörter: safety analysis, verification @inproceedings{Gonschorek2015DCDS, title = {Slice or Unfold - Experiments on Checking Synchronous Models with Backwards Slicing}, author = {Tim Gonschorek and Frank Ortmeier}, editor = {International Federation of Automatic Control}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/05/paper_bwmc_dcds15.pdf}, year = {2015}, date = {2015-05-31}, booktitle = {5th International Workshop on Dependable Control of Discrete Systems (DCDS 2015)}, abstract = {Nowadays, model checking approaches have one major drawback: They suffer from the state space explosion problem. We think one major problem is that the verification tools always must hold some (symbolic) representation, e.g. a BDD or a adjacency list, in the memory during the verification process. In this paper we propose a verification approach that does not need to hold a complete representation while checking the model. This is done by slicing backward the transition rules, which defines the complete state system.%144 Here, we present the basic backward slicing approach for verifying CTL safety properties traversing the state machine by using a given transition model. In the following , we give a little evaluation with special test models and compare the results to the state of the art model checker nuXmv.}, note = {accepted, will be published this year}, keywords = {safety analysis, verification}, pubstate = {published}, tppubtype = {inproceedings} } Nowadays, model checking approaches have one major drawback: They suffer from the state space explosion problem. We think one major problem is that the verification tools always must hold some (symbolic) representation, e.g. a BDD or a adjacency list, in the memory during the verification process. In this paper we propose a verification approach that does not need to hold a complete representation while checking the model. This is done by slicing backward the transition rules, which defines the complete state system.%144 Here, we present the basic backward slicing approach for verifying CTL safety properties traversing the state machine by using a given transition model. In the following , we give a little evaluation with special test models and compare the results to the state of the art model checker nuXmv. |
Rabeler, Ben Abstraktion kontinuierlichen Verhaltens zur modellbasierten Sicherheitsanalyse Abschlussarbeit 2015. Abstract | Links | BibTeX | Schlagwörter: hybrid model checking, model based verification, model checking @mastersthesis{BARabeler2015, title = {Abstraktion kontinuierlichen Verhaltens zur modellbasierten Sicherheitsanalyse}, author = {Ben Rabeler}, editor = {Otto-von-Guericke-Universit\"{a}t Magdeburg}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/06/ba_thesis_rabeler.pdf}, year = {2015}, date = {2015-05-18}, abstract = {Die Sicherheit von technischen System ist in vielen Gebieten wie der Luftfahrt oder im Stra{\ss}enverkehr von elementarer Bedeutung f\"{u}r die Hersteller solcher Systeme wie f\"{u}r die Anwender. Ein Ansatz um die Sicherheit von diskreten Systemen zu zeigen, besteht darin, diese in einem diskreten Modell zu abstrahieren und anschlie{\ss}end mit einem Model Checker auf gef\"{a}hrdende Situationen zu \"{u}berpr\"{u}fen. Viele Szenarien in den Anwendungsbereichen wie der Luftfahrt oder dem Stra{\ss}enverkehr beruhen jedoch auf kontinuierlichem Systemverhalten. In dieser Arbeit wird ein Verfahren vorgestellt, das ein kontinuierliches System in diskrete Automaten abstrahiert, sodass diese Automaten mit einem symbolischen Model Checker auf eine Sicherheitsspezifi kation \"{u}berpr\"{u}ft werden k\"{o}nnen. Das Verfahren wurde in Umgebung, in der diskrete Modelle erstellt und \"{u}berpr\"{u}ft werden k\"{o}nnen, als Prototyp umgesetzt. Dieser dient dazu anhand von Experimenten Eigenschaften des Verfahrens herauszufi nden.}, keywords = {hybrid model checking, model based verification, model checking}, pubstate = {published}, tppubtype = {mastersthesis} } Die Sicherheit von technischen System ist in vielen Gebieten wie der Luftfahrt oder im Straßenverkehr von elementarer Bedeutung für die Hersteller solcher Systeme wie für die Anwender. Ein Ansatz um die Sicherheit von diskreten Systemen zu zeigen, besteht darin, diese in einem diskreten Modell zu abstrahieren und anschließend mit einem Model Checker auf gefährdende Situationen zu überprüfen. Viele Szenarien in den Anwendungsbereichen wie der Luftfahrt oder dem Straßenverkehr beruhen jedoch auf kontinuierlichem Systemverhalten. In dieser Arbeit wird ein Verfahren vorgestellt, das ein kontinuierliches System in diskrete Automaten abstrahiert, sodass diese Automaten mit einem symbolischen Model Checker auf eine Sicherheitsspezifi kation überprüft werden können. Das Verfahren wurde in Umgebung, in der diskrete Modelle erstellt und überprüft werden können, als Prototyp umgesetzt. Dieser dient dazu anhand von Experimenten Eigenschaften des Verfahrens herauszufi nden. |
Dörfler, Stephan Protokollautomat für die Kommunikation zwischen Ladestation und Elektrofahrzeug Abschlussarbeit Otto-von-Guericke-Universität Magdeburg, 2015. Links | BibTeX | Schlagwörter: @mastersthesis{Doerfler2015, title = {Protokollautomat f\"{u}r die Kommunikation zwischen Ladestation und Elektrofahrzeug}, author = {Stephan D\"{o}rfler}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/05/thesis_doerfler_2015.pdf}, year = {2015}, date = {2015-04-09}, school = {Otto-von-Guericke-Universit\"{a}t Magdeburg}, type = {Bachelorarbeit}, keywords = {}, pubstate = {published}, tppubtype = {mastersthesis} } |
Lipaczewski, Michael; Prosvirnova, Tatiana; Ortmeier, Frank; Rauzy, Antoine; Struck, Simon Comparison of Modeling Formalisms for Safety Analyses: SAML and AltaRica Artikel Reliability Engineering & System Safety, 2015. Abstract | Links | BibTeX | Schlagwörter: Altarica, model-based, safety analysis, SAML @article{saml-vs-altarica-ress-elsevier-2015, title = {Comparison of Modeling Formalisms for Safety Analyses: SAML and AltaRica}, author = {Michael Lipaczewski and Tatiana Prosvirnova and Frank Ortmeier and Antoine Rauzy and Simon Struck}, url = {http://www.sciencedirect.com/science/article/pii/S0951832015001040}, year = {2015}, date = {2015-04-08}, journal = {Reliability Engineering & System Safety}, abstract = {Many states/transitions formalisms have been proposed in the literature to perform Safety Analyses. In this paper we compare two of them: SAML and AltaRica. These formalisms have been developed by different communities. Their “look-and-feel” are thus quite different. Yet, their underlying mathematical foundations are very similar: both of them rely on state automata. It is therefore of interest to study their ability to assess the reliability of systems, their respective advantages and drawbacks and to seek for opportunities of a cross fertilization.}, keywords = {Altarica, model-based, safety analysis, SAML}, pubstate = {published}, tppubtype = {article} } Many states/transitions formalisms have been proposed in the literature to perform Safety Analyses. In this paper we compare two of them: SAML and AltaRica. These formalisms have been developed by different communities. Their “look-and-feel” are thus quite different. Yet, their underlying mathematical foundations are very similar: both of them rely on state automata. It is therefore of interest to study their ability to assess the reliability of systems, their respective advantages and drawbacks and to seek for opportunities of a cross fertilization. |
Gonschorek, Tim A Backward Model Checking Approach with Slicing Abschlussarbeit Otto-von-Guericke-University Magdeburg, 2015. Abstract | BibTeX | Schlagwörter: formal verification, model checking @mastersthesis{Gonschorek2015, title = {A Backward Model Checking Approach with Slicing}, author = {Tim Gonschorek}, editor = {Tim Gonschorek }, year = {2015}, date = {2015-02-25}, address = {Universit\"{a}tsplatz 2, 39106 Magdeburg}, school = {Otto-von-Guericke-University Magdeburg}, abstract = {As software intensive safety critical systems are more and more introduced in our daily lives, it must be ensured that those systems safe. One method for ensuring that a system follows its given speci cation, i.e., does not have some unwanted behavior, is model checking. Although, nowadays larger models can be veri ed, model checking algorithms does not perform well in combination with complex real world problems. To overcome this diculties, this thesis proposes a new backward model checking algorithm using SMT programs instead of boolean encodings for representing the systems state. Additionally, it uses model based slicing to reduce the impact of the complexity of a given model. This thesis explains such an algorithm, which can be used for verifying safety properties. Further, this thesis presents a prototypical implementation of this algorithm. This prototype will be used to evaluate the algorithm in comparison to the BDD and the IC3 algorithms implemented in the model checker nuXmv. The evaluation shows that there are some cases where the proposed approach performs better than the given BDD algorithm.}, keywords = {formal verification, model checking}, pubstate = {published}, tppubtype = {mastersthesis} } As software intensive safety critical systems are more and more introduced in our daily lives, it must be ensured that those systems safe. One method for ensuring that a system follows its given speci cation, i.e., does not have some unwanted behavior, is model checking. Although, nowadays larger models can be veri ed, model checking algorithms does not perform well in combination with complex real world problems. To overcome this diculties, this thesis proposes a new backward model checking algorithm using SMT programs instead of boolean encodings for representing the systems state. Additionally, it uses model based slicing to reduce the impact of the complexity of a given model. This thesis explains such an algorithm, which can be used for verifying safety properties. Further, this thesis presents a prototypical implementation of this algorithm. This prototype will be used to evaluate the algorithm in comparison to the BDD and the IC3 algorithms implemented in the model checker nuXmv. The evaluation shows that there are some cases where the proposed approach performs better than the given BDD algorithm. |
Alatartsev, Sergey; Stellmacher, Sebastian; Ortmeier, Frank Robotic Task Sequencing Problem: A Survey Artikel Journal of Intelligent and Robotic Systems, 2015, ISSN: 1573-0409. Abstract | Links | BibTeX | Schlagwörter: @article{Alatartsev2015, title = {Robotic Task Sequencing Problem: A Survey}, author = { Sergey Alatartsev and Sebastian Stellmacher and Frank Ortmeier}, url = {http://link.springer.com/article/10.1007/s10846-015-0190-6 https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/05/Alatartsev_JIRS2015.pdf}, doi = {10.1007/s10846-015-0190-6}, issn = {1573-0409}, year = {2015}, date = {2015-01-01}, booktitle = {Journal of Intelligent and Robotic Systems}, journal = {Journal of Intelligent and Robotic Systems}, publisher = {Springer}, abstract = {Today, robotics is an important cornerstone of modern industrial production. Robots are used for numerous reasons including reliability and continuously high quality of work. The main decision factor is the overall efficiency of the robotic system in the production line. One key issue for this is the optimality of the whole set of robotic movements for industrial applications, which typically consist of multiple atomic tasks such as welding seams, drilling holes, etc. Currently, in many industrial scenarios such movements are optimized manually. This is costly and error-prone. Therefore, researchers have been working on algorithms for automatic computation of optimal trajectories for several years. This problem gets even more complicated due to multiple additional factors like redundant kinematics, collision avoidance, possibilities of ambiguous task performance, etc. This survey article summarizes and categorizes the approaches for optimization of the robotic task sequence. It provides an overview of existing combinatorial problems that are applied for robot task sequencing. It also highlights the strengths and the weaknesses of existing approaches as well as the challenges for future research in this domain. The article is meant for both scientists and practitioners. For scientists, it provides an overview on applied algorithmic approaches. For practitioners, it presents existing solutions, which are categorized according to the classes of input and output parameters.}, keywords = {}, pubstate = {published}, tppubtype = {article} } Today, robotics is an important cornerstone of modern industrial production. Robots are used for numerous reasons including reliability and continuously high quality of work. The main decision factor is the overall efficiency of the robotic system in the production line. One key issue for this is the optimality of the whole set of robotic movements for industrial applications, which typically consist of multiple atomic tasks such as welding seams, drilling holes, etc. Currently, in many industrial scenarios such movements are optimized manually. This is costly and error-prone. Therefore, researchers have been working on algorithms for automatic computation of optimal trajectories for several years. This problem gets even more complicated due to multiple additional factors like redundant kinematics, collision avoidance, possibilities of ambiguous task performance, etc. This survey article summarizes and categorizes the approaches for optimization of the robotic task sequence. It provides an overview of existing combinatorial problems that are applied for robot task sequencing. It also highlights the strengths and the weaknesses of existing approaches as well as the challenges for future research in this domain. The article is meant for both scientists and practitioners. For scientists, it provides an overview on applied algorithmic approaches. For practitioners, it presents existing solutions, which are categorized according to the classes of input and output parameters. |
2014 |
Plauschin, Mathias Klassifikation latenter Fingerspuren mithilfe von Smartphones Abschlussarbeit 2014. Links | BibTeX | Schlagwörter: @mastersthesis{Plauschin2014, title = {Klassifikation latenter Fingerspuren mithilfe von Smartphones}, author = {Mathias Plauschin}, url = {/cse/wp-content/uploads/2015/03/thesis_plauschin_2014.pdf}, year = {2014}, date = {2014-11-30}, keywords = {}, pubstate = {published}, tppubtype = {mastersthesis} } |
Fritsch, Michael Erhöhung von Quellcode-Wartbarkeit durch Entwurfsmusterautomatisierung Abschlussarbeit 2014. Links | BibTeX | Schlagwörter: Automation, Design Patterns, Maintainability @mastersthesis{Fritsch2014, title = {Erh\"{o}hung von Quellcode-Wartbarkeit durch Entwurfsmusterautomatisierung}, author = {Michael Fritsch}, editor = {Sebastian Nielebock and Frank Ortmeier}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/04/MA_Fritsch1.pdf}, year = {2014}, date = {2014-11-14}, keywords = {Automation, Design Patterns, Maintainability}, pubstate = {published}, tppubtype = {mastersthesis} } |
Dietze, Denis Semantische Veri kation von selbstbeschreibenden Geratekonfi gurationen Abschlussarbeit 2014. Links | BibTeX | Schlagwörter: @mastersthesis{Dietze2014, title = {Semantische Veri kation von selbstbeschreibenden Geratekonfi gurationen}, author = {Denis Dietze}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/03/thesis_dietze_2014.pdf}, year = {2014}, date = {2014-09-30}, keywords = {}, pubstate = {published}, tppubtype = {mastersthesis} } |
Dittmann, Denny Visualisierungskomponente für ein Hochspannungs-Gleichstrom-Übertragungs-Netz Überwachungssystem Abschlussarbeit 2014. Links | BibTeX | Schlagwörter: @mastersthesis{Dittmann2014, title = {Visualisierungskomponente f\"{u}r ein Hochspannungs-Gleichstrom-\"{U}bertragungs-Netz \"{U}berwachungssystem}, author = {Denny Dittmann}, url = {/cse/wp-content/uploads/2015/03/thesis_dittmann_2014.pdf}, year = {2014}, date = {2014-09-30}, keywords = {}, pubstate = {published}, tppubtype = {mastersthesis} } |
Hebecker, Tanja; Buchholz, Robert; Ortmeier, Frank Model-Based Local Path Planning for UAVs Artikel Journal of Intelligent & Robotic Systems, 78 , S. 127-142 , 2014, ISSN: 1573-0409. Abstract | Links | BibTeX | Schlagwörter: Grid map, Obstacle avoidance, Reachable set, Wavefront algorithm @article{hebecker2014JIRS, title = {Model-Based Local Path Planning for UAVs}, author = { Tanja Hebecker and Robert Buchholz and Frank Ortmeier}, editor = {Springer Netherlands}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/05/10.1007_s10846-014-0097-72.pdf http://link.springer.com/article/10.1007/s10846-014-0097-7}, doi = {10.1007/s10846-014-0097-7}, issn = {1573-0409}, year = {2014}, date = {2014-08-01}, journal = {Journal of Intelligent & Robotic Systems}, volume = {78}, pages = {127-142 }, abstract = {Autonomous aviation continuously becomes more and more important. Algorithms that enable this autonomy have developed quickly in the last years. This paper describes a concept for a reactive path planning algorithm. The aim is to develop a method for static obstacle avoidance of an unmanned aerial vehicle (UAV) by calculating collision-free paths within the field of view of a UAV’s obstacle detection sensor. In contrast to other algorithms, this method considers the properties of the obstacle detection sensors, plans paths that the UAV is able to track, and is applied in three-dimensional space without access to an inner loop controller. In this work we represent the field of view of a UAV as a grid map and apply the wavefront algorithm as the local path planning algorithm. We reduce the configuration space of UAVs within the field of view by calculating an approximated worst-case reachable set based on a linearized reference model. We evaluate the method with approximated specifications for the unmanned helicopters ARTIS and Yamaha RMAX, and with specifications for the obstacle detection sensors LIDAR {\textendash} and stereo camera. Experiments show that this method is able to generate collision-free paths in a region constricted by obstacles.}, keywords = {Grid map, Obstacle avoidance, Reachable set, Wavefront algorithm}, pubstate = {published}, tppubtype = {article} } Autonomous aviation continuously becomes more and more important. Algorithms that enable this autonomy have developed quickly in the last years. This paper describes a concept for a reactive path planning algorithm. The aim is to develop a method for static obstacle avoidance of an unmanned aerial vehicle (UAV) by calculating collision-free paths within the field of view of a UAV’s obstacle detection sensor. In contrast to other algorithms, this method considers the properties of the obstacle detection sensors, plans paths that the UAV is able to track, and is applied in three-dimensional space without access to an inner loop controller. In this work we represent the field of view of a UAV as a grid map and apply the wavefront algorithm as the local path planning algorithm. We reduce the configuration space of UAVs within the field of view by calculating an approximated worst-case reachable set based on a linearized reference model. We evaluate the method with approximated specifications for the unmanned helicopters ARTIS and Yamaha RMAX, and with specifications for the obstacle detection sensors LIDAR – and stereo camera. Experiments show that this method is able to generate collision-free paths in a region constricted by obstacles. |
Jagla, Tim Benedict Cross-Platform Remote Control of Web-Based Media Abschlussarbeit 2014. Abstract | Links | BibTeX | Schlagwörter: mobile devices, web communication @mastersthesis{thesis-jagla-2014, title = {Cross-Platform Remote Control of Web-Based Media}, author = {Tim Benedict Jagla}, url = {/cse/wp-content/uploads/2015/03/thesis-jagla-2014.pdf}, year = {2014}, date = {2014-06-19}, abstract = {A multitude of network and media related topics will be discussed in this work. From the basics of networking and different web communication techniques as well as media preparation and provision a concept will be derived to solve the problem of the general lack in web standard compliant browsers for mobile devices within the domain of web applications. A prototypical implementation will be presented and critically examined.}, keywords = {mobile devices, web communication}, pubstate = {published}, tppubtype = {mastersthesis} } A multitude of network and media related topics will be discussed in this work. From the basics of networking and different web communication techniques as well as media preparation and provision a concept will be derived to solve the problem of the general lack in web standard compliant browsers for mobile devices within the domain of web applications. A prototypical implementation will be presented and critically examined. |
Heumüller, Robert; Quante, Jochen; Thums, Andreas Parsing Variant C Code: An Evaluation on Automotive Software Inproceedings GI, (Hrsg.): 16. Workshop Software-Reengineering & Evolution, 2014. BibTeX | Schlagwörter: c, parsing, preprocessor, Software product line @inproceedings{Heum\"{u}ller2014, title = {Parsing Variant C Code: An Evaluation on Automotive Software}, author = {Robert Heum\"{u}ller and Jochen Quante and Andreas Thums}, editor = {GI}, year = {2014}, date = {2014-04-30}, booktitle = {16. Workshop Software-Reengineering & Evolution}, keywords = {c, parsing, preprocessor, Software product line}, pubstate = {published}, tppubtype = {inproceedings} } |
Heumüller, Robert VECS Dataflow - A SAML Language Extension Allowing Intuitive Creation of Formal Automata Specifications Abschlussarbeit 2014. Links | BibTeX | Schlagwörter: dataflow, model-based, model-checking, safety @mastersthesis{thesis-heumueller-2014, title = {VECS Dataflow - A SAML Language Extension Allowing Intuitive Creation of Formal Automata Specifications}, author = {Robert Heum\"{u}ller}, url = {/cse/wp-content/uploads/2015/03/thesis.pdf}, year = {2014}, date = {2014-04-10}, type = {Bachelor\'s Thesis}, keywords = {dataflow, model-based, model-checking, safety}, pubstate = {published}, tppubtype = {mastersthesis} } |
Lipaczewski, Michael; Filax, Marco; Ortmeier, Frank Bringing VECS to the World - Challenges and Accomplishments in Teaching of Formal Model Analysis Inproceedings European Conference on Software Engineering Education. - Herzogenrath : Shaker, S. 217-228, 2014. BibTeX | Schlagwörter: model-based, VECS @inproceedings{FODB:80901605, title = {Bringing VECS to the World - Challenges and Accomplishments in Teaching of Formal Model Analysis}, author = { Michael Lipaczewski and Marco Filax and Frank Ortmeier}, year = {2014}, date = {2014-01-01}, booktitle = {European Conference on Software Engineering Education. - Herzogenrath : Shaker}, pages = {217-228}, keywords = {model-based, VECS}, pubstate = {published}, tppubtype = {inproceedings} } |
Gonschorek, Tim; Filax, Marco; Lipaczewski, Michael; Ortmeier, Frank VECS - Verification Enviroment for Critical Systems - Tool Supported Formal Modeling an Verification Buchkapitel IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment. - Magdeburg : Univ., S. 63-64, 2014. Links | BibTeX | Schlagwörter: model-based, VECS @inbook{FODB:80901373, title = {VECS - Verification Enviroment for Critical Systems - Tool Supported Formal Modeling an Verification}, author = { Tim Gonschorek and Marco Filax and Michael Lipaczewski and Frank Ortmeier}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/07/gonshorek_VECS_2014.pdf}, year = {2014}, date = {2014-01-01}, booktitle = {IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment. - Magdeburg : Univ.}, pages = {63-64}, keywords = {model-based, VECS}, pubstate = {published}, tppubtype = {inbook} } |
Heumüller, Robert; Lipaczewski, Michael; Ortmeier, Frank A Dataflow Notation for SAML - Formal Modeling Without Fearing Timing Constraints Inproceedings IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment. - Magdeburg : Univ., S. 43-50, 2014. BibTeX | Schlagwörter: model-based, VECS @inproceedings{FODB:80901349, title = {A Dataflow Notation for SAML - Formal Modeling Without Fearing Timing Constraints}, author = { Robert Heum\"{u}ller and Michael Lipaczewski and Frank Ortmeier}, year = {2014}, date = {2014-01-01}, booktitle = {IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment. - Magdeburg : Univ.}, pages = {43-50}, keywords = {model-based, VECS}, pubstate = {published}, tppubtype = {inproceedings} } |
Filax, Marco; Gonschorek, Tim; Lipaczewski, Michael; Ortmeier, Frank On Traceability of Informal Specifications for Model-Based Verification Inproceedings IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment., S. 11-18, Magdeburg : Univ., 2014. Abstract | Links | BibTeX | Schlagwörter: model-based, VECS, VIP-MoBaSA @inproceedings{FODB:80901202, title = {On Traceability of Informal Specifications for Model-Based Verification}, author = { Marco Filax and Tim Gonschorek and Michael Lipaczewski and Frank Ortmeier}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/07/filax_IMBSA_2014.pdf}, year = {2014}, date = {2014-01-01}, booktitle = {IMBSA 2014: short & tutorial proceedings of the 4th international symposium on model based safety assessment.}, pages = {11-18}, publisher = {Magdeburg : Univ.}, abstract = {Safety critical systems are often specified by a set of informal requirements. The fulfillment of those requirements has, in general, to be verified through external assessors. In most cases models (i.e. UML diagrams) are used to communicate system architectures and decide whether a given system meets its requirements. Even though, there already exist multiple approaches to verify safety critical systems and assessors would benefit from the usage of model-based system verifications, they are not commonly used in industry. We propose a traceable modeling approach for verifying safety critical systems specified with a set of informal unstructured requirements. The proposed process is divided into three phases: the analysis of the given set of informal requirements, semi-formalization and formalization.}, keywords = {model-based, VECS, VIP-MoBaSA}, pubstate = {published}, tppubtype = {inproceedings} } Safety critical systems are often specified by a set of informal requirements. The fulfillment of those requirements has, in general, to be verified through external assessors. In most cases models (i.e. UML diagrams) are used to communicate system architectures and decide whether a given system meets its requirements. Even though, there already exist multiple approaches to verify safety critical systems and assessors would benefit from the usage of model-based system verifications, they are not commonly used in industry. We propose a traceable modeling approach for verifying safety critical systems specified with a set of informal unstructured requirements. The proposed process is divided into three phases: the analysis of the given set of informal requirements, semi-formalization and formalization. |
Mäurer, Lukas; Hebecker, Tanja; Stolte, Torben; Lipaczewski, Michael; Möhrstädt, Uwe; Ortmeier, Frank On Bringing Object-Oriented Software Metrics into the Model-Based World - Verifying ISO 26262 Compliance in Simulink Inproceedings Publishing, Springer International (Hrsg.): System analysis and modeling: models and reusability. - Berlin [u.a.] : Springer, S. 207-222, Springer, 2014, ISBN: 978-3-319-11743-0. Abstract | Links | BibTeX | Schlagwörter: @inproceedings{FODB:80901022, title = {On Bringing Object-Oriented Software Metrics into the Model-Based World - Verifying ISO 26262 Compliance in Simulink}, author = { Lukas M\"{a}urer and Tanja Hebecker and Torben Stolte and Michael Lipaczewski and Uwe M\"{o}hrst\"{a}dt and Frank Ortmeier}, editor = {Springer International Publishing}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/05/maeurer2014SAM.pdf http://link.springer.com/chapter/10.1007%2F978-3-319-11743-0_15}, doi = {10.1007/978-3-319-11743-0_15}, isbn = {978-3-319-11743-0}, year = {2014}, date = {2014-01-01}, booktitle = {System analysis and modeling: models and reusability. - Berlin [u.a.] : Springer}, pages = {207-222}, publisher = {Springer}, series = {Lecture notes in computer science; 8769}, abstract = {For ensuring functional safety of electrical/electronic systems, it is necessary to exclude malfunctions from hardware and software as well as from the interaction of both. In today’s passenger vehicles, more and more safety critical functionalities are implemented in software. Thus, its importance for functional safety increases. The dominating safety standard for the automotive domain (ISO 26262) considers the software part and defines requirements for safety critical software. However, applying and fulfilling the standard is a major problem in industry. In this context, the paper presents a novel metric-based approach to evaluate dataflow-oriented software architectures used in many model-driven processes regarding the fulfillment of requirements defined by ISO 26262 (in particular part 6). The core idea is to derive metrics for model-based software from already existing, well-performing metrics elaborated for other programming paradigms. To link metrics to requirements fulfillment of ISO 26262, we briefly sketch the factor-criteriametrics paradigm for this problem. Technically, this paper presents a generic meta-model for dataflow systems, which is used to define the metrics. We implemented this meta-model and the metrics as a prototype for Matlab Simulink. As examples, two models of a 400 kW full Drive-by- Wire experimental vehicle with all-wheel-steering, all-wheel-drive, and electro-mechanical brakes are analyzed using this prototype.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } For ensuring functional safety of electrical/electronic systems, it is necessary to exclude malfunctions from hardware and software as well as from the interaction of both. In today’s passenger vehicles, more and more safety critical functionalities are implemented in software. Thus, its importance for functional safety increases. The dominating safety standard for the automotive domain (ISO 26262) considers the software part and defines requirements for safety critical software. However, applying and fulfilling the standard is a major problem in industry. In this context, the paper presents a novel metric-based approach to evaluate dataflow-oriented software architectures used in many model-driven processes regarding the fulfillment of requirements defined by ISO 26262 (in particular part 6). The core idea is to derive metrics for model-based software from already existing, well-performing metrics elaborated for other programming paradigms. To link metrics to requirements fulfillment of ISO 26262, we briefly sketch the factor-criteriametrics paradigm for this problem. Technically, this paper presents a generic meta-model for dataflow systems, which is used to define the metrics. We implemented this meta-model and the metrics as a prototype for Matlab Simulink. As examples, two models of a 400 kW full Drive-by- Wire experimental vehicle with all-wheel-steering, all-wheel-drive, and electro-mechanical brakes are analyzed using this prototype. |
Nykolaichuk, Mykhaylo; Lipaczewski, Michael; Liebusch, Tino; Ortmeier, Frank On Efficiently Specifying Models for Model Checking Inproceedings Proceedings of 4th International Symposium on Model Based Safety and Assessment (IMBSA 2014), 2014. Abstract | Links | BibTeX | Schlagwörter: model-based, VECS @inproceedings{nykolaychukIMBSA_2014, title = {On Efficiently Specifying Models for Model Checking}, author = { Mykhaylo Nykolaichuk and Michael Lipaczewski and Tino Liebusch and Frank Ortmeier}, url = {http://link.springer.com/chapter/10.1007/978-3-319-12214-4_2 https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/Nykolaychuk_IMBSA_2014.pdf }, year = {2014}, date = {2014-01-01}, booktitle = {Proceedings of 4th International Symposium on Model Based Safety and Assessment (IMBSA 2014)}, abstract = {Using formal methods for quality assurance is recommended in many standards for safety critical applications. In most industrial contexts, model checking is the only viable option for formal verification, as interactive approaches often require very highly specialized experts. However, model checking typically suffers from the well-known state-space explosion problem. Due to this problem, engineers typically have to decide on a trade-off between readability and completeness of the model on one side, and the state space size, and thus, computational feasibility on the other. In this paper, we propose a method for reducing the state space by restructuring models. The core idea is to introduce as few additional states as possible by model design making state transitions more complex. To avoid unreadability and infeasible model sizes, we introduce a concept for hierarchical boolean formulas to efficiently specify state transitions. For evaluation purposes, we applied this approach to a case study using the VECS toolkit. In this exemplary case study, we were able to reduce the state space size significantly and make verification time feasible.}, keywords = {model-based, VECS}, pubstate = {published}, tppubtype = {inproceedings} } Using formal methods for quality assurance is recommended in many standards for safety critical applications. In most industrial contexts, model checking is the only viable option for formal verification, as interactive approaches often require very highly specialized experts. However, model checking typically suffers from the well-known state-space explosion problem. Due to this problem, engineers typically have to decide on a trade-off between readability and completeness of the model on one side, and the state space size, and thus, computational feasibility on the other. In this paper, we propose a method for reducing the state space by restructuring models. The core idea is to introduce as few additional states as possible by model design making state transitions more complex. To avoid unreadability and infeasible model sizes, we introduce a concept for hierarchical boolean formulas to efficiently specify state transitions. For evaluation purposes, we applied this approach to a case study using the VECS toolkit. In this exemplary case study, we were able to reduce the state space size significantly and make verification time feasible. |
Nielebock, Sebastian; Gonschorek, Tim; Ortmeier, Frank A Graphical Notation for Probabilistic Specifications Inproceedings 2014, (Verification and Assurance - Second VeriSure Workshop 2014). Abstract | Links | BibTeX | Schlagwörter: graphical specification patterns, specification, specification patterns, verification @inproceedings{nielebock_et_al_verisure_2014, title = {A Graphical Notation for Probabilistic Specifications}, author = { Sebastian Nielebock and Tim Gonschorek and Frank Ortmeier}, url = {http://www.easychair.org/smart-program/VSL2014/VeriSure-2014-07-23.html#talk:3203 https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/05/nielebock_verisure_20142.pdf}, year = {2014}, date = {2014-01-01}, abstract = {Nowadays formal methods represent a powerful but in practice not well supported way for verification. One reason among others for this is that such methods are often conceived of being too theoretical, can likely be misunderstood by non-experts, and notations are therefore misapplied. For example to specify formal specifications, complex logics are state-of-the-art, especially for probabilistic verification properties. It is not only that users are unable to construct correct specifications but they also miss to understand what is meant by the verification results based on the specification. In this paper we address this problem and endorse the usage of a graphical notation to construct such specification properties, especially probabilistic ones. We present how such a notation may look and emphasize that one single notation is sufficient to solve both lack of comprehensibility of the specification as well as of the verification results. Moreover, we extract some future research directions.}, note = {Verification and Assurance - Second VeriSure Workshop 2014}, keywords = {graphical specification patterns, specification, specification patterns, verification}, pubstate = {published}, tppubtype = {inproceedings} } Nowadays formal methods represent a powerful but in practice not well supported way for verification. One reason among others for this is that such methods are often conceived of being too theoretical, can likely be misunderstood by non-experts, and notations are therefore misapplied. For example to specify formal specifications, complex logics are state-of-the-art, especially for probabilistic verification properties. It is not only that users are unable to construct correct specifications but they also miss to understand what is meant by the verification results based on the specification. In this paper we address this problem and endorse the usage of a graphical notation to construct such specification properties, especially probabilistic ones. We present how such a notation may look and emphasize that one single notation is sufficient to solve both lack of comprehensibility of the specification as well as of the verification results. Moreover, we extract some future research directions. |
Alatartsev, Sergey; Belov, Anton; Nykolaichuk, Mykhaylo; Ortmeier, Frank Robot Trajectory Optimization for the Relaxed End-Effector Path Inproceedings Proceedings of the 11th International Conference on Informatics in Control, Automation and Robotics (ICINCO), 2014. Abstract | Links | BibTeX | Schlagwörter: @inproceedings{Alatartsev2014_1, title = {Robot Trajectory Optimization for the Relaxed End-Effector Path}, author = { Sergey Alatartsev and Anton Belov and Mykhaylo Nykolaichuk and Frank Ortmeier}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/05/Alatartsev_ICINCO2014.pdf}, year = {2014}, date = {2014-01-01}, booktitle = {Proceedings of the 11th International Conference on Informatics in Control, Automation and Robotics (ICINCO)}, abstract = {In this paper we consider the trajectory optimization problem for the effective tasks performed by industrial robots, e.g., welding, cutting or camera inspection. The distinctive feature of such tasks is that a robot has to follow a certain end-effector path with its motion law. For example, welding a line with a certain velocity has an even influence on the surface. The end-effector path and its motion law depend on the industrial process requirements. They are calculated without considering robot kinematics, hence, are often “awkward” for the robot execution, e.g., cause high jerks in the robot’s joints. In this paper we present the trajectory optimization problem where the end-effector path is allowed to have a certain deviation. Such path is referred to as relaxed path. The goal of the paper is to make use of this freedom and construct the minimal-cost robot trajectory. To demonstrate the potential of the problem, jerk of the robot joint trajectory was minimized.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } In this paper we consider the trajectory optimization problem for the effective tasks performed by industrial robots, e.g., welding, cutting or camera inspection. The distinctive feature of such tasks is that a robot has to follow a certain end-effector path with its motion law. For example, welding a line with a certain velocity has an even influence on the surface. The end-effector path and its motion law depend on the industrial process requirements. They are calculated without considering robot kinematics, hence, are often “awkward” for the robot execution, e.g., cause high jerks in the robot’s joints. In this paper we present the trajectory optimization problem where the end-effector path is allowed to have a certain deviation. Such path is referred to as relaxed path. The goal of the paper is to make use of this freedom and construct the minimal-cost robot trajectory. To demonstrate the potential of the problem, jerk of the robot joint trajectory was minimized. |
Alatartsev, Sergey; Ortmeier, Frank Improving the Sequence of Robotic Tasks with Freedom of Execution Inproceedings IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), 2014. Abstract | Links | BibTeX | Schlagwörter: @inproceedings{Alatartsev2014, title = {Improving the Sequence of Robotic Tasks with Freedom of Execution}, author = { Sergey Alatartsev and Frank Ortmeier}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/05/Alatartsev_IROS2014.pdf}, year = {2014}, date = {2014-01-01}, booktitle = {IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)}, abstract = {An industrial robot’s workflow typically consists of a set of tasks that have to be repeated multiple times. A task could be, for example, welding a seam or cutting a hole. The efficiency with which the robot performs the sequence of tasks is an important factor in most production domains. The more often a set of tasks can be performed by a robot the more advantages it provides to the company. In most practical scenarios, the majority of tasks have a certain freedom of execution. For example, closed-contour welding task can often be started and finished at any point of the curve. Also the exact orientation of the welding torch is not fixed, but may be in a certain range, e.g., between 85◦ and 95◦ . Currently, these degrees of freedom are used to manually generate robot trajectories. However, their quality highly depends on skills and experience of the robot programmer. In this paper we propose a method that is able to automatically improve the given sequence of robotic tasks by adding certain freedom to (i) the position of the starting point along the curve, (ii) the orientation of the end-effector and (iii) the robot configuration. The proposed approach does not depend on the production domain and could be combined with any algorithm for constructing the initial task sequence. We evaluate the algorithm on a realistic case study and show that it could significantly improve the production time on the test instances from the cutting-deburring domain.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } An industrial robot’s workflow typically consists of a set of tasks that have to be repeated multiple times. A task could be, for example, welding a seam or cutting a hole. The efficiency with which the robot performs the sequence of tasks is an important factor in most production domains. The more often a set of tasks can be performed by a robot the more advantages it provides to the company. In most practical scenarios, the majority of tasks have a certain freedom of execution. For example, closed-contour welding task can often be started and finished at any point of the curve. Also the exact orientation of the welding torch is not fixed, but may be in a certain range, e.g., between 85◦ and 95◦ . Currently, these degrees of freedom are used to manually generate robot trajectories. However, their quality highly depends on skills and experience of the robot programmer. In this paper we propose a method that is able to automatically improve the given sequence of robotic tasks by adding certain freedom to (i) the position of the starting point along the curve, (ii) the orientation of the end-effector and (iii) the robot configuration. The proposed approach does not depend on the production domain and could be combined with any algorithm for constructing the initial task sequence. We evaluate the algorithm on a realistic case study and show that it could significantly improve the production time on the test instances from the cutting-deburring domain. |
2013 |
Nielebock, Sebastian Komposition gewöhnlicher Differentialgleichungen mit sicherheitsrelevanten Zustandsautomaten Abschlussarbeit 2013. Links | BibTeX | Schlagwörter: differential equations, safety, state-based @mastersthesis{thesis-nielebock-2013, title = {Komposition gew\"{o}hnlicher Differentialgleichungen mit sicherheitsrelevanten Zustandsautomaten}, author = {Sebastian Nielebock}, url = {/cse/wp-content/uploads/2015/03/MA_Nielebock_final_version.pdf}, year = {2013}, date = {2013-09-17}, keywords = {differential equations, safety, state-based}, pubstate = {published}, tppubtype = {mastersthesis} } |
Gonschorek, Tim Methodik zur Abstraktion kontinuierlicher Differentialgleichungen Abschlussarbeit Otto-von-Guericke-University Magdeburg, 2013. Abstract | Links | BibTeX | Schlagwörter: hybrid model checking, model based verification @mastersthesis{Gonschorek2013, title = {Methodik zur Abstraktion kontinuierlicher Differentialgleichungen}, author = {Tim Gonschorek}, editor = {Tim Gonschorek}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/BA_2013_Gonschorek.pdf}, year = {2013}, date = {2013-06-19}, address = {Universit\"{a}tsplatz 2, 39106 Magdeburg}, school = {Otto-von-Guericke-University Magdeburg}, abstract = {Reale Phanomene aus Natur und Technik konnen oft nur durch kontinuierliche Modelle abgebildet werden. Mithilfe eines Modelchecker konnen Modelle auf Grundlage einer vorgegebenen Spezi kation automatisiert veri ziert werden. Jedoch konnen die meisten Modelchecker nur mit diskreten Modellen umgehen. Deshalb kann ein kontinuierliches Modell nicht direkt mit einem Modelchecker gepruft werden. Diese Arbeit prasentiert eine Methodik, mit der es moglich ist, kontinuierliche Modelle sowohl im Zeitbereich, als auch im Wertebereich zu diskretisieren. Das Modell wird dazu in einen endlichen, diskreten Zustandsautomaten umgewandelt. Es wird ein konkretes Vorgehen erklart, um kontinuierliche Di erentialgleichungen in Di erenzengleichungen umzuwandeln, die in Zustandsubergangen eingebunden werden konnen. Dadurch wird es moglich, die Vorteile eins Modelcheckers fur die Veri kation kontinuierlicher Modelle zu nutzen. Um sicherzustellen, dass der erstellte Automat das kontinuierliche Modell hinreichend abstrahiert, um mithilfe eines Modelcheckers Aussagen tre en zu konnen, wird die Methodik anhand eines Beispielmodells evaluiert. Um die praktische Anwendbarkeit zu zeigen, wird ein komplexe Fallstudie von einem Modelica-Modell in einen SAML-Automaten transformiert. DesWeiteren wird die Architektur einer Java-Komponente vorgestellt, mit der eine Modelica-Datei in eine SAML-Datei transformiert werden kann, um sie mithilfe eines Modelcheckers gegen eine vorgegebene Spezi kation zu veri zieren. Diese Komponente soll als erste Implementation eines Importers fur Modelica-Dateien in eine SAML Umgebung dienen.}, keywords = {hybrid model checking, model based verification}, pubstate = {published}, tppubtype = {mastersthesis} } Reale Phanomene aus Natur und Technik konnen oft nur durch kontinuierliche Modelle abgebildet werden. Mithilfe eines Modelchecker konnen Modelle auf Grundlage einer vorgegebenen Spezi kation automatisiert veri ziert werden. Jedoch konnen die meisten Modelchecker nur mit diskreten Modellen umgehen. Deshalb kann ein kontinuierliches Modell nicht direkt mit einem Modelchecker gepruft werden. Diese Arbeit prasentiert eine Methodik, mit der es moglich ist, kontinuierliche Modelle sowohl im Zeitbereich, als auch im Wertebereich zu diskretisieren. Das Modell wird dazu in einen endlichen, diskreten Zustandsautomaten umgewandelt. Es wird ein konkretes Vorgehen erklart, um kontinuierliche Di erentialgleichungen in Di erenzengleichungen umzuwandeln, die in Zustandsubergangen eingebunden werden konnen. Dadurch wird es moglich, die Vorteile eins Modelcheckers fur die Veri kation kontinuierlicher Modelle zu nutzen. Um sicherzustellen, dass der erstellte Automat das kontinuierliche Modell hinreichend abstrahiert, um mithilfe eines Modelcheckers Aussagen tre en zu konnen, wird die Methodik anhand eines Beispielmodells evaluiert. Um die praktische Anwendbarkeit zu zeigen, wird ein komplexe Fallstudie von einem Modelica-Modell in einen SAML-Automaten transformiert. DesWeiteren wird die Architektur einer Java-Komponente vorgestellt, mit der eine Modelica-Datei in eine SAML-Datei transformiert werden kann, um sie mithilfe eines Modelcheckers gegen eine vorgegebene Spezi kation zu veri zieren. Diese Komponente soll als erste Implementation eines Importers fur Modelica-Dateien in eine SAML Umgebung dienen. |
Ortmeier, Frank; Struck, Simon; Meinicke, Jens; Quante, Jochen A Pragmatic Approach For Debugging Parameter-Driven Software Inproceedings Kowalewski, Stefan; Rumpe, Bernhard (Hrsg.): Software Engineering 2013, S. 199-212, 2013. Abstract | Links | BibTeX | Schlagwörter: debugging, embedded software, parameter driven software @inproceedings{SE2013-Param, title = {A Pragmatic Approach For Debugging Parameter-Driven Software}, author = { Frank Ortmeier and Simon Struck and Jens Meinicke and Jochen Quante}, editor = {Stefan Kowalewski and Bernhard Rumpe}, url = {https://subs.emis.de/LNI/Proceedings/Proceedings213/199.pdf}, year = {2013}, date = {2013-02-01}, booktitle = {Software Engineering 2013}, volume = {213}, pages = {199-212}, series = {Lecture Notes in Informatics}, abstract = {Debugging a software system is a difficult and time consuming task. This is in particular true for control software in technical systems. Such software typically has a very long life cycle, has been programmed by aengineers and not computer scientists, and has been extended numerous times to adapt to a changing environment and new technical products. As a consequence, the software is often not in an ideal condition. Additionally, such software often faces real-time requirements, which often makes it impossible to use dynamic techniques (e.,g., single-stepping or tracing). Technically, such software is often realized in C/C++ in a rather imperative programming style. Adaptation and extension is often done by adding configuration parameters. As a consequence, checking for correctness as well as debugging requires to consider the source code as well as its configuration parameters. In this paper, we propose a pragmatic approach to debugging such Software. The approach was designed such that (a) it does not require any understanding of the software before starting, and (b) that it can be easily used by programmers and not only by experts. We evaluated the approach on an artificial but realistic case study provided by Robert Bosch GmbH.}, keywords = {debugging, embedded software, parameter driven software}, pubstate = {published}, tppubtype = {inproceedings} } Debugging a software system is a difficult and time consuming task. This is in particular true for control software in technical systems. Such software typically has a very long life cycle, has been programmed by aengineers and not computer scientists, and has been extended numerous times to adapt to a changing environment and new technical products. As a consequence, the software is often not in an ideal condition. Additionally, such software often faces real-time requirements, which often makes it impossible to use dynamic techniques (e.,g., single-stepping or tracing). Technically, such software is often realized in C/C++ in a rather imperative programming style. Adaptation and extension is often done by adding configuration parameters. As a consequence, checking for correctness as well as debugging requires to consider the source code as well as its configuration parameters. In this paper, we propose a pragmatic approach to debugging such Software. The approach was designed such that (a) it does not require any understanding of the software before starting, and (b) that it can be easily used by programmers and not only by experts. We evaluated the approach on an artificial but realistic case study provided by Robert Bosch GmbH. |
Ortmeier, Frank; Struck, Simon; Güdemann, Matthias Efficient Optimization of Large Probabilistic Models Artikel Elsevier Journal of Systems and Software, 03/78 , 2013. Abstract | Links | BibTeX | Schlagwörter: model checking, optimization, safety @article{2013-safety-opti-jss, title = {Efficient Optimization of Large Probabilistic Models}, author = { Frank Ortmeier and Simon Struck and Matthias G\"{u}demann}, url = {http://hal.inria.fr/docs/00/81/66/36/PDF/Struck-Gudemann-Ortmeier-13.pdf}, year = {2013}, date = {2013-01-01}, journal = {Elsevier Journal of Systems and Software}, volume = {03/78}, abstract = {The development of safety critical systems often requires design decisions which influence not only dependability, but also other properties which are often even antagonistic to dependability, e.g., cost. Finding good compromises c onsidering different goals while at the same time guaranteeing sufficiently high saf ety of a system is a very difficult task. We propose an integrated approach for modeling, analysis and optim ization of safety critical systems. It is fully automated with an implementat ion based on the Eclipse platform. The approach is tool-independent, different a nalysis tools can be used and there exists an API for the integration of different optimiza- tion and estimation algorithms. For safety critical systems, a very important criterion is the hazard occurrence probability, whose computation can be quite costly. Therefore we also provide means to speed up optimization by devising different combinations of stochastic estimators and illustrate how t hey can be integrated into the approach. We illustrate the approach on relevant case-studies and provide ex perimental details to validate its effectiveness and applicability.}, keywords = {model checking, optimization, safety}, pubstate = {published}, tppubtype = {article} } The development of safety critical systems often requires design decisions which influence not only dependability, but also other properties which are often even antagonistic to dependability, e.g., cost. Finding good compromises c onsidering different goals while at the same time guaranteeing sufficiently high saf ety of a system is a very difficult task. We propose an integrated approach for modeling, analysis and optim ization of safety critical systems. It is fully automated with an implementat ion based on the Eclipse platform. The approach is tool-independent, different a nalysis tools can be used and there exists an API for the integration of different optimiza- tion and estimation algorithms. For safety critical systems, a very important criterion is the hazard occurrence probability, whose computation can be quite costly. Therefore we also provide means to speed up optimization by devising different combinations of stochastic estimators and illustrate how t hey can be integrated into the approach. We illustrate the approach on relevant case-studies and provide ex perimental details to validate its effectiveness and applicability. |
Trojahn, Matthias; Arndt, Florian; Ortmeier, Frank Authentication with Keystroke Dynamics on Touchscreen Keypads - Effect of different N-Graph Combinations Konferenz MOBILITY 2013, The Third International Conference on Mobile Services, Resources, and Users, 2013. BibTeX | Schlagwörter: @conference{Trojahn.2013m, title = {Authentication with Keystroke Dynamics on Touchscreen Keypads - Effect of different N-Graph Combinations}, author = { Matthias Trojahn and Florian Arndt and Frank Ortmeier}, year = {2013}, date = {2013-01-01}, booktitle = {MOBILITY 2013, The Third International Conference on Mobile Services, Resources, and Users}, pages = {114-119}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
Trojahn, Matthias; Ortmeier, Frank KeyGait Framework for Continuously Biometric Authentication during Usage of a Smartphone Konferenz MOBILITY 2013, The Third International Conference on Mobile Services, Resources, and Users, 2013. BibTeX | Schlagwörter: @conference{Trojahn.2013l, title = {KeyGait Framework for Continuously Biometric Authentication during Usage of a Smartphone}, author = { Matthias Trojahn and Frank Ortmeier}, year = {2013}, date = {2013-01-01}, booktitle = {MOBILITY 2013, The Third International Conference on Mobile Services, Resources, and Users}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
Alatartsev, Sergey; Ortmeier, Frank Path Planning for Industrial Robots Among Multiple Underspecified Tasks Inproceedings Proceedings of the Magdeburger-Informatik-Tage 2. Doktorandentagung (MIT), 2013. Abstract | Links | BibTeX | Schlagwörter: @inproceedings{MIT2013, title = {Path Planning for Industrial Robots Among Multiple Underspecified Tasks}, author = {Sergey Alatartsev and Frank Ortmeier}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/05/Alatartsev_DoctoralDay2013.pdf}, year = {2013}, date = {2013-01-01}, booktitle = {Proceedings of the Magdeburger-Informatik-Tage 2. Doktorandentagung (MIT)}, abstract = {This paper is an overview of the currently going PhD project. The main goal of the project is to optimize a sequence of industrial robotic tasks. We want to make use of the fact that robotic tasks often allow some freedom during the execution. In contrast, this extra freedom is ignored by state-of-the-art approaches. This work refers to extra freedom as under-specification. This paper presents a comprehensive overview of the state-of-the-art approaches in task sequencing. We state the thesis goals and make a short introduction to the methods developed within the PhD project. Work packages are formed based on the list of unaccomplished goals. }, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } This paper is an overview of the currently going PhD project. The main goal of the project is to optimize a sequence of industrial robotic tasks. We want to make use of the fact that robotic tasks often allow some freedom during the execution. In contrast, this extra freedom is ignored by state-of-the-art approaches. This work refers to extra freedom as under-specification. This paper presents a comprehensive overview of the state-of-the-art approaches in task sequencing. We state the thesis goals and make a short introduction to the methods developed within the PhD project. Work packages are formed based on the list of unaccomplished goals. |
Ortmeier, Frank; Lipaczewski, Michael Teaching and Training Formal Methods for Safety Critical Systems Konferenz Proceedings of the 39th Euromicro Conference on Iv Software Engineering and Advanced Applications (SEAA 2013), 2013. Abstract | Links | BibTeX | Schlagwörter: model-based, VECS @conference{teaching-saml_SEAA2013, title = {Teaching and Training Formal Methods for Safety Critical Systems}, author = { Frank Ortmeier and Michael Lipaczewski}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/Teaching_and_Training_Formal_Methods_for_Safety_Critical-_ystems.pdf}, year = {2013}, date = {2013-01-01}, booktitle = {Proceedings of the 39th Euromicro Conference on Iv Software Engineering and Advanced Applications (SEAA 2013)}, abstract = {Embedded systems become a major part in many domains. This also involves systems which might create heavy damages and injuries when they fail. However, because of the rising number of software components used within this embedded hardware, safety-related problems are hard to discover, and it is even harder to prove that there are none. One approach to guarantee the correctness of a system is model-based safety analysis. They rely on an abstract representation of the system which can then be analyzed using model checkers. The results of these analysis are in general much more precise and often reveal surprising results of failure combinations, where no one had ever thought about before. Nevertheless model-based safety analysis is not used widely. Mainly because it is not well-known and hard to apply to current safety standards which rely on manual approaches. Another fact might be, that most approaches are scientific and in most cases prototypes that are hard to use. In this paper we present some ideas and first steps towards an easy to learn and easy to use model based safety approach. Additionally we present different user-interfaces that are supposed to support the user in his learning.}, keywords = {model-based, VECS}, pubstate = {published}, tppubtype = {conference} } Embedded systems become a major part in many domains. This also involves systems which might create heavy damages and injuries when they fail. However, because of the rising number of software components used within this embedded hardware, safety-related problems are hard to discover, and it is even harder to prove that there are none. One approach to guarantee the correctness of a system is model-based safety analysis. They rely on an abstract representation of the system which can then be analyzed using model checkers. The results of these analysis are in general much more precise and often reveal surprising results of failure combinations, where no one had ever thought about before. Nevertheless model-based safety analysis is not used widely. Mainly because it is not well-known and hard to apply to current safety standards which rely on manual approaches. Another fact might be, that most approaches are scientific and in most cases prototypes that are hard to use. In this paper we present some ideas and first steps towards an easy to learn and easy to use model based safety approach. Additionally we present different user-interfaces that are supposed to support the user in his learning. |
Alatartsev, Sergey; Mersheeva, Vera; Augustine, Marcus; Ortmeier, Frank On Optimizing a Sequence of Robotic Tasks Inproceedings Proceedings of the International Conference on Intelligent Robots and Systems (IROS), IEEE, 2013. Abstract | Links | BibTeX | Schlagwörter: @inproceedings{IROS2013, title = {On Optimizing a Sequence of Robotic Tasks}, author = { Sergey Alatartsev and Vera Mersheeva and Marcus Augustine and Frank Ortmeier}, url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/05/Alatartsev_IROS2013.pdf}, year = {2013}, date = {2013-01-01}, booktitle = {Proceedings of the International Conference on Intelligent Robots and Systems (IROS)}, publisher = {IEEE}, abstract = {Production speed and energy efficiency are crucial factors for any application scenario in industrial robotics. The most important factor for this is planning of an optimized sequence of atomic subtasks. In a welding scenario, an atomic subtask could be understood as a single welding seam/spot while the sequence could be the ordering of these atomic tasks. Optimization of a task sequence is normally modeled as the Traveling Salesman Problem (TSP). This works well for simple scenarios with atomic tasks without execution freedom like spot welding. However, many types of tasks allow a certain freedom of execution. A simple example is seam welding of a closed-contour, where typically the starting-ending point is not specified by the application. This extra degree of freedom allows for much more efficient task sequencing. In this paper, we describe an extension of TSP to model a problem of finding an optimal sequence of tasks with such extra degree of freedom. We propose a new, efficient heuristic to solve such problems and show its applicability. Obtained computational results are close to the optimum on small instances and outperforms the state of the art approaches on benchmarks available in literature.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Production speed and energy efficiency are crucial factors for any application scenario in industrial robotics. The most important factor for this is planning of an optimized sequence of atomic subtasks. In a welding scenario, an atomic subtask could be understood as a single welding seam/spot while the sequence could be the ordering of these atomic tasks. Optimization of a task sequence is normally modeled as the Traveling Salesman Problem (TSP). This works well for simple scenarios with atomic tasks without execution freedom like spot welding. However, many types of tasks allow a certain freedom of execution. A simple example is seam welding of a closed-contour, where typically the starting-ending point is not specified by the application. This extra degree of freedom allows for much more efficient task sequencing. In this paper, we describe an extension of TSP to model a problem of finding an optimal sequence of tasks with such extra degree of freedom. We propose a new, efficient heuristic to solve such problems and show its applicability. Obtained computational results are close to the optimum on small instances and outperforms the state of the art approaches on benchmarks available in literature. |
Trojahn, Matthias; Ortmeier, Frank Biometric Keystroke Authentication on Smartphones Using a Capacitive Display Konferenz 2. Doktorandentagung Magdeburger-Informatik-Tage 2013 (MIT 2013), 2013. Links | BibTeX | Schlagwörter: @conference{Trojahn.2013k, title = {Biometric Keystroke Authentication on Smartphones Using a Capacitive Display}, author = { Matthias Trojahn and Frank Ortmeier}, url = {http://www2.cs.uni-magdeburg.de/inf_media/bilder/Forschung/MIT/2013/Tagungsband_MIT2013.pdf#page=29}, year = {2013}, date = {2013-01-01}, booktitle = {2. Doktorandentagung Magdeburger-Informatik-Tage 2013 (MIT 2013)}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
Trojahn, Matthias; Arndt, Florian; Ortmeier, Frank Authentication with Time Features of Keystroke Dynamics on Touchscreens Inproceedings 14th Conference on Communications and Multimedia Security (CMS), S. 197-199, 2013, ISBN: 978-3-642-40778-9. Abstract | Links | BibTeX | Schlagwörter: @inproceedings{Trojahn.2013j, title = {Authentication with Time Features of Keystroke Dynamics on Touchscreens}, author = { Matthias Trojahn and Florian Arndt and Frank Ortmeier}, url = {https://link.springer.com/chapter/10.1007/978-3-642-40779-6_17}, doi = {10.1007/978-3-642-40779-6}, isbn = {978-3-642-40778-9}, year = {2013}, date = {2013-01-01}, booktitle = {14th Conference on Communications and Multimedia Security (CMS)}, pages = {197-199}, abstract = {Keystroke authentication is a well known method to secure the mobile devices. Especially, the increasing amount of personal and sensitive data stored on these devices makes a secure authentication system necessary. Traditional security techniques like the four-digit PIN-input are insufficient and do not correspond to the present password standards. A keystroke behavior based authentication system could increase the security. Different researches have been published based on keystroke authentication systems with traditional PC keypads. But the keystroke behavior on touchscreens, as they are nowadays used on smartphones, are not analyzed before.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Keystroke authentication is a well known method to secure the mobile devices. Especially, the increasing amount of personal and sensitive data stored on these devices makes a secure authentication system necessary. Traditional security techniques like the four-digit PIN-input are insufficient and do not correspond to the present password standards. A keystroke behavior based authentication system could increase the security. Different researches have been published based on keystroke authentication systems with traditional PC keypads. But the keystroke behavior on touchscreens, as they are nowadays used on smartphones, are not analyzed before. |
Trojahn, Matthias; Schadewald, Christian; Ortmeier, Frank Keystroke Authentication with a Capacitive Display using Different Mobile Devices Konferenz 10th International Conference on Security and Cryptography (SECRYPT), 2013. Links | BibTeX | Schlagwörter: @conference{Trojahn.2013i, title = {Keystroke Authentication with a Capacitive Display using Different Mobile Devices}, author = { Matthias Trojahn and Christian Schadewald and Frank Ortmeier}, url = {http://ieeexplore.ieee.org/abstract/document/7223219/}, year = {2013}, date = {2013-01-01}, booktitle = {10th International Conference on Security and Cryptography (SECRYPT)}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
Trojahn, Matthias; Beck, Alexander; Ortmeier, Frank Biometrische Authentifizierung zur Fahrererkennung in Lkws Konferenz D-A-CH security 2013, 2013. BibTeX | Schlagwörter: @conference{Trojahn.2013h, title = {Biometrische Authentifizierung zur Fahrererkennung in Lkws}, author = { Matthias Trojahn and Alexander Beck and Frank Ortmeier}, year = {2013}, date = {2013-01-01}, booktitle = {D-A-CH security 2013}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
Trojahn, Matthias; Beck, Alexander; Ortmeier, Frank Biometrische Alternativen zum Habenfaktor bei Smartphones Konferenz D-A-CH security 2013, 2013. BibTeX | Schlagwörter: @conference{Trojahn.2013g, title = {Biometrische Alternativen zum Habenfaktor bei Smartphones}, author = { Matthias Trojahn and Alexander Beck and Frank Ortmeier}, year = {2013}, date = {2013-01-01}, booktitle = {D-A-CH security 2013}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
Trojahn, Matthias; Ortmeier, Frank Designing an Enterprise Security Strategy for Mobile Intranet Access Konferenz Seventh International Conference on Software Security and Reliability Companion (SERE 2013), 2013. Links | BibTeX | Schlagwörter: @conference{Trojahn.2013e, title = {Designing an Enterprise Security Strategy for Mobile Intranet Access}, author = { Matthias Trojahn and Frank Ortmeier}, url = {http://ieeexplore.ieee.org/abstract/document/6616319/}, year = {2013}, date = {2013-01-01}, booktitle = {Seventh International Conference on Software Security and Reliability Companion (SERE 2013)}, keywords = {}, pubstate = {published}, tppubtype = {conference} } |
Trojahn, Matthias; Arndt, Florian; Weinmann, Markus; Ortmeier, Frank Emotion Recognition Through Keystroke Dynamics on Touchscreen Keyboards Buchkapitel mit eigenem Titel 15th International Conference on Enterprise Information Systems, 2013. Abstract | Links | BibTeX | Schlagwörter: @incollection{Trojahn.2013f, title = {Emotion Recognition Through Keystroke Dynamics on Touchscreen Keyboards}, author = { Matthias Trojahn and Florian Arndt and Markus Weinmann and Frank Ortmeier}, url = {https://www.researchgate.net/publication/257603545_Emotion_Recognition_Through_Keystroke_Dynamics_on_Touchscreen_Keyboards}, year = {2013}, date = {2013-01-01}, booktitle = {15th International Conference on Enterprise Information Systems}, abstract = {Automatic emotion recognition through computers offers a lot of advantages, as the interaction between human and computers can be improved. For example, it is possible to be responsive to anger or frustration of customers automatically while working with a webpage. Mouse cursor movements and keystroke dynamics were already used and examined for such a recognition on conventional keyboards. The aim of this work is to investigate keystroke dynamics on touchscreen keyboards which gets a cumulative relevance through the increasingly further circulation of smartphones and tablets. Furthermore, it is possible to record additional information like pressure and size of keystrokes. This could increase the recognition rate for emotions. In order to record the keystroke dynamics, an application and keyboard layout for Android OS were developed. In addition, hypotheses were established on the basis of Yerkes-Dodson-Law and Flow theory and besides, a study with 152 test persons for the data collection was implemented. Subsequently, a data evaluation with the SPSS software was accomplished. Most of the hypotheses were confirmed and the results of the study show that emotions can be explained by the keystroke dynamics and recognized in this way. }, keywords = {}, pubstate = {published}, tppubtype = {incollection} } Automatic emotion recognition through computers offers a lot of advantages, as the interaction between human and computers can be improved. For example, it is possible to be responsive to anger or frustration of customers automatically while working with a webpage. Mouse cursor movements and keystroke dynamics were already used and examined for such a recognition on conventional keyboards. The aim of this work is to investigate keystroke dynamics on touchscreen keyboards which gets a cumulative relevance through the increasingly further circulation of smartphones and tablets. Furthermore, it is possible to record additional information like pressure and size of keystrokes. This could increase the recognition rate for emotions. In order to record the keystroke dynamics, an application and keyboard layout for Android OS were developed. In addition, hypotheses were established on the basis of Yerkes-Dodson-Law and Flow theory and besides, a study with 152 test persons for the data collection was implemented. Subsequently, a data evaluation with the SPSS software was accomplished. Most of the hypotheses were confirmed and the results of the study show that emotions can be explained by the keystroke dynamics and recognized in this way. |