Skill-based Engineering and Control on Field-Device-Level with OPC UA - Zimmermann, Patrick; Axmann, Etienne; Brandenbourger, Benjamin; Dorofeev, Kirill; Mankowski, André; Zanini, Paulo (Proceedings of the IEEE International Conference on Emerging Technologies And Factory Automation (ETFA), 2019)
The configuration of current automated production systems is complex and therefore time consuming while the market demands an easy setup and adaptability due to smaller batch sizes and volatile markets. While there are different concepts in research on how to simplify the engineering process by using generic skills or capabilities of devices, run-time control is still achieved with proprietary communication protocols and commands. The concept in this paper uses skills not only in the phase of engineering but also consequently for direct and generic control of field-devices. An executable skill-metamodel therefore describes the methodological functionality which is implemented by using OPC UA due to its vendor independence as well as built-in services and information model. The implementation uses client/server-based OPC UA and the pub/sub pattern to prepare for a deterministic real-time control in conjunction with TSN, which is required by industrial automation.
Keywords: industry 4.0

SMT-Based Deployment Calculation in Industrial Automation Domain - Terzimehić, Tarik; Wenger, Monika; Voss, Sebastian; Grüner, Sten; Elfham, Haitham (Proceedings of the IEEE International Conference on Emerging Technologies And Factory Automation (ETFA), 2019)
The desired flexibility of industrial automation systems foresees among others flexible deployment and execution of control applications on distributed control nodes. This task can be performed more efficiently by an automated deployment algorithm yielding a valid deployment and optimizing nonfunctional objectives. Although extensively investigated, automated deployment approaches for the automotive domain cannot be translated to industrial control applications, due to a different execution semantics. Thus, in this paper, we present a method of satisfiability modulo theories (SMT)-based automated deployment of the industrial automation systems. We formalize and implement domain-relevant constraints and objectives. Our contribution is threefold: 1) we formalize the functional coupling and end-to-end deadline constraints and objectives while considering the semantics of control applications, 2) we encode the deployment problem into an SMT form, and 3) we validate the approach on an abstract example and a domain-relevant use case. The results obtained in this paper will allow application engineers to fulfill functional and real-time requirements by automatically solving the deployment problem.
Keywords: BaSys 4.0; Model-based systems engineering; MbSE; deployment; Industry 4.0; IEC 61499; SMT; E2E latency; functional coupling; design-space exploration; DSE

Software Engineering for Smart Cyber-Physical Systems (SEsCPS 2018) - Workshop Report - Bures, Tomas; Weyns, Danny; Schmerl, Bradley; Fitzgerald, John; Aniculaesei, Adina; Berger, Christian; Cambeiro, Joao; Carlson, Jan; Chowdhury, Shafiul Azam; Daun, Marian; Li, Nianyu; Markthaler, Matthias; et al. (SIGSOFT Softw. Eng. Notes, 2019)
Smart Cyber-Physical Systems (sCPS) are a novel kind of Cyber- Physical System engineered to take advantage of large-scale cooperation between devices, users and environment to achieve added value in the face of uncertainty and changing environments. Examples of sCPS include modern traffic systems, Industry 4.0 systems, systems for smart buildings, and smart energy grids. The uniting aspect of all these systems is that to achieve their high level of intelligence, adaptivity and ability to optimize and learn, they rely heavily on software. This makes them software-intensive systems, where software becomes their most complex part. Engineering sCPS thus becomes a recognized software engineering discipline, which, due to specifics of sCPS, can only partially rely on the existing body of knowledge in software engineering. In fact, it turns out that many of the traditional approaches to architecture modeling and software development fall short in their ability to cope with the high dynamicity and uncertainty of sCPS. This calls for innovative approaches that jointly reflect and address the specifics of such systems. This paper maps the discussions and results of the Fourth International Workshop on Software Engineering for Smart Cyber-Physical Systems (SEsCPS 2018), which focuses on challenges and promising solutions in the area of software engineering for sCPS.
Keywords: cyber-physical systems; software engineering; Model-based Systems Engineering; MbSE

The Neurorobotics Platform for Teaching – Embodiment Experiments with Spiking Neural Networks and Virtual Robots - Vasquez Tieck, Juan Camilo; Kaiser, Jacques; Steffen, Lea; Schulze, Martin; von Arnim, Axel; Reichard, Daniel; Roennau, Arne; Dillmann, Rüdiger (2019 IEEE International Conference on Cyborg and Bionic Systems (CBS), 2019)
Understanding the brain is an interdisciplinary effort spanning over the fields of computational neuroscience, machine learning and robotics. The collaboration between researchers across these fields should be encouraged by comprehensive simulation platforms. The Neurorobotics Platform (NRP) developed by the Human Brain Project enables such collaboration by allowing researchers to define virtual experiments in which brain models are connected to simulated robots. In this paper, we present how we use the NRP as an education tool to introduce master students to neurorobotics. The students are given the task to define, implement and solve three virtual neurorobotics challenges related to perception, arm motion and locomotion. Without any previous knowledge on neurorobotics, the students completed this task within the course of one semester. We present the challenges, which are now open-source benchmarks available online, as well as example solutions from the students to these challenges. This paper gives a glimpse of what new users are capable of by using the NRP to simulate their neurorobotics experiment. Aside from educating the students, this initiative also allowed to collect their direct feedback on the NRP. This feedback is valuable for the Human Brain Project as a whole since it helps identify how new users interact with the platform.
Keywords: neurorobotics; neuromorphic; neuromorphic computing; HBP; NRP; virtual; robotics

A Biomimetic Control Method Increases the Adaptability of a Humanoid Robot Acting in a Dynamic Environment - Capolei, Marie-Claire; Angelidis, Emmanouil; Falotico, Egidio; Lund, Henrik Hautop; Tolu, Silvia (Frontiers in Neurorobotics, 2019)
Keywords: neuromorphic; neurorobotics; icub; robotics; nrp; hbp

BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings - Gavrilenko, Natalia; Ponce de León, Hernán; Furbach, Florian; Heljanko, Keijo; Meyer, Roland (Computer Aided Verification (CAV) 2019., 2019)
We present Dartagnan, a bounded model checker (BMC) for concurrent programs under weak memory models. Its distinguishing feature is that the memory model is not implemented inside the tool but taken as part of the input. Dartagnan reads CAT, the standard language for memory models, which allows to define x86/TSO, ARMv7, ARMv8, Power, C/C++, and Linux kernel concurrency primitives. BMC with memory models as inputs is challenging. One has to encode into SMT not only the program but also its semantics as defined by the memory model. What makes Dartagnan scale is its relation analysis, a novel static analysis that significantly reduces the size of the encoding. Dartagnan matches or even exceeds the performance of the model-specific verification tools Nidhugg and CBMC, as well as the performance of Herd, a CAT-compatible litmus testing tool. Compared to the unoptimized encoding, the speed-up is often more than two orders of magnitude.
Keywords: Weak memory models; CAT; Concurrency; BMC; SMT; Model-based Systems Engineering; MbSE

Adoption of Software Platforms: Reviewing Influencing Factors and Outlining Future Research - Engert, Martin; Pfaff, Matthias; Krcmar, Helmut (Twenty-Third Pacific Asia Conference on Information Systems: PACIS 2019. Xi'An, China., 2019)

Combined Data Transfer Response Time and Mapping Exploration in MPSoCs - Diewald, Alexander; Barner, Simon; Saidi, Selma (10th International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems (WATERS) co-located with ECRTS, 2019)
Recent embedded applications such as Autonomous Driver Assistance Systems (ADAS) require large computational resources that increase the need for HW accelerators, e.g., in system-on-chip-based platforms. Synthesising optimal task/data mappings and schedules for such platforms becomes increasingly challenging, even more in safety-critical contexts. For designing real-time heterogeneous systems, response time computation and the resolution of task mapping problems are required as demanded in the WATERS 2019 challenge. Our contribution to address the challenge is to extend a design space exploration (DSE) formulation of mapping applications on MPSoCs architectures to consider DMA-based data (pre)-fetching. The approach is performed in two steps. First, we determine task mappings to a heterogeneous MPSoC platform using a multi-objective evolutionary algorithm (MOEA)-based DSE. In order to check the feasibility of an allocation, and to rate its quality, we use a SMT solver to construct schedules whose latency is close to the achievable minimum. Our task response time analysis considers the effects of memory access times and DMAs to supply the SMT scheduler with data fetching latencies. The MOEA-DSE, the SMT scheduler, and the response time calculation are integrated into the AutoFOCUS 3 tool that has been extended with an importer for the AMALTHEA model that specifies the challenge use case.
Keywords: AutoFOCUS3; design-space exploration; DSE; deployment synthesis; mapping; model-based systems engineering; MbSE

Skill-basiertes Engineering auf Basis von OPC UA Companion Specifications - Mankowski, André; Axmann, Etienne; Brandenbourger, Benjamin; Dorofeev, Kirill; Zanini, Paulo; Zimmermann, Patrick (20. Leitkongress der Mess- und Automatisierungstechnik AUTOMATION 2019 – Autonomous Systems and 5G in Connected Industries, 2019)
Aktuelle Automatisierungssysteme benötigen eine komplexe und zeitaufwändige Konfiguration, während der Markt aufgrund kleinerer Losgrößen eine einfachere Einrichtung und Anpassungsfähigkeit verlangt. Während es unterschiedliche Konzepte gibt, wie man den Engineering-Prozess durch Fähigkeiten bzw. Skills in der Forschung vereinfachen kann, ist die Laufzeitkontrolle mit proprietären Kommunikationsprotokollen und Befehlen nach wie vor Stand der Technik. Dieser Beitrag schlägt ein Konzept vor, wie Fähigkeiten (Skills) nicht nur im Engineering, sondern auch für die Steuerung von Geräten auf Feldebene eingesetzt werden können. Ein ausführbares Skill-Modell beschreibt dabei die methodische Funktionalität, während OPC UA aufgrund seiner Herstellerunabhängigkeit und der integrierten Dienste z.B. für die Informationsmodellierung zur Implementierung verwendet wird. Das umgesetzte Konzept nutzt dabei OPC UA zur skill-basierten Steuerung eines exemplarischen Fertigungsprozesses zur Produktion von Fidget Spinnern und wird anhand eines Demonstrators veranschaulicht.

Towards Machine Learning for Learnability of MDD Tools - bin Abid, Saad; Mahajan, Vishal; Lúcio, Levi (Software Engineering and Knowledge Engineering (SEKE) Conference, Lisbon, Portugal, 2019)
Learning how to build software systems using new tools can be a daunting task to anyone new to the job. This is especially true of tools that provide a large number of functionalities and views on the system under development, such as IDES for Model-Driven Development (MDD). Applying Machine Learning (ML) techniques can help in this state of affairs by pointing out to appropriate next actions to rookie or even intermediate developers. AutoFOCUS3 (AF3) is a mature MDD tool we are building in-house and for which we provide regular tutorials to new users. These users come from both the academia (e.g, students/professors) and the industry (e.g. managers/software engineers). Nonetheless, AF3 remains a complex tool and we have found there is a need to speedup the learning curve of the tool for students that attend our tutorials-or alternatively and more importantly for others that simply download the tool and attempt using it without human supervision. In this paper, we describe a machine learning-based recommendation system named MAGNET for aiding beginner and intermediate users of AF3 in learning the tool. We describe how we have gathered data and trained an ML model to suggest new commands, how a recommender system was integrated in the AF3, experiments we have run thus far, and the future directions of our work.
Keywords: Model-Driven Development; MDD; AutoFOCUS3; Machine Learning; Intelligent Recommendation Systems; IRS; Eclipse IDE; Domain-Specific Languages; DSLs; development interaction data; methodology; tooling; model-based systems engineering; MbSE

Addressing Inherent Uncertainty: Risk-Sensitive Behavior Generation for Automated Driving using Distributional Reinforcement Learning - Bernhard, Julian; Pollok, Stefan; Knoll, Alois (2019 IEEE Intelligent Vehicles Symposium (IV), 2019)

Bridging the Gap between Open Source Software and Vehicle Hardware for Autonomous Driving - Kessler, Tobias; Bernhard, Julian; Buechel, Martin; Esterle, Klemens; Hart, Patrick; Malovetz, Daniel; Truong Le, Michael; Diehl, Frederik; Brunner, Thomas; Knoll, Alois (2019 IEEE Intelligent Vehicles Symposium, 2019)

From Specifications to Behavior: Maneuver Verification in a Semantic State Space - Esterle, Klemens; Aravantinos, Vincent; Knoll, Alois (2019 IEEE Intelligent Vehicles Symposium, 2019)

Leveraging Semantic Embeddings for Safety-Critical Applications - Brunner, Thomas; Diehl, Frederik; Truong Le, Michael; Knoll, Alois (The IEEE Conference on Computer Vision and Pattern Recognition (CVPR) Workshops, 2019)
Semantic Embeddings are a popular way to represent knowledge in the field of zero-shot learning. We observe their interpretability and discuss their potential utility in a safety-critical context. Concretely, we propose to use them to add introspection and error detection capabilities to neural network classifiers. First, we show how to create embeddings from symbolic domain knowledge. We discuss how to use them for interpreting mispredictions and propose a simple error detection scheme. We then introduce the concept of semantic distance: a real-valued score that measures confidence in the semantic space. We evaluate this score on a traffic sign classifier and find that it achieves near state-of-the-art performance, while being significantly faster to compute than other confidence scores. Our approach requires no changes to the original network and is thus applicable to any task for which domain knowledge is available.

Model-based methodology for space vehicles - Zverlov, Sergey; Voss, Sebastian; Böhm, Thomas; Herpel, Hans-Jürgen; Kerep, Mladen (Proceedings of the Eurospace Annual Conference on Data Systems in Aerospace (DASIA), 2019)
The technological challenges that companies in the space domain are facing today are becoming more and more complex. On the one hand complexity of the tasks that need to be performed by the new generation of spacecrafts is increasing. On the other hand, the development needs to be cost and time efficient to be able to compete against new players in this domain, such as SpaceX. To deal with these challenges new development tools and methods are needed. In scope of this work we propose a model-based approach for future spacecrafts. We integrated this approach into a state-of-the-art model-based tool and applied it onto an industrial case-study to show proof-of-concept.
Keywords: AutoFOCUS3; case study; model-based systems engineering; MbSE

Providentia - A Large Scale Sensing System for the Assistance of Autonomous Vehicles - Krämmer, Annkathrin; Schöller, Christoph; Gulati, Dhiraj; Knoll, Alois (Robotics Science and Systems Workshops (RSS Workshops), 2019)
The environmental perception of autonomous vehicles is not only limited by physical sensor ranges and algorithmic performance, but also occlusions degrade their understanding of the current traffic situation. This poses a great threat for safety, limits their driving speed and can lead to inconvenient maneuvers that decrease their acceptance. Intelligent Transportation Systems can help to alleviate these problems. By providing autonomous vehicles with additional detailed information about the current traffic in form of a digital model of their world, i.e. a digital twin, an Intelligent Transportation System can fill in the gaps in the vehicle's perception and enhance its field of view. However, detailed descriptions of implementations of such a system and working prototypes demonstrating its feasibility are scarce. In this work, we propose a hardware and software architecture to build such a reliable Intelligent Transportation System. We have implemented this system in the real world and show that it is able to create an accurate digital twin of an extended highway stretch. Furthermore, we provide this digital twin to an autonomous vehicle and demonstrate how it extends the vehicle's perception beyond the limits of its on-board sensors.
Keywords: Intelligent Transportation Systems; Autonomous Driving; Robotics

Running Large-Scale Simulations on the Neurorobotics Platform to Understand Vision – The Case of Visual Crowding - Bornet, Alban; Kaiser, Jacques; Kroner, Alexander; Falotico, Egidio; Ambrosano, Alessandro; Cantero, Kepa; Herzog, Michael; Francis, Gregory (Frontiers in Neurorobotics, 2019)
Traditionally, human vision research has focused on specific paradigms and proposed models to explain very specific properties of visual perception. However, the complexity and scope of modern psychophysical paradigms undermine the success of this approach. For example, perception of an element strongly deteriorates when neighboring elements are presented in addition (visual crowding). As it was shown recently, the magnitude of deterioration depends not only on the directly neighboring elements but on almost all elements and their specific configuration. Hence, to fully explain human visual perception, one needs to take large parts of the visual field into account and combine all the aspects of vision that become relevant at such scale. These efforts require sophisticated and collaborative modeling. The Neurorobotics Platform (NRP) of the Human Brain Project offers a unique opportunity to connect models of all sorts of visual functions, even those developed by different research groups, into a coherently functioning system. Here, we describe how we used the NRP to connect and simulate a segmentation model, a retina model, and a saliency model to explain complex results about visual perception. The combination of models highlights the versatility of the NRP and provides novel explanations for inward-outward anisotropy in visual crowding.
Keywords: robotics; human brain project; HBP; neurorobotics; neuromorphics; brain simulation; spiking neural networks; NRP; robot simulation

SMErobotics: Smart Robots for Flexible Manufacturing - Perzylo, Alexander; Rickert, Markus; Kahl, Björn; Somani, Nikhil; Lehmann, Christian; Kuss, Alexander; Profanter, Stefan; Billeso Beck, Anders; Haage, Mathias; Rath Hansen, Mikkel; Tofveson Nibe, Malene; Roa, Máximo A.; et al. (IEEE Robotics & Automation Magazine, 2019)
Current market demands require an increasingly agile production environment throughout many manufacturing branches. Traditional automation systems and industrial robots, on the other hand, are often too inflexible to provide an economically viable business case for companies with rapidly changing products. The introduction of cognitive abilities into robotic and automation systems is, therefore, a necessary step toward lean changeover and seamless human–robot collaboration. In this article, we introduce the European Union (EU)-funded research project SMErobotics, which focuses on facilitating the use of robot systems in small and medium-sized enterprises (SMEs). We analyze open challenges for this target audience and develop multiple efficient technologies to address related issues. Real-world demonstrators of several end users and from multiple application domains show the impact these smart robots can have on SMEs. This article intends to give a broad overview of the research conducted in SMErobotics. Specific details of individual topics are provided through references to our previous publications.
Keywords: robotics; smerobotics

Bedarfsanalyse, Machbarkeitsevaluation und IT-Architekturentwurf von Distributed Ledger Technology in der öffentlichen Verwaltung - Balta, Dian; Krcmar, Helmut; Kuhn, Peter (Fachtagungen Verwaltungsinformatik und Rechtsinformatik, 2019)

Body Randomization Reduces the Sim-to-Real Gap for Compliant Quadruped Locomotion - Vandersompele, Alexander; Urbain, Gabriel; Mahmud, Hossain; Wyffels, Francis; Dambre, Joni (Frontiers in Neurorobotics, 2019)
Designing controllers for compliant, underactuated robots is challenging and usually requires a learning procedure. Learning robotic control in simulated environments can speed up the process whilst lowering risk of physical damage. Since perfect simulations are unfeasible, several techniques are used to improve transfer to the real world. Here, we investigate the impact of randomizing body parameters during learning of CPG controllers in simulation. The controllers are evaluated on our physical quadruped robot. We find that body randomization in simulation increases chances of finding gaits that function well on the real robot.
Keywords: robotics; human brain project; HBP; neurorobotics; neuromorphics; brain simulation; spiking neural networks; NRP; robot simulation

Künstliche Intelligenz Out-of-the-Box – aber was steckt in der Box? - Balta, Dian; Krcmar, Helmut; Kuhn, Peter (Fachtagungen Verwaltungsinformatik und Rechtsinformatik, 2019)

Runtime Monitoring Neuron Activation Patterns - Cheng, Chih-Hong; Nührenberg, Georg; Yasuoka, Hirotoshi (Design, Automation & Test in Europe Conference & Exhibition, 2019)

The Collaborative Virtual Reality Neurorobotics Lab - Weissker, Tim; Angelidis, Emmanouil; Kulik, Alexander; Beck, Stephan; Kunert, Andre; Frolov, Anton; Weber, Sandro; Kreskowski, Adrian; Froehlich, Bernd (Proceedings of the IEEE Conference on Virtual Reality and 3D User Interfaces (VR), 2019)
We present the collaborative Virtual Reality Neurorobotics Lab, which allows multiple collocated and remote users to experience, discuss and participate in neurorobotic experiments in immersive virtual reality. We describe the coupling of the Neurorobotics Platform of the Human Brain Project with our collaborative virtual reality and 3D telepresence infrastructure and highlight future opportunities arising from our work for research on direct human interaction withsimulated robots and brains.
Keywords: robotics; human brain project; HBP; neurorobotics; neuromorphics; brain simulation; spiking neural networks; NRP; robot simulation

Wissensbasierte digitale Unterstützung in der Pflanzenbauberatung - Nafissi, Anahita; Weckesser, Fabian; Kessler, Ingmar; Rickert, Markus; Pfaff, Matthias; Peisl, Sebastian; Beck, Michael (Referate der 39. GIL-Jahrestagung in Wien: Informatik in der Land-, Forst- und Ernährungswirtschaft Fokus: Digitalisierung für landwirtschaftliche Betriebe in kleinstrukturierten Regionen – ein Widerspruch in sich?, 2019)
Obwohl die Landwirtschaft schon immer technologische Neuerungen in der Produktion einsetzt, ist gerade die landwirtschaftliche Beratung bisher noch verhältnismäßig wenig digitalisiert. Oft ist es gängige Praxis für Landwirte und Berater, gesetzliche Regelungen, Fachliteratur und Betriebsdaten in Papierform nachzuschlagen und in unstrukturierten, digitalen Dokumenten einzutragen. Zur Unterstützung der Landwirte und der Pflanzenbauberatung wird ein Entscheidungshilfesystem entwickelt, welches die Beratung in der Landwirtschaft digital unterstützen und erleichtern soll, indem es aktuelles Fach- und Expertenwissen sowie individuelle Betriebsdaten abruft, aufbereitet und zweckgebunden auswertet. Dafür ist es notwendig, das entsprechende Fachwissen aus vielfältigen heterogenen Datenquellen in einer einheitlichen Wissensbasis verfügbar zu machen. Der hier beschriebene Ansatz verwendet Semantic-Web-Technologien wie OWL-Ontologien und SPARQL-Abfragen, um diese Daten hinsichtlich ihrer Bedeutung, d.h. semantisch, zu modellieren und abzufragen.
Keywords: farmexpert; robotics

Digitalgestützte Bürgerbeteiligung & KI - Balta, Dian; Krcmar, Helmut; Kuhn, Peter; Kulus, Daniel; Sellami, Mahdi (PLANERIN, 2019)
Digitalisierung und künstliche Intelligenz (KI) gelten als prägende Themen und wecken eine hohe Aufmerksamkeit in Gesellschaft, Wirtschaft, Politik und Verwaltung. Im Bereich Bürgerbeteiligung bergen Digitalisierung und in letzter Zeit auch KI eine Reihe von Chancen und Herausforderungen. Für die Beteiligungspraxis stellen sich daher u. a. folgende Fragen: Welche Aufgaben kann KI in Beteiligungsverfahren übernehmen? Wie gut sind solche Systeme heute schon und welche Qualitäten haben die erzielten Ergebnisse? Welche Fortschritte sind zu erwarten? Der Artikel gibt erste Antworten basierend auf Untersuchungen und dem Einsatz von Prototypen im Rahmen von Bürgerbeteiligungsverfahren in Hamburg und schließt mit einem Ausblick in die Zukunft.

OPC UA versus ROS, DDS, and MQTT: Performance Evaluation of Industry 4.0 Protocols - Profanter, Stefan; Tekat, Ayhun; Dorofeev, Kirill; Rickert, Markus; Knoll, Alois (Proceedings of the IEEE International Conference on Industrial Technology (ICIT), 2019)
Ethernet-based protocols are getting more and more important for Industry 4.0 and the Internet of Things. In this paper, we compare the features, package overhead, and performance of some of the most important protocols in this area. First, we present a general feature comparison of OPC UA, ROS, DDS, and MQTT, followed by a more detailed wire protocol evaluation, which gives an overview over the protocol overhead for establishing a connection and sending data. In the performance tests we evaluate open-source implementations of these protocols by measuring the round trip time of messages in different system states: idle, high CPU load, and high network load. The performance analysis concludes with a test measuring the round trip time for 500 nodes on the same host.
Keywords: robotics; smecobot

Structure and behavior preserving statecharts refinements - Syriani, Eugene; Sousa, Vasco; Lúcio, Levi (Science of Computer Programming, 2019)
Statecharts are one of the most popular modeling formalisms that is used in a diversity of real world applications, such as cyber-physical systems, mobile computing, and bio-informatics. Following common step-wise refinement strategies, modelers often develop and evolve Statecharts models incrementally to satisfy requirements and changes. Although there are already several existing Statecharts refinement approaches, they provide insufficient guarantees to support reasoning about the preservation of both its internal structure, to enhance development and maintenance, and its behavior, which external components using the Statecharts model may depend on. In this paper, we formulate formal requirements to minimally limit the allowable Statecharts refinement operations such that certain assumptions on the structure and reachability of the Statecharts model will hold. To satisfy these requirements, we propose a set of practical bounding refinement rules that allows the modeler to achieve such refinements for which notions of behavior and structure preservation can be statically verified under some assumptions. Our implementation shows how these rules can be applied in realistic scenarios.
Keywords: Statechart; Refinement; Software design; Verification; Model-based Systems Engineering; MbSE

A general proof certification framework for modal logic - Libal, Tomer; Volpe, Marco (Mathematical Structures in Computer Science, 2019)
One of the main issues in proof certification is that different theorem provers, even when designed for the same logic, tend to use different proof formalisms and produce outputs in different formats. The project ProofCert promotes the usage of a common specification language and of a small and trusted kernel in order to check proofs coming from different sources and for different logics. By relying on that idea and by using a classical focused sequent calculus as a kernel, we propose here a general framework for checking modal proofs. We present the implementation of the framework in a Prolog-like language and show how it is possible to specialize it in a simple and modular way in order to cover different proof formalisms, such as labelled systems, tableaux, sequent calculi and nested sequent calculi. We illustrate the method for the logic K by providing several examples and discuss how to further extend the approach.
Keywords: Model-based Systems Engineering; MbSE

A Hybrid Approach of Solar Power Forecasting Using Machine Learning - Bajpai, Arpit; Duchon, Markus (2019 3rd International Conference on Smart Grid and Smart Cities (ICSGSC), 2019)
Photovoltaic (PV) power generation is prone to fluctuations and it is affected by different weather conditions. Therefore, accurate forecasting becomes vital for grid operators to manage grid operations. In this study, multiple machine learning models are used, and different weather parameters are analyzed for PV forecasting. The performance of different models is compared. The proposed forecasting models are tested with 4 kWp PV device installed at our institute, fortiss GmbH and the comparison of the models is done through error analysis. The accuracy is evaluated using historical weather data. The study proposes a novel approach of PV forecasting where a model is built based on the principle of pipelining clustering, classification and regression algorithms. Clustering and classification algorithms group the data-points with similar weather conditions. Subsequently, segmented regression is applied to these groups. Weather forecast of the next day is utilized to determine the models used for forecasting. The results show that the proposed forecasting model for PV systems is effective and promising.

A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols - Alturki, Musab A.; Ban Kirigin, Tajana; Kanovich, Max; Nigam, Vivek; Scedrov, Andre; Talcott, Carolyn (Foundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows, 2019)

A Perspective On Digital Wellbeing - Schmidmaier, Matthias (the he ACM Conference on Human Factors in Computing System, Workshop on Designing for Digital Wellbeing, 2019)
Technology is all around us, supporting and distracting us at the same time. In this work we present our perspective on the definition of digital wellbeing and how to achieve it. For digital wellbeing approaches, we define two categories creative and corrective and discuss relevant, exemplary user resources like time, trust or social skills. Finally we give a short outlook on the challenging future - is marrying a virtual popstar a form of digital wellbeing?

An OPC UA based Energy Management Platform for Multi-Energy Prosumers in Districts - Bytschkow, Denis; Capone, Alexandre; Mayer, Jan; Kramer, Michael; Licklederer, Thomas (IEEE PES, 2019)
Control and optimization in smart energy systems rely heavily on mathematical models of power system engineers. Simultaneously, software engineers that create control and monitoring systems are faced with questions for designing appropriate system interfaces, such that different kinds of interaction schemes are supported. Often, the data specifications required by the interfaces are implicitly available within the mathematical models. Moreover, control and optimization schemes sometimes require data to be transferred to be able to operate. Despite these synergies, these tasks are generally treated separately. In this work, we aim to reduce the gap between those activities to facilitate the development of interactive and collaborative systems. We model a system consisting of multiple buildings and multiple energy networks to optimize their operation. We work with the model in a follow up step to create an industrially applicable interface that relies on the OPC UA communication protocol, which is widely used in industry and is easily integrated in modern SCADA systems. We finally demonstrate the application of the proposed approach using a co-simulation.

Benefits and Challenges of Smart Highways for the User - Wiegand, Gesa (IUI Workshops, 2019)

BLE Injection-Free Attack: A Novel Attack On Bluetooth LowEnergy Devices - Cassimiro T. dos Santos, Aellison; Filho, José L. Soares; Silva, 1Avilla 1I. S.; Nigam, Vivek; Fonseca, Iguatemi (Journal of Ambient Intelligence and Humanized Computing, 2019)

Cooperative Multi-Vehicle Behavior Coordination for Autonomous Driving - Kessler, Tobias; Knoll, Alois (IEEE Intelligent Vehicles Symposium (IV), 2019)

Design and Runtime Verification Side-by-Side in eTrice - Kanav, Sudeep; Lúcio, Levi; Hilden, Christian; Schuetz, Thomas (Proceedings of the NASA Formal Methods Symposium, 2019)
eTrice is a mature open-source model-based software engineering tool, based on the ROOM methodology. It is currently used in the industry for the development of solutions for domains such as health, heavy machinery and the automotive. eTrice natively incorporates mechanisms for runtime verification. At the request of the developers of eTrice, we have incorporated model checking in their tool chain, by partly reusing the existing runtime verification architecture. We report on the implementation of the tool, experiments that we conducted, and lessons learned regarding the synergies between the two verification techniques.
Keywords: Model-based Systems Engineering; MbSE

Effective Management of Standardizing in E-Government - Balta, Dian (Corporate Standardization Management and Innovation, 2019)

ExplicitCase: Tool-support for Creating and Maintaining Assurance Arguments Integrated with System Models - Nigam, Vivek; Tsalidis, Alexandros; Voss, Sebastian; Cârlan, Carmen (2019 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), 2019)
Assurance cases are collections of standard-mandated documents that entail the specification of system's objectives and a collection of processes, development or verification evidence regarding the satisfaction of the respective objectives. A considerable amount of work has been done in the direction of modelling assurance cases, to support communication and reasoning regarding the system's safety. In this work, we present a set of features of ExplicitCase - a tool for modeling assurance cases. While there is a plethora of tools for creating and managing model-based assurance cases, the uniqueness of our tool is that it integrates assurance case models with system models created in AutoFOCUS3 (AF3) - an open-source model-based development tool for embedded software systems. While trying to keep up with state-of-the-art assurance case editors, the newly implemented features support assurance case creation using typed patterns, change impact analysis for assurance cases, assessment of the confidence in the created assurance arguments, export of the argumentation diagrams generated in ExplicitCase and integration of assurance case models with system models created in AutoFOCUS3. In particular, based on the integration with AF3 system models, we propose automatic support for detecting the impact of a change within system models on the assurance case model, thus enabling the integrated development of system and assurance case models.
Keywords: AutoFOCUS3; model-based safety cases; ExplicitCase; Model-based systems engineering; MbSE

Formal Security Verification of Industry 4.0 Applications - Nigam, Vivek; Talcott, Carolyn (24th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2019, Zaragoza, Spain, September 10-13, 2019, 2019)

I Drive - You Trust: Explaining Driving Behavior Of Autonomous Cars - Wiegand, Gesa; Schmidmaier, Matthias; Weber, Thomas; Hußmann, Heinrich (Extended Abstracts of the 2019 CHI Conference on Human Factors in Computing Systems, 2019)
Keywords: autonomous driving; explainability; mental model; situation awareness

ICT gateway to simulation environment for electrical fault injection and recovery - Gupta, Pragya Kirti; Savolainen, Pekka; Duchon, Markus (2019 IEEE International Conference on Communications, Control, and Computing Technologies for Smart Grids, 2019)

InCarAR: A Design Space Towards 3D Augmented Reality Applications in Vehicles - Wiegand, Gesa; Mai, Christian; Holländer, Kai; Hußmann, Heinrich (Proceedings of the 11th International Conference on Automotive User Interfaces and Interactive Vehicular Applications, 2019)

Interactive Image Restoration - Han, Zhiwei; Weber, Thomas; Matthes, Stefan; Liu, Yuanting; Shen, Hao (the Neural Information Processing Systems 2019, Human-centric Machine Learning Workshop, 2019)
Machine learning and many of its applications are considered hard to approach due to their complexity and lack of transparency. One mission of human-centric machine learning is to improve algorithm transparency and user satisfaction while ensuring an acceptable task accuracy. In this work, we present an interactive image restoration framework, which exploits both image prior and human painting knowledge in an iterative manner such that they can boost on each other. Additionally, in this system users can repeatedly get feedback of their interactions from the restoration progress. This informs the users about their impact on the restoration results, which leads to better sense of control, which can lead to greater trust and approachability. The positive results of both objective and subjective evaluation indicate that, our interactive approach positively contributes to the approachability of restoration algorithms in terms of algorithm performance and user experience.

Logical and Semantic Frameworks with Applications - Nigam, Vivek; Thiemann, René (Theor. Comput. Sci., 2019)

On Computer-Aided Techniques for Supporting Safety and Security Co-Engineering - Kondeva, Antoaneta; Cârlan, Carmen; Rueß, Harald; Nigam, Vivek (Proceedings of the 2019 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), 2019)
With the increasing system interconnectivity, cyberattacks on safety-critical systems can lead to catastrophic events. This calls for a better safety and security integration. Indeed, a safety assessment contains security relevant information, such as, key safety hazards, that shall not be triggered by cyber-attacks. Guidelines, such as, SAE J3061 and ED202A, already recommend to exchange information gathered by safety and security engineers during different phases of development. However, these guidelines do not specify exactly how and which information shall be exchanged. We propose a methodology for enabling computer aided techniques for extracting security relevant information from safety analysis. In particular, we propose techniques for automatically constructing Attack Trees from safety artefacts such as fault trees, hazard analysis and safety patterns. Lastly, we illustrate these techniques on an Industry 4.0 application.
Keywords: Model-based systems engineering; MbSE

On Integrating Design Thinking for a Human-centered Requirements Engineering - Hehn, Jennifer; Mendez, Daniel; Uebernickel, Falk; Brenner, Walter; Broy, Manfred (IEEE Software, 2019)

PerTract: Model Extraction and Specification of Big Data Systems for Performance Prediction by the Example of Apache Spark and Hadoop - Kroß, Johannes; Krcmar, Helmut (Big Data and Cognitive Computing, 2019)
Evaluating and predicting the performance of big data applications are required to efficiently size capacities and manage operations. Gaining profound insights into the system architecture, dependencies of components, resource demands, and configurations cause difficulties to engineers. To address these challenges, this paper presents an approach to automatically extract and transform system specifications to predict the performance of applications. It consists of three components. First, a system-and tool-agnostic domain-specific language (DSL) allows the modeling of performance-relevant factors of big data applications, computing resources, and data workload. Second, DSL instances are automatically extracted from monitored measurements of Apache Spark and Apache Hadoop (i.e., YARN and HDFS) systems. Third, these instances are transformed to model- and simulation-based performance evaluation tools to allow predictions. By adapting DSL instances, our approach enables engineers to predict the performance of applications for different scenarios such as changing data input and resources. We evaluate our approach by predicting the performance of linear regression and random forest applications of the HiBench benchmark suite. Simulation results of adjusted DSL instances compared to measurement results show accurate predictions errors below 15% based upon averages for response times and resource utilization.

Real-Time Personalization in Adaptive IDEs - Schmidmaier, Matthias; Han, Zhiwei; Weber, Thomas; Liu, Yuanting; Hußmann, Heinrich (the 27th Conference on User Modeling, Adaptation and Personalization (UMAP), 2019)
Integrated Development Environments (IDEs) are used for a varietyof software development tasks. Their complexity makes them chal-lenging to use though, especially for less experienced developers. In this paper, we outline our approach for an user-adaptive IDE that is able to track the interactions, recognize the user's intent and expertise, and provide relevant, personalized recommendations in real-time. To obtain a user model and provide recommendations, interaction data is processed in a two-stage process: first, we derive a bandit based global model of general task patterns from a dataset of labeled interactions. Second, when the user is working with the IDE, we apply a pre-trained classifier in real-time to get task labels from the user's interactions. With those and user feedback we fine-tune a local copy of the global model. As a result, we obtain a personalized user model which provides user-specific recommendations. We finally present various approaches for using these recommendations to adapt the IDE's interface. Modifications range from visual highlighting to task automation, including explanatory feedback.
Keywords: Adaptive IDE; User Modeling; Personalized Recommendation Systems; Human-Centered Machine Learning

Resource-Bounded Intruders in Denial of Service Attacks - Aires Urquiza, Abraão; Alturki, Musab A.; Ban Kirigin, Tajana; Nigam, Vivek; Scedrov, Andre (32nd IEEE Computer Security Foundations Symposium, CSF 2019, Hoboken, NJ, USA, June 25-28, 2019, 2019)

Roadmap to Skill Based Systems Engineering - Evers, Kathrin; Seyler, Jan R; Aravantinos, Vincent; Lúcio, Levi; Mehdi, Anees (24th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), 2019)
Finding the right solution for a given automation problem is one of the biggest challenges for customers of industrial control and automation companies. This search needs to address customers’ demands and preferences such as cost-effectiveness, energy-consumption, durability, working space, etc. Consequently, solutions may comprise different products of different providers. This leads to an enormous search space of diverse potential solutions. As of today, the search process involves human effort. Thus, a good understanding of system engineering is required not only on the manufacturer side but on the customer side as well. Furthermore, integration and configuration of the products into a functional system needs extra effort.In this paper, we present our first ideas on reducing the complexity of this search task. Our approach is laid out in three layers: (i) a customer only needs to describe their desired automation application on an abstract level. (ii) manufacturers need to categorize their products as per functionality and characteristics. (iii) the linking between the requirements as per customer’s description to relevant products is done automatically.This paper provides a roadmap for the research necessary to implement these three layers in practice. We lay out the essential research questions and provide a conceptual division of the work, thus pointing out the challenges that need to be solved to allow for further automation in this area.
Keywords: Model-based Systems Engineering; MbSE

Sector Coupling with Optimization: A comparison between single buildings and combined quarters - Heidemann, Lena; Bytschkow, Denis; Capone, Alexandre; Licklederer, Thomas; Kramer, Michael (The 8th DACH+ Conference on Energy Informatics, 2019)
The combination of building technologies with renewable energies, storagesystems and low carbon technologies, like Combined Heat and Power (CHP) andheat pumps, demands to consider different energy networks, i.e. sector coupling,in their building energy management systems (BEMS). This and the observationthat energy equipment in buildings is often oversized and seldom used to its fullpotential during the most time of the year calls for a holistic approach toestablish sustainable multi-energy neighbourhoods. In this work, we introduce amodel for a district energy system with sector coupling that integrates BEMS andcompare the results of this model for the optimized operation of single buildingsand the integrated solution to quantify the possible saving potential.

Sharing Economy: Potential im öffentlichen Sektor - Balta, Dian; Hofmann, Sara; Kuhn, Peter; Krcmar, Helmut (BERICHTE DES NEGZ, 2019)

Subexponentials in non-commutative linear logic - Kanovich, Max; Kuznetsov, Stepan; Nigam, Vivek; Scedrov, Andre (Mathematical Structures in Computer Science, 2019)

Symbolic Timed Trace Equivalence - Nigam, Vivek; Talcott, Carolyn; Aires Urquiza, Abraão (Foundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows, 2019)

Towards Automatically Identifying Potential Sustainability Effects of Requirements - Groher, Iris; Seyff, Norbert; Iqbal, Tahira (8th International Workshop on Requirements Engineering for Sustainable Systems (RE4SuSy), 2019)
Software developers are gradually becoming aware that their systems have effects on sustainability. The identification of potential effects software-intensive systems can have on different sustainability dimensions over time is yet in its infancy. Researchers are currently exploring approaches which strongly make use of expert knowledge to identify potential effects. In this work in progress paper, we are looking at the problem from a different angle: we report on the exploration of a machine learning-based approach to identify potential effects. Such an approach allows to save time and costs but increases the risk that potential effects are overseen. First results of applying the machine learning-based approach in the domain of home automation systems are promising, but also indicate that further research is needed before our approach can be applied in practice. Furthermore, we have learned that even providing the ground truth for training the algorithms is a challenging task.

Towards Computer-Aided Software Requirements Process - Reich, Marina; Chuprina, Tatiana; Nigam, Vivek (Proceedings of the Workshops of the Software Engineering Conference 2019, Stuttgart, Germany, February 19, 2019., 2019)

TSNsched: Automated Schedule Generation for Time Sensitive Networking - Schneider, Ben; Nigam, Vivek (2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22-25, 2019, 2019)

Usability of Development Tools: A CASE-Study - Weber, Thomas; Zoitl, Alois; Hußmann, Heinrich (the 22nd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion, 2019)
To facilitate model-driven development in practice, we need tools that support and empower developers. Many of the tools for it, however, are somewhat lacking with respect to usability, which can act as a major obstacle in adopting a model-driven approach and impede productivity. Efforts to find concrete usability flaws in model-driven tools are still relatively rare, and in the human computer interaction community, usability for highly specialized expert software is also not a prominent topic. In this work we conduct an evaluation using a number of usability evaluations methods on the 4diac IDE as an example of a model-driven engineering tool to see what works and where the problems are. With those different methods we found a considerable number of usability issues of varying severity as well as some indication which methods work in what context. These findings of course help improving the 4diac IDE specifically but also offer more general insights that may benefit other tools in improving their user experience. Overall our evaluation shows that there is a definite need for better usability and more evaluation of it.

Verification of Ada Programs with AdaHorn - Beyene, Tewodros; Herrera, Christian; Nigam, Vivek (Ada User Journal, 2019)
We propose AdaHorn , a model checker for verification of Ada programs with respect to correctness properties given as assertions. AdaHorn translates an Ada program together with its assertion into a set of Constrained Horn Clauses, and feeds it to a Horn constraints solver. We evaluate the performance of AdaHorn on a set of Ada programs inspired by C programs from the software verification competition (SV-COMP). Our experimental results show that AdaHorn outputs correct results in more cases than GNATProve, which is a widely used Ada verification framework.

Verification of Ada Programs with AdaHorn - Nigam, Vivek (Ada User Journal, 2019)

A Bird's Eye View on Requirements Engineering and Machine Learning - Iqbal, Tahira; Elahidoost, Parisa; Lúcio, Levi (Proceedings of the 25th Asia-Pacific Software Engineering Conference (APSEC), 2018)
Machine learning (ML) has demonstrated practical impact in a variety of application domains. Software engineering is a fertile domain where ML is helping in automating different tasks. In this paper, our focus is the intersection of software requirement engineering (RE) and ML. To obtain an overview of how ML is helping RE and the research trends in this area, we have surveyed a large number of research articles. We found that the impact of ML can be observed in requirement elicitation, analysis and specification, validation and management. Furthermore, in these categories, we discuss the specific problem solved by ML, the features and ML algorithms used as well as datasets, when available. We outline lessons learned and envision possible future directions for the domain.
Keywords: Requirements Engineering; Machine learning; State of the art; Overview; Model-based Systems Engineering; MbSE

Experience-Based Heuristic Search: Robust Motion Planning with Deep Q-Learning - Bernhard, Julian; Gieselmann, Robert; Esterle, Klemens; Knoll, Alois (21st International Conference on Intelligent Transportation Systems (ITSC), 2018)

Intelligent Hardware-Software Platform for Efficient Coupling of Water-Energy Nexus in Smart Cities: A Conceptual Framework - Pindoriya, Naran; Duchon, Markus; Gupta, Pragya Kirti; Pampana, Venkatesh; Singh, SN; Giza, Jakob; Hackenberg, Bastian; Rajput, Arvind; Jethi, Janki (EAI International Conference on Smart Cities, 2018)
Smart cities are envisioned to efficiently use two most critical resources: water and energy. Advanced techniques are being developed to conserve water and to minimize the use of conventional energy. The integration of battery energy storage (BES) technology and renewable energy (RE) sources in the system is very much required to enable the efficient coupling and modularization of electricity and water infrastructure. This chapter presents a conceptual framework to demonstrate an Internet of Things (IoT)-based intelligent hardware-software platform to efficiently manage the most critical infrastructure in sustainable smart cities: water and energy technologies. The integrated framework focuses on the challenges of water-energy nexus. It includes advanced technologies for metering and communication, and computational intelligence using machine learning techniques in purview of the infrastructural constraints for optimal integration of BES and RE source. Towards developing the conceptual framework, the systematic approach of developing an intelligent hardware-software platform is presented in this chapter. The proposed framework will be deployed in the smart city test bed at Gujarat International Finance Tec-City (GIFT), India. Test bed for water-energy nexus includes water treatment plant (WTP), sewage treatment plant (STP), and street lightings connected with BES and solar photovoltaic (PV) generation. We also discuss the use cases towards water-energy nexus that will be implemented in this framework. The intellectual merit of the framework is the development of hardware-software technology platform—comprising a set of common knowledge, theoretical approaches, mathematical models, optimization, and analytical tools—that will contribute in making possible the promising environmentally sustainable smart city.

Roadgraph Generation and Free-Space Estimation in Unknown Structured Environments for Autonomous Vehicle Motion Planning - Kessler, Tobias; Minnerup, Pascal; Esterle, Klemens; Feist, Christian; Mickler, Florian; Roth, Erwin; Knoll, Alois (21st International Conference on Intelligent Transportation Systems ITSC 2018, 2018)

Spatiotemporal Motion Planning with Combinatorial Reasoning for Autonomous Driving - Esterle, Klemens; Hart, Patrick; Bernhard, Julian; Knoll, Alois (21st International Conference on Intelligent Transportation Systems, ITSC 2018, Maui, HI, USA, November 4-7, 2018, 2018)

[T3] Develop your Own Car - Lúcio, Levi; Voss, Sebastian; Chuprina, Tatiana; Bayha, Andreas; Eder, Johannes; Kanav, Sudeep (MODELS Conference Tutorials, 2018)
AutoFOCUS3 (AF3) is a mature model-driven engineering environment to develop software for embedded systems. For the past 20 years,several versions of AF3 have served as a platform for experimenting with cutting-edge research ideas in Model-Driven Development. AF3 is a tool that fully encompasses the software life cycle, from requirements, to architecture, simulation, deployment, code generation and verification. The attendees of this tutorial will be given the unique opportunity to model and deploy software on a real remote-controlled vehicle, using only AF3. Attendees will start by modeling the software controller for a blinker, which will be integrated with the model of the vehicle’s software. The generated code will then be flashed onto a Raspberry Pi contained in the physical remote-controlled model vehicle which can then be driven in the real world. Attendees who finish early will be able to model more advanced driving assistance functionalities. The last part of the tutorial will be dedicated to deepening the attendees’ understanding of the modeling capabilities of AF3 in areas such as requirements engineering, design-space exploration, building safety cases, formal verification, modeling processes, testing or variability modeling.
Keywords: AutoFOCUS3; case study; fortissimo; rover; model-based systems engineering; MbSE

A modular approach to integrate verification tools in model based development - Kanav, Sudeep (Proceedings of the 21st ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings, 2018)
The problem of integrating an existing formal verification tool in a given software specification tool arises repeatedly both in industry and academia. At present this task is executed in an ad-hoc manner and is time consuming. Moreover, interpreting the results of the verification to locate and fix the bug (by the human user) is implicitly complicated, hence, time consuming. In this work we draft a solution for reducing the complexity of these tasks and aim at reducing the time required to complete them. We sketch a framework formalizing the concepts required to execute these tasks in a modular fashion and implement a solution based on domain specific languages (DSLs) and parameterizable model transformations. We expect that the modularity of our framework will raise its potential to be reused. We plan on evaluating this work on a set of modeling environments and a set of verification tools.
Keywords: AutoFOCUS3; simulation; case study; model-based systems engineering; MbSE

An Efficient and Time-Optimal Trajectory Generation Approach for Waypoints under Kinematic Constraints and Error Bounds - Lin, Jianjie; Somani, Nikhil; Hu, Biao; Rickert, Markus; Knoll, Alois (Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), 2018)
This paper presents an approach to generate the time-optimal trajectory for a robot manipulator under certain kinematic constraints such as joint position, velocity, acceleration, and jerk limits. This problem of generating a trajectory that takes the minimum time to pass through specified waypoints is formulated as a nonlinear constraint optimization problem. Unlike prior approaches that model the motion of consecutive waypoints as a Cubic Spline, we model this motion with a seven-segment acceleration profile, as this trajectory results in a shorter overall motion time while staying within the bounds of the robot manipulator's constraints. The optimization bottleneck lies in the complexity that increases exponentially with the number of waypoints. To make the optimization scale well with the number of waypoints, we propose an approach that has linear complexity. This approach first divides all waypoints to consecutive batches, each with an overlap of two waypoints. The overlapping waypoints then act as a bridge to concatenate the optimization results of two consecutive batches. The whole trajectory is effectively optimized by successively optimizing every batch. We conduct experiments on practical scenarios and trajectories generated by motion planners to evaluate the effectiveness of our proposed approach over existing state-of-the-art approaches.
Keywords: robotics; trajectory generation

Applications in HHI: Physical Cooperation - Rickert, Markus; Gaschler, Andre; Knoll, Alois (Humanoid Robotics: A Reference, 2018)
Humans critically depend on permanent verbal and nonverbal interaction - for aligning their mental states, for synchronizing their intentions and goals, and also for performing joint tasks, such as carrying a heavy object together, manipulating of objects in a common workspace, or handing over components and building or assembling larger structures in teams. Typically, physical interaction is initiated by a short joint planning dialog and then further accompanied by a stream of verbal utterances. For obtaining a smooth interaction flow in a given situation, humans typically use all their communication modalities and senses, and this often happens even unconsciously. As we move toward the introduction of robotic co-workers that serve humans - some of them will be humanoids; others will be of a different shape - humans will expect them to be integrated into the execution of the task at hand, just as well as if a human co-worker was involved. Such a flawless replacement will only be possible if these robots provide a number of basic action primitives, for example, handover from human to robot and vice versa. The robots must also recognize and anticipate the intention of the human by analyzing and understanding the scene as far as necessary for jointly working on the task. Most importantly, the robotic co-worker must be able to carry on a verbal and nonverbal dialog with the human partner, in parallel with and relating to the physical interaction process. In this chapter, we give an overview of the ingredients of an integrated physical interaction scenario. This includes methods to plan activities, to produce safe and human-interpretable motion, to interact through multimodal communication, to schedule actions for a joint task, and to align and synchronize the interaction by understanding human intentions. We summarize the state of the art in physical human-humanoid interaction systems and conclude by presenting three humanoid systems as case studies.
Keywords: robotics; human-robot interaction; humanoid robotics

AutomationML Mechatronic Models as Enabler of Automation Systems Engineering: Use-case and Evaluation - Vathoopan, Milan; Walzel, Hendrik; Eisenmenger, Waldemar; Zoitl, Alois; Brandenbourger, Benjamin (Proceedings of 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation (ETFA), 2018)

Controlling a virtual rover using AutoFOCUS3 - Lúcio, Levi; Kanav, Sudeep; Bayha, Andreas; Eder, Johannes (Proceedings of the MDETools Workshop co-located with MODELS 2018, 2018)
AUTOFOCUS3 (AF3) is a mature model-driven engineering environment for developing software for embedded systems. For the past 20 years, several versions of AF3 have served as a platform for experimenting with cutting edge research ideas in Model-Driven Development. AF3 is a tool that fully encompasses the software lifecycle, from requirements, to architecture, simulation, deployment, code generation and verification. In this article, we describe how we used an existing model of a complex controller for a real-life miniature vehicle and have downsized and adapted it to control a rover in a virtual environment. The model we present here automates the maneuvering of a rover to follow an-other leader rover in a virtual environment, while keeping a safe distance to it. The controller operates by adapting the rover’s speed and steering according to the position and movements of the leader. The results we present in this article illustrate the whole development cycle of an embedded system using AF3, from the development of the model down to deployment to a specific platform as well as code generation and connecting to the hardware
Keywords: AutoFOCUS3; case study; fortissimo; rover; model-based systems engineering; MbSE

Exploration of hardware topologies based on functions, variability and timing - Eder, Johannes (Proceedings of the 21st ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings, 2018)
This paper gives an overview over a dissertation project in the area of design space exploration for distributed, embedded systems. As the engineering of distributed embedded systems is getting more and more complex due to increasingly sophisticated functionalities demanding more and more powerful hardware, automation is required in order cope with this rising complexity. Using a model based systems engineering approach enables design space exploration methods which provide such automations, given a formalization of the problem in order to be solvable e.g. by SMT solvers. In this thesis we want to provide an automated synthesis of hardware topologies (E/E architectures) based on the functions which are deployed onto this topology and constraints and optimization objectives which are derived from the requirements of the system. The synthesis shall consider variability aspects (possible variants) of the hardware elements. Additionally, timing aspects of the deployed shall be regarded such that the solution of the synthesis is a hardware topology, a deployment of functions onto this topology and a schedule of these functions. The thesis shall be evaluated by using an automotive industrial use case of realistic size.
Keywords: AutoFOCUS3; design-space exploration; DSE; architecture synthesis; HW/SW co-design; model-based systems engineering; MbSE

From deployment to platform exploration: automatic synthesis of distributed automotive hardware architectures - Eder, Johannes; Bayha, Andreas; Voss, Sebastian; Ipatiov, Alexandru; Khalil, Maged (Proceedings of the 21th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, 2018)
In order to cope with the rising complexity of today's systems, model-based development of software-intensive embedded systems has become a de-facto standard in recent years. In a previous work, we demonstrated how such a model-based approach can enable automatization of certain development steps, namely the deployment of logical (platform-independent) system models to technical (platform-specific) system models. Together with Continental, we especially focused on industrial applicability. In this work, we demonstrate how we extended, again in cooperation with Continental, the previous approach in order to enable a synthesis of the topology of technical platforms (E/E architectures) together with a deployment. We furthermore introduced variability concepts in order to model variants of technical platforms which is an industrial required need. Our approach is thus capable of calculating a platform architecture and its topology which is optimized in terms of the deployment of logical system models, constraints, optimization objectives and choses the optimal variant for all technical models.
Keywords: AutoFOCUS3; design-space exploration; DSE; architecture synthesis; HW/SW co-design; model-based systems engineering; MbSE; case study

Optimization and Reconfiguration of IEC 61499-based Software Architectures - Terzimehić, Tarik (ACM/IEEE 21st International Conference on Model Driven Engineering Languages and Systems (MODELS) - Doctoral Symposium, 2018)
The fourth industrial revolution (Industry 4.0) strives for an optimized and flexible production process to reduce configuration costs. To achieve such a production process, first architecture-level decisions (i.e. deployment configuration, scheduling, etc.) are optimized. Following, these optimized architectural configurations are applied to dynamically reconfigure industrial control applications. To calculate software configurations, current research applies Design Space Exploration (DSE) techniques embedded into the IEC 61499 model-based approach. However, this research either applies simple and non-applicable constraints and objectives for real-life problems or considers architectural optimization solely at the design phase. Thus, reconfiguring industrial control applications is still an exhausting and manual task that requires production process' downtime. In this Ph.D. thesis, I handle the automatically optimized reconfiguration of the industrial automation systems. In particular, I propose applying DSE to calculate architectural configurations of IEC 61499-based control applications. To define different configuration problems from real-world situations, I identify domain-specific constraints and objectives. Furthermore, I will tackle the problem of runtime reconfiguration by applying several optimization strategies in various context scenarios and investigating an incremental search for new optimal configurations.
Keywords: Architectural Optimization; DSE; MbSE; model-based systems engineering; Industry 4.0; IEC 61499

Quantitative Projection Coverage for Testing ML-enabled Autonomous Systems - Cheng, Chih-Hong; Huang, Chung-Hao; Yasuoka, Hirotoshi (Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, 2018)

Toward an IT-strategy Approach for Small and Mid-sized Municipalities in a Federal System - Jakob, Markus; Krcmar, Helmut (18th European Conference on Digital Government, 2018)

Towards Dependability Metrics for Neural Networks - Cheng, Chih-Hong; Nührenberg, Georg; Rueß, Harald; Yasuoka, Hirotoshi (16th ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2018, Beijing, China, October 15-18, 2018, 2018)

Alternatives for Flexible Deployment Architectures in Industrial Automation Systems - Grüner, Sten; Malakuti, Somayeh; Schmitt, Johannes; Terzimehić, Tarik; Wenger, Monika; Elfham, Haitham (23rd International Conference on Emerging Technologies And Factory Automation, 2018)
One of the main challenges of future industrial systems is to flexibly (re)deploy control applications on hardware controllers - a feature that is missing in most state of the art automation systems. Due to the heterogeneous structure of control systems, e.g. different standards and hardware, a silver bullet architecture for flexible deployment seems to be infeasible. Instead we propose an abstract architecture covering different concrete reconfiguration system architectures along with a taxonomy for design decisions for the realization of such a system. The capability of the abstract architecture is demonstrated by mapping three fundamentally different concrete reconfiguration system architectures and is verified on an industrial use case of a logistic system of an aluminum cold rolling plant.
Keywords: MbSE; model-based systems engineering; deployment; reconfiguration

Der Referenzarchitekturbegriff im Wandel der Zeit - Reidt, Andreas; Pfaff, Matthias; Krcmar, Helmut (HMD Praxis der Wirtschaftsinformatik, 2018)
Architekturbegriffe spielen in der Wirtschaftsinformatik eine immer prominentere Rolle. Ein Beleg dafür ist der Begriff der Referenzarchitektur, welcher in einer stetig ansteigen Anzahl an Publikationen verwendet wird. Besonders im Kontext des Begriffs „Industrie 4.0“ und unternehmensübergreifenden Digitalisierungsbestrebungen wird der Begriff der Referenzarchitektur verstärkt verwendet, um auf eine gewisse Art der Standardisierung hinzuwirken und die Komplexität bei der Entwicklung von Systemen zu reduzieren. Jedoch ist die Verwendung des Begriffs und das Begriffsverständnis sehr heterogen, sodass der Vergleich, die Bewertung, eine Ableitung oder das Erstellen von Referenzarchitekturen sehr erschwert wird. Um solchen Herausforderung zu begegnen wird in diesem Beitrag das Begriffsverständnis von Referenzarchitekturen systematisiert, mit dem Ziel, eine einheitliche Grundlage für dessen Beschreibung und zum Vergleich von Referenzarchitekturen bereitzustellen. Hierzu werden geläufige Definitionen in Wissenschaft und Praxis dargelegt, diskutiert und an Hand der verfolgten Ziele sowie den Ausprägungen und Eigenschaften von Referenzarchitekturen systematisiert. Diese Systematik bildet dabei die Basis um auch zukünftige Begriffe und Eigenschaften im Kontext von Referenzarchitekturen einzuordnen bzw. zu klassifizieren.

Distributed Real-Time Architecture for Mixed-Criticality Systems: Algorithms and Tools - Migge, Jörn; Balbastre, Patricia; Barner, Simon; Chauvel, Franck; Craciunas, Silviu S.; Diewald, Alexander; Durrieu, Guy; Haugen, Oystein; Syed, Ali Abbas Jaffari; Pagetti, Claire; Oliver, Ramon Serna; Vasilevskiy, Anatoly (Distributed Real-Time Architecture for Mixed-Criticality Systems, 2018)
This chapter introduces the algorithms and tools to support the design and verification activities of the model driven development process. In addition, the scheduling and configuration algorithms are described to support different scheduling domains of the DREAMS architecture. This chapter begins with Section 5.1.2, which describes variability and design space exploration in the design of mixed-criticality systems. In Section 5.2, scheduling algorithms at different levels, e.g., partition level, task level, on-chip and off-chip communication are elaborated. Adaptation strategies is another topic which is covered in Section 5.3. Recovery strategies, transition modes for faster switching and algorithms for online admission of tasks in offline scheduling tables are described in this section. Timing analysis is described in Section 5.4 at different levels and Section 5.5 describes by the tools. At the Section 5.6 three toolchain use cases are presented that help to apply the toolchain.
Keywords: AutoFOCUS3; design-space exploration; DSE; architecture synthesis; HW/SW co-design; model-based systems engineering; MbSE

Distributed Real-Time Architecture for Mixed-Criticality Systems: Architectural Style - Obermaisser, Roman; Abuteir, Mohammed; Ahmadian, Hamidreza; Balbastre, Patricia; Barner, Simon; Coppola, Marcello; Coronel, Javier; Crespo, Alfons; Fohler, Gerhard; Gala, Gautam; Grammatikakis, Miltos; Ortube, Asier Larrucea; et al. (Distributed Real-Time Architecture for Mixed-Criticality Systems, 2018)
This chapter describes the architectural style of mixed-criticality systems and introduces the DREAMS waistline structure of services. It provides structuring rules according to several integration levels to support the integration of applications with different timing models and different safety assurance levels. Section 2.1 introduces the system model in mixed-criticality systems and describes the logical and physical system structures. In addition, it shows how those two system models can be mapped by a mixed-criticality name space. Section 2.2 elaborates on the DREAMS waistline structure of services and lists the core services as well as the optional services. In addi tion, the architectural building blocks and services of communication services, global time services, execution services as well as local and global resource management services are elaborated in this section. Section 2.3 gives an overview of the model-driven development based on the described building blocks. The DREAMS certification strategy along with the concept of modular certification and mixed-criticality patterns are introduced in Section 2.4. Fault assumptions is another topic which is covered in Section 2.5. The concept of fault containment regions is introduced to overcome the design faults as well as the physical faults. In addition, the failure modes, threats, threat models and threat analysis for the four major core services are elaborated in this chapter. At the end, the DREAMS harmonized platform as instantiation of the DREAMS architectural style is introduced in Section 2.6.

Distributed Real-Time Architecture for Mixed-Criticality Systems: Modeling and Development Process - Barner, Simon; Chauvel, Franck; Diewald, Alexander; Eizaguirre, Fernando; Haugen, Oystein; Migge, Jörn; Vasilevskiy, Anatoly (Distributed Real-Time Architecture for Mixed-Criticality Systems, 2018)
This chapter introduces the DREAMS metamodel and a model-driven development process ranging from variability exploration to configuration synthesis. The metamodel is described in Section 4.1 and is organized into a set of viewpoints, each of which represents one system aspect. The logical viewpoint is introduced in Section 4.2 and allows for the platform-independent description of applications. The technical viewpoint enables the hierarchical description of the architecture and services of the platform. The timing viewpoint is introduced in Section 4.3 to model timing requirements that must be satisfied in order to guarantee a correct and safe operation of the system. Safety management is another topic that is covered in Section 4.4 and is supported by a safety modeling viewpoint. The deployment and resource allocation viewpoints are addressed in Section 4.5 and link the application model with the platform model. Section 4.6 describes a configuration viewpoint and defines a model-driven process to generate deployable configuration artifacts for HW/SW target platform. Lastly, in Section 4.7 a variability viewpoint constitutes the basis of a product-line exploration process.
Keywords: AutoFOCUS3; methodology; tooling; model-based systems engineering; MbSE

Formalizing EARS – First Impressions - Lúcio, Levi; Iqbal, Tahira (2018 1st International Workshop on Easy Approach to Requirements Syntax (EARS), 2018)
The Easy Approach to Requirements Specification (EARS) has been designed primarily as a set of templates to assist requirements engineers in writing software requirements that are clear and understandable. Its target are thus requirements engineers, software architects and developers. Due to the minimalistic nature of the English sentences that make up an EARS specification, it is reasonable to expect that automated tasks can be performed on EARS specification, among which verification and code synthesis. Given English cannot be directly understood by machines without some degree of ambiguity, EARS requirements can only by automatically processed if they are translated in advance into formal specifications. In this short paper, we explore how a translation from EARS into Linear Temporal Logic can be implemented in practice.
Keywords: EARS; Linear Temporal Logic; Translation; Formalization; Model-based Systems Engineering; MbSE

Managing Standardization in eGovernment: A Coordination Theory based Analysis Framework - Balta, Dian; Krcmar, Helmut (Electronic Government, 2018)
Standardization plays an important role for a smooth organizational, semantic, technical and legal interoperation of eGovernment services. Still, standardization struggles with the complexity of administrative procedures that have to be supported and provided online. Managing this complexity poses a crucial challenge for an efficient and effective eGovernment. Different management frameworks have been developed, but the progress of standardization in practice is still perceived as insufficient. To address the challenge of standardization management in eGovernment, we propose a coordination theory based framework for analysis. It consists of three coordination modes distinguished based on their mechanisms and relevant context dimensions. In our research approach, we interpret a single case study of a standardization project in Germany where artefacts were developed from a pragmatism perspective. We discuss our findings and conclude on implications for research and practice.

Using Design Space Exploration to Calculate Deployment Configurations of IEC 61499-based Systems - Terzimehić, Tarik; Voss, Sebastian; Wenger, Monika (14th IEEE International Conference on Automation Science and Engineering (IEEE CASE 2018), 2018)
Continuous digitalization in the industry leads to new, highly complex systems that increase configuration costs. In particular, software and hardware changes cause major downtime. To dynamically reconfigure control system and avoid downtime, it is necessary to calculate valid or optimal deployment configurations. Previous research applies Design Space Exploration (DSE) techniques embedded into model-based design methodologies to calculate deployment configurations. However, current research either aims domains other than industrial automation or applies simple and, for real-life problems, not applicable constraints and objectives. Thus, the deployment of software components to hardware components is still an exhausting and manual task. In this work, we take first steps towards an automatically optimized deployment of the industrial automation systems. In particular, we propose applying DSE to calculate deployment configurations of IEC 61499-based control applications. In order to reduce the exploration space, we identify domain-specific constraints and objectives. Furthermore, we extend the IEC 61499 System and Application models' descriptions by proposing relevant hardware and software annotations. We exhibit the applicability of the identified annotations, constraints and objectives on the example of an Industry 4.0 relevant case study.
Keywords: IEC 61499; control system; design-space exploration; DSE; deployment; Industry 4.0; Model-based Systems Engineering; MbSE

An Event-Based AutomationML Model for the Process Execution of ‘Plug-and-Produce’ Assembly Systems - Danny, Paul; Ferreira, Pedro; Dorofeev, Kirill; Lohse, Niels (IEEE 16th International Conference of Industrial Informatics (INDIN), 2018)
Assembly systems today are facing significant pressure to deliver high performance process executions, while being responsive to the fluctuating market demands. However, the implementation the trending Cyber Physical Systems concepts via ‘Plug-and-Produce’ devices produces some communication overheads. In this direction, the openMOS project aims to decouple the elements that are responsible for adaptation and general operations of the system. This allows the system to have two parallel processes. Towards this end, the priority is to deliver high performance process executions, while the other process focuses on delivering the required agility. The focus of this work is narrowed down to the development of task execution tables that guarantees high performance process executions. In this direction, the definition of task execution table is based on an existing AutomationML (AML) model that highlights the explicit relationships between the Product, Process and Resource (PPR) domains. A new decisional attribute has been added to the existing ‘Skill’ concept, which provides the flexibility to incorporate event-based process alternatives. An insight description on how the system handles process executions during run-time failures is also provided. Finally, this paper illustrates the run-time implementation of the execution table with a help of an industrial case study that has been used for a demonstration activity within the openMOS project.

Verification of Binarized Neural Networks via Inter-neuron Factoring - (Short Paper) - Cheng, Chih-Hong; Nührenberg, Georg; Huang, Chung-Hao; Rueß, Harald (Verified Software. Theories, Tools, and Experiments - 10th International Conference, VSTTE 2018, Oxford, UK, July 18-19, 2018, Revised Selected Papers, 2018)

ML + FV = ♡? A Survey on the Application of Machine Learning to Formal Verification - Amrani, Moussa; Lúcio, Levi; Bibal, Adrian (arXiv, 2018)
Formal Verification (FV) and Machine Learning (ML) can seem incompatible due to their opposite mathematical foundations and their use in real-life problems: FV mostly relies on discrete mathematics and aims at ensuring correctness; ML often relies on probabilistic models and consists of learning patterns from training data. In this paper, we postulate that they are complementary in practice, and explore how ML helps FV in its classical approaches: static analysis, model-checking, theorem-proving, and SAT solving. We draw a landscape of the current practice and catalog some of the most prominent uses of ML inside FV tools, thus offering a new perspective on FV techniques that can help researchers and practitioners to better locate the possible synergies. We discuss lessons learned from our work, point to possible improvements and offer visions for the future of the domain in the light of the science of software and systems modeling.
Keywords: Model-based Systems Engineering; MbSE

Skill-based Engineering Approach using OPC UA Programs - Dorofeev, Kirill; Zoitl, Alois (IEEE 16th International Conference of Industrial Informatics (INDIN), 2018)
The modern manufacturing and production systems are changing into a flexible factory layout that raises a demand for distributed control systems, where various components from different vendors communicating over their capabilities (skills) to execute a production task. This paper offers a way of how the skills, offered by an automation system component, can be represented using a generic interface to allow the higher control levels to easily orchestrate the skills available in the system and control their execution in the runtime. We show how a skill can be modeled using a Finite State Machine and present a concrete example how the concept can be realized by means of the OPC UA communication protocol.

Towards a Common Manufacturing Service Bus to Enable Flexible Plug-and-Produce Automation - Miranda, Fabio; Martins, Renato; Dorofeev, Kirill; Gentile, Valerio; Ferreira, Pedro; Guedes, Magno (ISR 2018; 50th International Symposium on Robotics, 2018)
This paper aims to contribute to the wide adoption of emerging CPS technology, designed to increase the flexibility of current assembly lines, by incorporating real plug-and-produce capabilities and enabling skill based process execution. The solution herein proposed presents a middleware to allow fast registration and seamless communication between different automation systems and components, that is a manufacturing service bus, or MSB. This service bus integrates well known standards, such as OPC-UA and AutomationML to leverage compliance with current and future Industry 4.0 initiatives. In small lot production systems, results show that the overhead introduced by this additional stack, during production phase, is minimal when compared with the potential gain in terms of time and cost reduction during installation and ramp-up phases.

Handling system complexity in sCPS: usable design space exploration - Voss, Sebastian; Eder, Johannes (2018 IEEE/ACM 4th International Workshop on Software Engineering for Smart Cyber-Physical Systems (SEsCPS), 2018)
With a growing demand for complex features in smart cyber physical systems, the design of such system is getting increasingly complex. These features demand sound and scalable approaches to deal with the increasing design space. Consequently, standards (e.g. like ISO26262) propose methods and techniques for the systematic development of (in this case: automotive) systems. The growing amount of functionality correspondingly require more powerful electronic platforms and thus methods to deal with the integration. In this paper, we describe drivers for complexity and illustrate how formal methods, namely design space exploration techniques, can be applied to deal with this complexity. This approach is based on requirements defined by the given standards and supports the system designer by a (semi-) automatic approach to handle the complexity in system design - already in early design phases.
Keywords: AutoFOCUS3; design-space exploration; DSE; deployment synthesis; mapping; model-based systems engineering; MbSE

Applying DSE for Solving the Deployment Problem in Industry 4.0 - Terzimehić, Tarik; Voss, Sebastian; Wenger, Monika; Aravantinos, Vincent (14th Dagstuhl Workshop on Model-Based Development of Embedded Systems (MBEES), 2018)
Keywords: Model-based Systems Engineering; MbSE; design-space exploration; DSE

Model-Based Calibration of a Robotic C-Arm System Using X-Ray Imaging - Thürauf, Sabine; Hornung, Oliver; Körner, Mario; Vogt, Florian; Knoll, Alois; Nasseri, M. Ali (Journal of Medical Robotics Research, 2018)
In interventional radiology or surgery, C-arm systems are typical imaging modalities. Apart from 2D X-ray images, C-arm systems are able to perform 2D/3D overlays. For this application, a previously recorded 3D volume is projected on a 2D X-ray image for providing additional information to the clinician. The required accuracy for this application is 1.5 mm. Such a spatial accuracy is only achievable with C-arms, if a calibration is performed. State-of-the-art approaches interpolate between values of lookup tables of a sampled Cartesian volume. However, due to the non-linear system behavior in Cartesian space, a trade-off between the calibration effort and the calibrated volume is necessary. This leads to the calibration of the most relevant subvolume and high calibration times. We discuss a new model-based calibration approach for C-arm systems which potentially leads to a smaller calibration effort and simultaneously to an increased calibrated volume. In this work, we demonstrate that it is possible to calibrate a robotic C-arm system using X-ray images and that a static model of the system is required to achieve the desired accuracy for 2D/3D overlays, if re-orientations of the system are performed.
Keywords: robotics; roboterröntgen

Architecture Exploration for Safety-Critical Systems - Diewald, Alexander; Barner, Simon; Voss, Sebastian (Proceedings of the DATE Workshop on New Platforms for Future Cars: Current and Emerging Trends (NPCAR), 2018)
Future cars will host massively more functionality that comes along with the introduction of new technologies such as neural networks and data fusion, which are enablers for autonomous driving, but which require massive processing capabilities. Hence, new architectures are required that can handle the contradicting requirements for efficiency and safety compliance. The increased complexity and size of upcoming target architectures raise the need for advanced design methodologies and tool support. In this work, we present an approach that combines model-driven development (MDD) with design space exploration (DSE) that can explore suitable architectures of safety functions and platforms also in early design phases and enables trade-off decisions. The DSE uses optimization decomposition for complexity reduction and reusability while respecting the dependencies implied by development processes.
Keywords: AutoFOCUS3; design-space exploration; DSE; architecture synthesis; HW/SW co-design; model-based systems engineering; MbSE

Formal analysis of feature degradation in fault-tolerant automotive systems - Becker, Klaus; Voss, Sebastian; Schätz, Bernhard (Science of Computer Programming, 2018)
Safety critical fault-tolerant embedded systems have to react properly on failures of internal system elements to avoid failure propagation and finally a harmful external failure at the system boundary. Beside failure detection, actions for failure handling are essential to cover safety requirements. Actions reach from enabling fail-silent, fail-safe or fail-operational behavior of system elements, or also hybrids of this in a mixed criticality system design. Graceful degradation can be applied when system resources become insufficient, reducing the set of provided functional features. In this paper, we address mixed criticality and mixed reliability automotive systems. We consider mixed reliability by functional features having different fail-operational requirements. Beside pure fail-operational features, we also consider degradations of functional features, called fail-degraded features. We describe a formal system model that contains, i.a., the functional features of a vehicle, possible feature degradations, software components that realize the features, as well as the deployment of software components to execution units. We provide a structural analysis of the level of degradation on system level and feature level, which is required in scenarios of failing execution units and/or software components. Combined with this analysis, we synthesize valid deployments of software components to execution units, incorporating an adequate level of redundancy to meet the fail-operational requirements, if feasible. We apply our approach to a constructed automotive example.
Keywords: Graceful degradation; Fault tolerance; Redundancy; Fail-operational; Mixed criticality; Model-based Systems Engineering; MbSE

Künstliche Intelligenz – Chancen für Wirtschaft und Gesellschaft in Bayern - Rueß, Harald; Krcmar, Helmut (Künstliche Intelligenz – Chancen für Wirtschaft und Gesellschaft in Bayern, 2018)
Kaum ein Begriff wird derzeit so strapaziert wie Künstliche Intelligenz (KI). Sie ist inzwischen zu einem der populärsten Teilgebiete der Informatik geworden, das weit über die Grenzen des Fachs hinausstrahlt. Das vorliegende White Paper führt in das Themengebiet KI ein und beleuchtet deren Anwendungsfelder. Die Autoren vergleichen, wie Industrieländer in diesem Bereich aufgestellt sind und zeigen auf, wie sich KI Technologien auf deren Wirtschaftswachstum auswirken. Sie untersuchen, wie die Strategien erfolgreicher Nationen aussehen und wie Deutschland und insbesondere Bayern aufgestellt sind. Das Werk schließt mit konkreten Vorschlägen, wie die bayerische Wirtschaft von KI-Technologien profitieren kann und welche Kompetenzen sie dafür ausbauen muss, um den Industriestandort Bayern zu stärken.

Neural Networks for Safety-Critical Applications - Challenges, Experiments and Perspectives - Cheng, Chih-Hong; Diehl, Frederik; Hinz, Gereon Michael; Hamza, Yassine; Nührenberg, Georg; Rickert, Markus; Rueß, Harald; Truong Le, Michael (Proceedings of the Design, Automation & Test in Europe Conference & Exhibition (DATE), 2018)
We propose a methodology for designing dependable Artificial Neural Networks (ANNs) by extending the concepts of understandability, correctness, and validity that are crucial ingredients in existing certification standards. We apply the concept in a concrete case study for designing a highway ANN-based motion predictor to guarantee safety properties such as impossibility for the ego vehicle to suggest moving to the right lane if there exists another vehicle on its right.
Keywords: autonomous driving; robotics; neural networks; safety

Roboter mit Hirn - Tsakiridou, Evdoxia; von Arnim, Axel (Blog Innovations Report, 2018)
fortiss hat für ein Teilprojekt des „Human Brain Project“ einen neuen Simulator entwickelt, mit dem Neurowissenschaftler ihre Hirnmodelle in virtuelle Roboter "verpflanzen" können. Das Besondere dabei: Die virtuellen Roboter sind mit einem Gehirn ausgestattet, das mit so genannten gepulsten neuronalen Netzen arbeitet. Diese sind ihrem biologischen Vorbild näher als die aus dem maschinellen Lernen bekannten neuronalen Netze der ersten Generation. Sie versprechen eine bessere Kodierung von Nervenimpulsen und somit eine feinere Abstimmung von Bewegungen. Die Idee: Wenn Roboter sich ähnlich wie Menschen bewegen, können sie in Zukunft leichter gebaut und sicherer gesteuert werden.
Keywords: human brain project; HBP; neurorobotics; neuromorphics; brain simulation; spiking neural networks; NRP; robot simulation

KABouM: Knowledge-Level Action and Bounding Geometry Motion Planner - Gaschler, Andre; Petrick, Ronald P. A.; Khatib, Oussama; Knoll, Alois (Journal of Artificial Intelligence Research, 2018)
For robots to solve real world tasks, they often require the ability to reason about both symbolic and geometric knowledge. We present a framework, called KABouM, for integrating knowledge-level task planning and motion planning in a bounding geometry. By representing symbolic information at the knowledge level, we can model incomplete information, sensing actions and information gain; by representing all geometric entities–objects, robots and swept volumes of motions–by sets of convex polyhedra, we can efficiently plan manipulation actions and raise reasoning about geometric predicates, such as collisions, to the symbolic level. At the geometric level, we take advantage of our bounded convex decomposition and swept volume computation with quadratic convergence, and fast collision detection of convex bodies. We evaluate our approach on a wide set of problems using real robots, including tasks with multiple manipulators, sensing and branched plans, and mobile manipulation.
Keywords: robotics; smerobotics; james

Concept of Distributed Interpolation for Skill-Based Manufacturing with Real-Time Communication - Dripke, Caren; Schneider, Ben; Dragan, Mihai; Verl, Alexander (Fachkolloqium der Wissesschaftliche Gesellschaft Montage Handhabung Industrierobotik, 2018)
Distributed manufacturing unit control can be implemented by equipping all manufacturing components with individual controls offering standardized skills. The control of multi-component groups often requires real-time communication and a communication architecture that is adapted to the distributed control concept.We present applicable communication concepts for distributed interpolation, where the distributed interpolation use case in particular demonstrates challenges caused by the synchronous execution of skills.
Keywords: distributed interpolation; deterministic real-time communication; time-Sensitive Networking; IEC 61499

Using IEC 61499 Models for Automatic Network Configuration of Distributed Automation Systems - Schneider, Ben; Voss, Sebastian; Wenger, Monika; Zoitl, Alois (9th Vienna International Conference on Mathmatical Modelling (MATHMOD2018), 2018)
The new Ethernet standard Time-Sensitive Networking is an enabler for Industrial Internet of Things (IIoT) but gets more and more difficult to configure with a continuous rising number of network nodes, because each node has to be set up separately. We propose an approach towards automatic configuration of real-time networks based on models of IEC 61499, a modeling language for distributed industrial automation systems. Therefore, these existing models are analysed w.r.t. their network modeling capabilities and missing information is shown.
Keywords: distributed industrial automation; IEC 61499; Time-Sensitive Networking; TSN; real-time; deterministic networking; schedule synthesis; model-based systems engineering; MbSE

Prerequisite to Measure Information Security - A State of the Art Literature Review - Diesch, Rainer; Pfaff, Matthias; Krcmar, Helmut (Proceedings of the 4th International Conference on Information Systems Security and Privacy (ICISSP), 2018)
The field of information security is growing in research and practice over the past years. Recent studies highlight a gap in measuring and monitoring information security. In this context various definitions and synonymous expressions exist to describe information security. The aim of the work is to compare and delimit the various terms in this field of research and give a thematic overview of current articles in place. In particular, five dimensions of information security are developed and outlined. Additionally, an overview of possible research directions in the field of measuring and monitoring information security is provided.
Keywords: BMSE; Security

BMC with Memory Models as Modules - Ponce de León, Hernán; Furbach, Florian; Heljanko, Keijo; Meyer, Roland (FMCAD, 2018)
This paper reports progress in verification tool engineering for weak memory models. We present two bounded model checking tools for concurrent programs. Their distinguishing feature is modularity: Besides a program, they expect as input a module describing the hardware architecture for which the program should be verified. DARTAGNAN verifies state reachability under the given memory model using a novel SMT encoding. PORTHOS checks state equivalence under two given memory models using a guided search strategy. We have performed experiments to compare our tools against other memory model-aware verifiers and find them very competitive, despite the modularity offered by our approach.
Keywords: Model-based Systems Engineering; MbSE

A Logical Framework with Commutative and Non-commutative Subexponentials - Kanovich, Max; Kuznetsov, Stepan; Nigam, Vivek; Scedrov, Andre (Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, 2018)
Logical frameworks allow the specification of deductive systems usingthe same logical machinery. Linear logical frameworks have been successfullyused for the specification of a number of computational, logics and proofsystems. Its success relies on the fact that formulas can be distinguished as linear,which behave intuitively as resources, and unbounded, which behave intuitionistically.Commutative subexponentials enhance the expressiveness of linear logicframeworks by allowing the distinction of multiple contexts. These contexts maybehave as multisets of formulas or sets of formulas. Motivated by applicationsin distributed systems and in type-logical grammar, we propose a linear logicalframework containing both commutative and non-commutative subexponentials.Non-commutative subexponentials can be used to specify contexts which behaveas lists, not multisets, of formulas. In addition, motivated by our applications intype-logical grammar, where the weakenening rule is disallowed, we investigatethe proof theory of formulas that can only contract, but not weaken. In fact, ourcontraction is non-local. We demonstrate that under some conditions such formulasmay be treated as unbounded formulas, which behave intuitionistically.

Arch'N'Smile: A Jump'N'Run Game Using Facial Expression Recognition Control For Entertaining Children During Car Journeys - Müller, Niklas; Eska, Bettina; Schäffer, Richard; Völkel, Sarah; Braun, Michael; Wiegand, Gesa; Alt, Florian (Proceedings of the 17th International Conference on Mobile and Ubiquitous Multimedia, 2018)

Challenges in Skill-based Engineering of Industrial Automation Systems - Malakuti, Somayeh; Bock, Jürgen; Weser, Michael; Venet, Pierre; Zimmermann, Patrick; Wiegand, Mathias; Vogel, Julian; Wagner, Constantin; Bayha, Andreas (Proceedings of the 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation (ETFA), 2018)
Skill-based engineering is gaining attention as a means to increase flexibility and changeability in engineering industrial automation systems. This paper proposes the Skill-based Engineering Model (SEM), which formally describes the core entities that play a role in skill-based engineering. Accordingly, we propose a four dimensional classification scheme for skills, and assess the suitability of a property model and OWL ontologies to describe and match skills. For each case, we identify a list of challenges that must be addressed to make skill-based engineering a reality in industrial automation systems. We believe that this paper can guide researchers to study various open aspects of skill-based engineering to make it feasible in complex industrial automation systems.

Compact and efficiently verifiable models for concurrent systems - Ponce de León, Hernán; Mokhov, Andrey (Formal Methods in System Design, 2018)
Partial orders are a fundamental mathematical structure capable of representing concurrency and causality on a set of atomic events. In many applications it is essential to consider multiple partial orders, each representing a particular behavioral scenario or an operating mode of a system. With the exploding growth of the complexity of systems that software and hardware engineers design today, it is no longer feasible to represent each partial order of a large system explicitly, therefore compressed representations of sets of partial orders become essential for improving the scalability of design automation tools. In this paper we study two well known mathematical formalisms capable of the compressed representation of sets of partial orders: Labeled Event Structures and Conditional Partial Order Graphs. We discuss their advantages and disadvantages and propose efficient algorithms for transforming a set of partial orders from a given compressed representation in one formalism into an equivalent representation in another formalism without explicitly enumerating every partial order. The proposed algorithms make use of an intermediate mathematical formalism which we call Conditional Labeled Event Structures that combines the advantages of both structures. Finally, we compare these structures on a number of benchmarks coming from concurrent software and hardware domains.
Keywords: Model-based Systems Engineering; MbSE

Comprehensive View on Architectural Requirements for Maintenance Information Systems - Reidt, Andreas; Krcmar, Helmut; Schuhbäck, Stefan (Proceedings of the 13th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2018), 2018)

Connecting PLCs with their Asset Administration Shell for Automatic Device Configuration - Wenger, Monika; Müller, Thorsten; Zoitl, Alois (IEEE 16th International Conference of Industrial Informatics (INDIN), 2018)
Current industrial automation systems integrate structural information and component configuration data within the code of their programmable logic controllers. This prevents the demanded flexibility and adaptability of Industrie 4.0 systems. The asset administration shell provides a defined mechanism for finding, accessing and interpreting standardized and vendor specific data of an asset.Within this work the asset administration shell has been analyzed according to its structure, its location, and its implementation forms. Based on that a concept is proposed to provide event driven run-time access for components to the asset administration shell, which enables an automatic self-configuration infrastructure for component instances. The proposed concept is applied on the logistic part of an aluminium cold rolling mill, provided by the SMS group. For demonstration the structural information of the logistic components has been described in terms of an AutomationML file, which has been loaded into a BaseX Database. The database content represents the asset administration shell, which is accessed during runtime by XQuery requests.

Deep Reinforcement Learning for Predictive Longitudinal Control of Automated Vehicles - Buechel, Martin; Knoll, Alois (Proceedings of the 21st International Conference on Intelligent Transportation Systems (ITSC), 2018)

Developing self-similar hybrid control architecture based on sgam-based methodology for distributed microgrids - Gupta, Pragya Kirti; Duchon, Markus (Designs, 2018)

Early Take-Over Preparation in Stereoscopic 3D - Wiegand, Gesa; Mai, Christian; Liu, Yuanting; Hußmann, Heinrich (Adjunct Proceedings of the 10th International Conference on Automotive User Interfaces and Interactive Vehicular Applications, 2018)

Effect-dependent transformations for concurrent programs - Benton, Nick; Hofmann, Martin; Nigam, Vivek (Sci. Comput. Program., 2018)
We describe a denotational semantics for an abstract effect system for a higher-order,shared-variable concurrent programming language. We prove the soundness of a numberof general effect-based program equivalences, including a parallelization equationthat specifies sufficient conditions for replacing sequential composition with parallelcomposition. Effect annotations are relative to abstract locations specified by contractsrather than physical footprints allowing us in particular to show the soundness of sometransformations involving fine-grained concurrent data structures, such as MichaelScottqueues, that allow concurrent access to different parts of mutable data structures.Our semantics is based on refining a trace-based semantics for first-order programsdue to Brookes. By moving from concrete to abstract locations, and adding type refinementsthat capture the possible side-effects of both expressions and their concurrentenvironments, we are able to validate many equivalences that do not hold in an unrefinedmodel. The meanings of types are expressed using a game-based logical relationover sets of traces. Two programs e1 and e2 are logically related if one is able to solvea two-player game: for any trace with result value v1 in the semantics of e1 (challenge)that the player presents, the opponent can present an (response) equivalent trace in thesemantics of e2 with a logically related result value v2.

Enable Co-Simulation for Industrial Automation by an FMU Exporter for IEC 61499 Models - Cabral, Jose; Wenger, Monika; Zoitl, Alois (IEEE 16th International Conference of Industrial Informatics (INDIN), 2018)
Different causes have contributed to the shift of paradigm in the automation field from centralized to modular and distributable. Software and hardware of Programmable Logic Controllers (PLCs) have evolved to be synchronized with the demands nowadays and new standards are trying to follow this trend. One of them is the IEC 61499 standard, which is intended for modelling distributed industrial solutions with a vendor-independent format. This shifting is also bringing new challenges and this paper focuses on the virtual commissioning of plants, which can become a harder task when the system is distributed and involves different interconnected modules. A major problem when doing a virtual commissioning is the coupling between the different physical systems and controlling tools since many vendors still offer closed integrated solutions. Functional Mockup Interface (FMI) is a standard for a cosimulation interface which intends to fill the gaps between different modelling tools, by packaging the models into Functional Mockup Unit (FMU) and allowing a co-simulation master algorithm to have access to the inside model through the proposed interface. This paper presents a mapping between IEC 61499 models and the FMI standard and an implementation of a tool that can export IEC 61499 models into FMUs, which would allow the co-simulation of physical plants and the PLCs software that controls it. An experiment is shown where a simple ProportionalIntegral-Derivative (PID) controller of a tank system is exported as an FMU and co-simulated together with a tank system modelled using OpenModelica.

Evidential and Continuous Integration of Software Verification Tools - Beyene, Tewodros; Rueß, Harald (Formal Methods, 2018)

Formal Analysis of Sneak-Peek: A Data Centre Attack and its Mitigations - Chen, Wei; Lin, Yuhui; Galpin, Vashti; Nigam, Vivek; Lee, Myungjin; Aspinall, David (33rd IFIP TC-11 SEC 2018 International Conference on Information Security and Privacy Protection (IFIPSEC 2018) - Poznan, Poland, 2018)
Attackers can exploit covert channels, such as timing side-channels, totransmit information without data owners or network administrators being aware.Sneak-Peek is a recently considered data centre attack, where, in a multi-tenantsetting, an insider attacker can communicate with colluding outsiders by intentionallyadding delays to traffic on logically isolated but physically shared links.Timing attack mitigations typically introduce delays or randomness which canmake it difficult to understand the trade-off between level of security (bandwidthof the covert channel) and performance loss. We demonstrate that formal methodscan help. We analyse the impacts of two Sneak-Peek mitigations, namely,noise addition and path hopping. We provide a precise mathematical model ofthe attack and of the effectiveness these defences. This mathematical analysis isextended by two tool-based stochastic formal models, one formalized in UPPAALand the other in CARMA. The formal models can capture more general and largernetworks than a paper-based analysis, can be used to check properties and makemeasurements, and are more easily modifiable than conventional network simulations.With UPPAAL, we can analyse the effectiveness of mitigations and withCARMA, we can analyse how these mitigations affect latencies in typical datacentre topologies. As results, we show that using a selective strategy for path hoppingis better than a random strategy, that using the two defences in conjunctionmay actually be worse than using a single defence, and we show the connectionbetween hop frequency and network latency.

Full contract verification for ATL using symbolic execution - Oakes, Bentley James; Troya, Javier; Lúcio, Levi; Wimmer, Manuel (Software & Systems Modeling, 2018)
The Atlas Transformation Language (ATL) is currently one of the most used model transformation languages and has become a de facto standard in model-driven engineering for implementing model transformations. At the same time, it is understood by the community that enhancing methods for exhaustively verifying such transformations allows for a more widespread adoption of model-driven engineering in industry. A variety of proposals for the verification of ATL transformations have arisen in the past few years. However, the majority of these techniques are either based on non-exhaustive testing or on proof methods that require human assistance and/or are not complete. In this paper, we describe our method for statically verifying the declarative subset of ATL model transformations. This verification is performed by translating the transformation (including features like filters, OCL expressions, and lazy rules) into our model transformation language DSLTrans. As we handle only the declarative portion of ATL, and DSLTrans is Turing-incomplete, this reduction in expressivity allows us to use a symbolic-execution approach to generate representations of all possible input models to the transformation. We then verify pre-/post-condition contracts on these representations, which in turn verifies the transformation itself. The technique we present in this paper is exhaustive for the subset of declarative ATL model transformations. This means that if the prover indicates a contract holds on a transformation, then the contract’s pre-/post-condition pair will be true for any input model for that transformation. We demonstrate and explore the applicability of our technique by studying several relatively large and complex ATL model transformations, including a model transformation developed in collaboration with our industrial partner. As well, we present our ‘slicing’ technique. This technique selects only those rules in the DSLTrans transformation needed for contract proof, thereby reducing proving time.
Keywords: Model transformation; ATL; Formal verification; Symbolic execution; Contracts; Pre-/post-conditions; Model-based Systems Engineering; MbSE

Highway Sensor System as Enabler for Autonomous Driving - Wiegand, Gesa; Liu, Yuanting (2018)

Incorporating negative information to process discovery of complex systems - Ponce de León, Hernán; Nardelli, Lucio; Carmona Josep,; K. L. M. vanden Broucke, Seppe (Inf. Sci., 2018)
The discovery of a formal process model from event logs describing real process executions is a challenging problem that has been studied from several angles. Most of the contributions consider the extraction of a model as a one-class supervised learning problem where only a set of process instances is available. Moreover, the majority of techniques cannot generate complex models, a crucial feature in some areas like manufacturing. In this paper we present a fresh look at process discovery where undesired process behaviors can also be taken into account. This feature may be crucial for deriving process models which are less complex, fitting and precise, but also good on generalizing the right behavior underlying an event log. The technique is based on the theory of convex polyhedra and satisfiability modulo theory (SMT) and can be combined with other process discovery approach as a post processing step to further simplify complex models. We show in detail how to apply the proposed technique in combination with a recent method that uses numerical abstract domains. Experiments performed in a new prototype implementation show the effectiveness of the technique and the ability to be combined with other discovery techniques.
Keywords: Model-based Systems Engineering; MbSE

Modular Fault Ascription and Corrective Maintenance Using a Digital Twin - Vathoopan, Milan; Johny, Maria; Zoitl, Alois; Knoll, Alois (IFAC-PapersOnLine, 2018)

On the accuracy of formal verification of selective defenses for TDoS attacks - Lemos, Marcilio; Dantas, Yuri Gil; Fonseca, Iguatemi; Nigam, Vivek (J. Log. Algebr. Meth. Program., 2018)
Telephony Denial of Service (TDoS) attacks target telephony services, such as Voice over IP (VoIP), not allowing legitimate users to make calls. There are few defenses that attempt to mitigate TDoS attacks, most of them using IP filtering, with limited applicability. In our previous work, we proposed to use selective strategies for mitigating HTTP Application-Layer DDoS Attacks demonstrating their effectiveness in mitigating different types of attacks. Developing such types of defenses is challenging as there are many design options, e.g., which dropping functions and selection algorithms to use. Our first contribution is to demonstrate both experimentally and by using formal verification that selective strategies are suitable for mitigating TDoS attacks. We used our formal model to help decide which selective strategies to use with much less effort than carrying out experiments. Our second contribution is a detailed comparison of the results obtained from our formal models and the results obtained by carrying out experiments. We demonstrate that formal methods is a powerful tool for specifying defenses for mitigating Distributed Denial of Service attacks allowing to increase our confidence on the proposed defense before actual implementation.

Proof-Relevant Logical Relations for Name Generation - Benton, Nick; Hofmann, Martin; Nigam, Vivek (Accepted to Logical Methods in Computer Science, 2018)
Pitts and Stark’s v-calculus is a paradigmatic total language for studying the problem ofcontextual equivalence in higher-order languages with name generation. Models for the ν-calculusthat validate basic equivalences concerning names may be constructed using functor categories ornominal sets, with a dynamic allocation monad used to model computations that may allocate freshnames. If recursion is added to the language and one attempts to adapt the models from (nominal)sets to (nominal) domains, however, the direct-style construction of the allocation monad no longerworks. This issue has previously been addressed by using a monad that combines dynamic allocationwith continuations, at some cost to abstraction.This paper presents a direct-style model of a v-calculus-like language with recursion using thenovel framework of proof-relevant logical relations, in which logical relations also contain objects(or proofs) demonstrating the equivalence of (the semantic counterparts of) programs. Apart fromproviding a fresh solution to an old problem, this work provides an accessible setting in which tointroduce the use of proof-relevant logical relations, free of the additional complexities associatedwith their use for more sophisticated languages.

Roadblocks on the Highway to Secure Cars: An Exploratory Survey on the Current Safety and Security Practice of the Automotive Industry - Huber, Michael M.; Brunner, Michael; Sauerwein, Clemens; Cârlan, Carmen; Breu, Ruth (Proceedings of the 37th International Conference on Computer Safety, Reliability, and Security (SAFECOMP 2018), 2018)
With various advances in technology, cars evolved to highly interconnected and complex Cyber-Physical Systems. Due to this development, the security of involved components and systems needs to be addressed in a rigorous way. The resulting necessity of combining safety and security aspects during the development processes has proven to be non-trivial due to the high interference between these aspects and their respective treatment. This paper discusses the results of an exploratory survey on how organizations from the automotive industry in the Euroregion tackle the challenge of integrating safety and security aspects during system development. The observed state of practice shows that there are significant deficits in the integration of both domains. The results of the exploratory survey enabled us to identify the most common challenges of realizing an integrated approach in a practical setting and discuss implications for future research.
Keywords: Automotive; Cyber-Physical Systems; Safety-Security Integration; Industrial survey; Model-based systems engineering; MbSE

Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols. - Alturki, Musab A.; Kanovich, Max; Nigam, Vivek; Scedrov, Andre; Talcott, Carolyn; Ban Kirigin, Tajana ("Workshop on Foundations of Computer Security", 2018)
Distance-bounding (DB) protocols were proposed tothwart relay attacks on proximity-based access control systems.In a DB protocol, the verifier computes an upper bound on thedistance to the prover by measuring the time needed for a signalto travel to the prover and back. DB protocols are, however,vulnerable to distance fraud, in which a dishonest prover isable to manipulate the distance bound computed by an honestverifier. Despite their conceptual simplicity, devising a formalcharacterization of DB protocols and distance fraud attacks thatis amenable to automated formal analysis is non-trivial, primarilybecause of their real-time and probabilistic nature. In this work,we present a framework, based on rewriting logic, for formallyanalyzing different forms of distance-fraud, including recentlyidentified timing attacks. We introduce a generic, real-time andprobabilistic model of DB protocols and use it to (mechanically)verify false-acceptance and false-rejection probabilities undervarious settings and attacker models through statistical modelchecking with MAUDE and PVESTA. Using this framework,we first accurately confirm known results and then define andquantitatively evaluate new guessing-ahead attack strategies thatwould otherwise be difficult to analyze manually.

Subexponentials in non-commutative linear logic - Kanovich, Max; Kuznetsov, Stepan; Nigam, Vivek; Scedrov, Andre (Mathematical Structures in Computer Science, 2018)
Linear logical frameworks with subexponentials have been used for the specification of,among other systems, proof systems, concurrent programming languages and linearauthorisation logics. In these frameworks, subexponentials can be configured to allow or notfor the application of the contraction and weakening rules while the exchange rule canalways be applied. This means that formulae in such frameworks can only be organised assets and multisets of formulae not being possible to organise formulae as lists of formulae.This paper investigates the proof theory of linear logic proof systems in thenon-commutative variant. These systems can disallow the application of exchange rule onsome subexponentials. We investigate conditions for when cut elimination is admissible inthe presence of non-commutative subexponentials, investigating the interaction of theexchange rule with the local and non-local contraction rules. We also obtain some newundecidability and decidability results on non-commutative linear logic with subexponentials.

The Smile is The New Like: Controlling Music with Facial Expressions to Minimize Driver Distraction - Braun, Michael; Völkel, Sarah; Wiegand, Gesa; Puls, Thomas; Steidl, Daniel; Weiß, Yannick; Alt, Florian (Proceedings of the 17th International Conference on Mobile and Ubiquitous Multimedia, 2018)

Towards a Mathematical Understanding of the Diﬀiculty in Learning with Feedforward Neural Networks - Shen, Hao (Proceedings of the 31st IEEE Conference on Computer Vision and Pattern Recognition (CVPR), 2018)

Which barriers hinder a successful digital transformation in small and medium-sized municipalities in a federal system? - Jakob, Markus; Krcmar, Helmut (Proceedings of the Central and Eastern European e|Dem and e|Gov Days 2018, 2018)

Automated Analysis of Multi-View Software Architectures - Cheng, Chih-Hong; Hamza, Yassine; Rueß, Harald (24th Asia-Pacific Software Engineering Conference, APSEC 2017, Nanjing, China, December 4-8, 2017, 2017)

Towards Capability-Based Worker Modelling in a Smart Factory - Vernim, Susanne; Walzel, Hendrik; Knoll, Alois; Reinhart, Gunther (Proceedings of 2017 IEEE International Conference on Industrial Engineering and Engineering Management (IEEM 2017), 2017)

Designing a far-reaching view for highway traffic scenarios with 5G-based intelligent infrastructure - Hinz, Gereon Michael; Buechel, Martin; Diehl, Frederik; Chen, Guang; Krämmer, Annkathrin; Kuhn, Juri; Lakshminarasimhan, Venkatnarayanan; Schellmann, Malte; Baumgarten, Uwe; Knoll, Alois (8. Tagung Fahrerassistenzsysteme, 2017)
Cooperative vehicle infrastructure systems offer significant potential for improved traffic safety, throughput and improved energy efficiency. Infrastructure sensors along the road can substitute vehicular sensor-sets, providing improved robustness and performance through different mounting positions and orientations, reducing occlusions, stationary locations, facilitating system-wide calibration, optimization for the specific traffic area in view, and vastly increase perception range by combining multiple measurement points. Communication via fifth Generation (5G) networks offers solutions to the corresponding substantial requirements for high bandwidth, low latency and high reliability for data and information communication. We propose a concept, which aims to provide a far-reaching view to (self-driving) vehicles and drivers with infrastructure sensors and 5G communication, as a cognitive system. The system detects and localizes traffic objects and predicts their future movements. The resulting information will be provided to traffic participants allowing for safer, more proactive and comfortable driving.
Keywords: V2X; autonomous driving; connected cars; 5G; sensor-sets; far-reaching view; big data; environmental perception

Ontology for Semantic Data Integration in the Domain of IT Benchmarking - Pfaff, Matthias; Neubig, Stefan; Krcmar, Helmut (Journal on Data Semantics, 2017)
A domain-specific ontology for IT benchmarking has been developed to bridge the gap between a systematic characterization of IT services and their data-based valuation. Since information is generally collected during a benchmark exercise using questionnaires on a broad range of topics, such as employee costs, software licensing costs, and quantities of hardware, it is commonly stored as natural language text; thus, this information is stored in an intrinsically unstructured form. Although these data form the basis for identifying potentials for IT cost reductions, neither a uniform description of any measured parameters nor the relationship between such parameters exists. Hence, this work proposes an ontology for the domain of IT benchmarking, available at https://w3id.org/bmontology . The design of this ontology is based on requirements mainly elicited from a domain analysis, which considers analyzing documents and interviews with representatives from Small- and Medium-Sized Enterprises and Information and Communications Technology companies over the last eight years. The development of the ontology and its main concepts is described in detail (i.e., the conceptualization of benchmarking events, questionnaires, IT services, indicators and their values) together with its alignment with the DOLCE-UltraLite foundational ontology.
Keywords: BMSE

Robotics Library: An Object-Oriented Approach to Robot Applications - Rickert, Markus; Gaschler, Andre (Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), 2017)
We discuss the architecture and software engineering principles of the Robotics Library (RL). Driven by requirements of robot systems, research projects, industrial applications, and education, we identify relevant design requirements and present an approach to manage hardware and real-time, provide a user-friendly, object-oriented interface to powerful kinematics and dynamics calculations, and support various platforms. After over ten years of development that started in 2004 and evaluating many variants of the architecture, we discuss the design choices for the components of the library in its current version.
Keywords: robotics; robotics library

Bringing DSE to life: exploring the design space of an industrial automotive use case - Eder, Johannes; Zverlov, Sergey; Voss, Sebastian; Khalil, Maged; Ipatiov, Alexandru (2017 ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MODELS), 2017)
In order to cope with the rising complexity of today's systems, model-based development of software-intensive embedded systems has become a de-facto standard in recent years. Such a development approach enables a variety of frontloading methods. Design space exploration is one of those techniques. However, in order to properly perform a valid exploration, a system model has to have a certain quality. This requires dedicated, meaningful models as an input according to well-known design principles, which entails the structuring of models according to different viewpoints and usage of dedicated models for each of these viewpoints.In this work, we demonstrate how, based on an industrial application model represented in SysML, design space exploration methods can be efficiently applied to enable the synthesis of deployments from a logical (platform-independent) system models to technical (platform-specific) system models. Moreover, we will demonstrate the applicability of this approach by a project conducted with Continental.
Keywords: AutoFOCUS3; design-space exploration; DSE; deployment synthesis; mapping; model-based systems engineering; MbSE; case study

Device Adapter Concept towards Enabling Plug&Produce Production Environments - Dorofeev, Kirill; Cheng, Chih-Hong; Guedes, Magno; Ferreira, Pedro; Profanter, Stefan; Zoitl, Alois (Proceedings of the IEEE International Conference on Emerging Technologies And Factory Automation (ETFA), 2017)
Keywords: openmos

DREAMS Toolchain: Model-Driven Engineering of Mixed-Criticality Systems - Barner, Simon; Diewald, Alexander; Migge, Jörn; Syed, Ali Abbas Jaffari; Fohler, Gerhard; Faugère, Madeleine; Gracia Pérez, Daniel (Proceedings of the ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MODELS '17), 2017)
Mixed-criticality systems (MCS) aim at boosting the integration density in safety-critical systems, resulting into efficient systems, while simultaneously providing increased performance. The DREAMS project provides a cross-domain architectural style for MCS based on networked, virtualized multi-cores controlled by hierarchical resource managers. However, the availability of a platform is only one side of the coin: deploying mixed-critical applications to shared resources typically requires design-time configurations (e.g., to ensure real-time constraints or separation constraints mandated by safety regulations). These configurations are the outcome of complex optimization problems which are intractable in a manual process that also hardly can guarantee the consistency of all deployable artefacts nor their traceability to the requirements. However, existing toolchains lack support for MCS integration, and particularly DREAMS' advanced platform capabilities. We present an integrated model-driven toolchain and the underlying metamodels covering all relevant aspects of MCS including applications, timing, platforms, deployments, configurations and annotations for extra-functional properties such as safety. The approach focuses on the left branch of the V-cycle, and ranges from product-line and design space exploration to resource allocation and configuration generation. We report on the integration of exploration tools and a reconfiguration graph synthesizer, and evaluate the resulting toolchains in two use cases consisting of a product-line of wind power control applications and an avionic subsystem respectively.
Keywords: Multicore processing; Resource management; Safety; Tools; Mixed-Criticalitity Systems; Product-Lines; AutoFOCUS3; design-space exploration; DSE; architecture synthesis; HW/SW co-design; model-based systems engineering; MbSE

EARS-CTRL: Building and Verifying Controllers for Dummies - Lúcio, Levi; Rahman, Salman; bin Abid, Saad; Mavin, Alistair (Tools and Demo Session track at MoDELS 2017, 2017)
In this paper we present the EARS-CTRL tool forsynthesizing and validating controller software for embeddedsystems. EARS-CTRL has as starting point requirements writtenin (English) natural language, more specifically in the EARS(Easy Approach to Requirements Syntax) language invented atRolls-Royce and currently in use at numerous organizationsaround the world. After expressing the requirements in English,the requirements engineer can produce the controller code atthe press of a button. EARS-CTRL then provides facilitiesfor validating the generated controller that allow step-by-stepsimulation or test-case generation using MATLAB Simulink.
Keywords: Software Controllers; Natural Language; Code Synthesis; MatLab Simulink; Model-based Systems Engineering; MbSE

ExplicitCase: Integrated Model-based Development of System and Safety Cases - Cârlan, Carmen; Barner, Simon; Diewald, Alexander; Tsalidis, Alexandros; Voss, Sebastian (Proceedings of the SAFECOMP 2017 Workshops ASSURE, DECSoS, SASSUR, TELERISE, and TIPS, 2017)
Tools for creating safety cases currently on the market target safety experts, whose main concern is the management of safety cases. However, for safety assurance, safety experts should collaborate with technical experts, who have better understanding of technical and operational hazards. Thus, there should be a closer collaboration between the management of safety cases and technical expertise. Technical expertise may be retrieved, among others, from model-based system artifacts and processes. In order to close the gap between safety and technical expertise, we present ExplicitCase, an open-source tool for semi-automatic modeling, maintenance, and verification of safety cases integrated with system models. The advantage of this tool is two-fold. First, it enables its users to capture safety relevant information from model-based artifacts into safety cases. Second, it makes the safety cases rationale available to engineers in order to help them reason about design choices, while minding safety concerns. We evaluate the approach and the implemented tool based on the experiences obtained in a project use case.
Keywords: Safety Cases; Goal Structuring Notation; System Models; AutoFOCUS3; model-based safety cases; ExplicitCase; model-based systems engineering; MbSE

Expressive Symbolic-Execution Contract Proving for the DSLTrans Transformation Language - Oakes, Bentley James; Lúcio, Levi; Gomes, Cláudio; Vangheluwe, Hans (McGill University, School of Computer Science, 2017)
The verification of model transformations is key for the adoption of model-driven engineering in academic and industrial processes. In this work, we provide a verification technique for our model transformation language DSLTrans, which is both confluent and terminating by construction. This technique proves structural pre-condition/ post-condition structural contracts for all inputs to a transformation. This is achieved by creating path conditions for the transformation through a symbolic execution of the transformation’s rules. These path conditions then represent all possible transformation executions through an abstraction relation. In this work, we provide a detailed description of both the path condition construction and contract proving techniques. As well, we provide arguments that our techniques are valid, such that proving a contract on the finite set of path conditions for a transformation implies that the contract holds on the infinite set of abstracted transformation executions.
Keywords: Model-based Systems Engineering; MbSE

GSN Support of Mixed-Criticality Systems Certification - Nicolas, Carlos-Fernando; Eizaguirre, Fernando; Ortube, Asier Larrucea; Barner, Simon; Chauvel, Franck; Sagardui, Goiuria; Pérez, Jon (Proceedings of the SAFECOMP 2017 Workshops ASSURE, DECSoS, SASSUR, TELERISE, and TIPS, 2017)
Safety-critical applications could benefit from the standardisation, cost reduction and cross-domain suitability of current heterogeneous computing platforms. They are of particular interest for Mixed-Criticality Product Lines (MCPL) where safety- and non-safety functions can be deployed on a single embedded device using suitable isolation artefacts and development processes. The development of MCPLs can be facilitated by providing a reference architecture, a model-based design, analysis tools and Modular Safety Cases (MSC) to support the safety claims. In this paper, we present a method based on the MSCs to ease the certification of MCPLs. This approach consists of a semi-automated composition of layered argument fragments that trace the safety requirements argumentation to the supporting evidences. The core of the method presented in this paper is an argument database that is represented using the Goal Structuring Notation language (GSN). The defined method enables the concurrent generation of the arguments and the compilation of evidences, as well as the automated composition of safety cases for the variants of products. In addition, this paper exposes an industrial-grade case study consisting of a safety wind turbine system where the presented methodology is exemplified.
Keywords: Goal Structuring Notation (GSN); Model-Based Development; Safety-critical Systems; Product Lines; Variability

Model-based Performance Evaluation of Batch and Stream Applications for Big Data - Kroß, Johannes; Krcmar, Helmut (2017 IEEE 25th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS), 2017)
Batch and stream processing represent the two main approaches implemented by big data systems such as Apache Spark and Apache Flink. Although only stream applications are intended to satisfy real-time requirements, both approaches are required to meet certain response time constraints. In addition, cluster architectures continuously expand and computing resources constitute high investments and expenses for organizations. Therefore, planning required capacities and predicting response times is crucial. In this work, we present a performance modeling and simulation approach by using and extending the Palladio component model. We predict performance metrics of batch and stream applications and its underlying processing systems by the example of Apache Spark on Apache Hadoop. Whereas most related work concentrates on one specific processing technique and focuses on the metric response time, we propose a general approach and consider the utilization of resources as well. In different experiments we evaluated our approach using applications and data workloads of the HiBench benchmark suite. The results indicate accurate predictions for upscaling cluster sizes as well as workloads with errors less than 18%.

OPC UA for Plug & Produce: Automatic Device Discovery using LDS-ME - Profanter, Stefan; Dorofeev, Kirill; Zoitl, Alois; Knoll, Alois (Proceedings of the IEEE International Conference on Emerging Technologies And Factory Automation (ETFA), 2017)
Current manufacturing and production are changing more and more into a flexible and adaptable factory layout that requires rapid changeover and short reconfiguration times of machines. Additionally the setup time for new devices should be as short as possible. In this paper we propose a hierarchical architecture for a multi-level Plug & Produce system and evaluate the proposed structure using open source OPC UA implementations for easy integration of new devices into an existing system. Aside from the requirements for such a system, basic concepts of the OPC UA Discovery Service Set are described and different open source OPC UA implementations for C/C++ and Java are compared.
Keywords: robotics; openmos

Process-Aware Model-Driven Development Environments - Lúcio, Levi; bin Abid, Saad; Rahman, Salman; Aravantinos, Vincent; Harwardt, Eduard; Kuestner, Ralf (MODELS Workshops, 2017)
Due to recent advances in Domain Specific Language (DSL) workbenches, it has become possible to build model-driven development environments as sets of individual DSLs that get composed for a specific purpose. In this paper we explore how model-driven development environments can become process-aware, to assist the user when building a model. We offer an explanation to our ideas at three levels of abstraction: 1) the meta-meta level, the Meta-Programming System (MPS) workbench with its language definition capabilities; 2) the meta level, where brick DSLs are defined and assembled into frameworks that are further tailored for particular modelling scenarios through the introduction of an explicit process for model construction; and 3)the model level, where models are built through progressive tool-guided refinements and automated steps based on the process introduced at the metalevel. We exemplify our approach by providing the main highlights of the ongoing development of a model-driven requirements gathering environment for our industrial partners.
Keywords: Process-awareness; Domain-Specific Languages; DSLs; Model Construction; generic requirement gathering; framework; process language; requirement refinement process; requirement engineer; model-based systems engineering; MbSE

How to Teach Your Robot in 5 Minutes: Applying UX Paradigms to Human-Robot-Interaction - Kraft, Martin; Rickert, Markus (Proceedings of the IEEE International Symposium on Robot and Human Interactive Communication (RO-MAN), 2017)
When creating modern and visually appealing user experiences for the interaction with industrial robots, previously known and universally applicable paradigms in app and web design can be utilized to increase accessibility and usability of the to be created service. This is especially the case when the expected user group consists of untrained and inexperienced users and therefore system interaction focus is laid more on build progress overview, safety for human and robot, as well as overall simplification of complicated features. In this paper, we present four of the most important paradigms of modern graphical user experiences in web and app design that can be used to forward the concept of interacting with an industrial robot without any experience-related thresholds. By redesigning an existing interaction concept of a working robot cell system for assembly tasks in a small and medium-sized enterprise environment the presented paradigms are being utilized. The achieved improvements are then examined in a before-after user study to analyze the paradigm's success in suiting the user's expectation and anticipation using the redesigned service.
Keywords: robotics; smerobotics

Automatically Classifying User Engagement for Dynamic Multi-party Human–Robot Interaction - Foster, Mary Ellen; Gaschler, Andre; Giuliani, Manuel (International Journal of Social Robotics, 2017)
A robot agent designed to engage in real-world human–robot joint action must be able to understand the social states of the human users it interacts with in order to behave appropriately. In particular, in a dynamic public space, a crucial task for the robot is to determine the needs and intentions of all of the people in the scene, so that it only interacts with people who intend to interact with it. We address the task of estimating the engagement state of customers for a robot bartender based on the data from audiovisual sensors. We begin with an offline experiment using hidden Markov models, confirming that the sensor data contains the information necessary to estimate user state. We then present two strategies for online state estimation: a rule-based classifier based on observed human behaviour in real bars, and a set of supervised classifiers trained on a labelled corpus. These strategies are compared in offline cross-validation, in an online user study, and through validation against a separate test corpus. These studies show that while the trained classifiers are best in a cross-validation setting, the rule-based classifier performs best with novel data; however, all classifiers also change their estimate too frequently for practical use. To address this issue, we present a final classifier based on Conditional Random Fields: this model has comparable performance on the test data, with increased stability. In summary, though, the rule-based classifier shows competitive performance with the trained classifiers, suggesting that for this task, such a simple model could actually be a preferred option, providing useful online performance while avoiding the implementation and data-scarcity issues involved in using machine learning for this task.
Keywords: robotics; james

Environment Effects at Phantom-Based X-Ray Pose Measurements - Thürauf, Sabine; Körner, Mario; Vogt, Florian; Hornung, Oliver; Nasseri, M. Ali; Knoll, Alois (Proceedings of the International Conference of the IEEE Engineering in Medicine and Biology Society (EMBC), 2017)
Image-based pose measurements relative to phantoms are used for various applications. Some examples are: tracking, registration or calibration. If highly precise measurements are needed, even changes of environment factors influence the measurements. This work evaluates how humidity and room temperature affect an image based pose measurements using a phantom. The pose measurement is used for the specific use case of an absolute accurate calibration of a C-arm X-ray system. However, the results are transferable to other applications, too. We describe the effects on different measurement parameters and experimentally evaluate the imprecisions caused by water absorption and thermal expansion of the phantom. The real world results show, that it is needed to monitor the environment effects if measurement precisions in the submillimeter scale are necessary.
Keywords: robotics; roboterröntgen

Absolute Accurate Calibration of a Robotic C-Arm System based on X-Ray Observations using a Kinematic Model - Thürauf, Sabine; Hornung, Oliver; Körner, Mario; Vogt, Florian; Nasseri, M. Ali; Knoll, Alois (Proceedings of the Workshop on Surgical Robots: Compliant, Continuum, Cognitive, and Collaborative, IEEE International Conference on Robotics and Automation (ICRA), 2017)
C-arm X-ray systems are commonly used imaging modalities in surgery or interventional radiology. In addition to typical 2D X-ray images, 2D/3D overlays can be performed by these systems. For the 2D/3D overlay a high spatial accuracy of 1:5mm is needed. This accuracy is only achievable, if a spatial calibration of the system is performed. We introduce a new calibration technique for C-arm systems based on an absolute accurate robot calibration to speed up the calibration process and increase the calibrated working volume in future. This work is a proof of concept and shows that the accuracy needed for 2D/3D overlays is achievable with an absolute accurate robot calibration based on X-ray images. However, a deformation model is needed if the C-arm system is reorientated.
Keywords: robotics; roboterröntgen

Estimating Worst-Case Bounds for Open CPS Runtimes with Genetic Algorithms - Horst, Oliver; Baumgarten, Uwe; Prehofer, Christian (Proceedings of the 8th Real-Time Scheduling Open Problems Seminar (RTSOPS) held in conjunction with the 29th Euromicro Conference on Real-Time Systems (ECRTS), 2017)

Motion Planning under Perception and Control Uncertainties with Space Exploration Guided Heuristic Search - Chen, Chao; Rickert, Markus; Knoll, Alois (Proceedings of the IEEE Intelligent Vehicles Symposium, 2017)
Reliability and safety are extremely important for autonomous driving in real traffic scenarios. However, due to imperfect control and sensing, the actual state of the vehicle cannot be flawlessly predicted or measured, but estimated with uncertainty. Therefor, it is important to consider the execution risk advance in motion planning for a solution with a high success rate. The Space Exploration Guided Heuristic Search (SEHS) method is extended to deal with perception and control uncertainty in its two planning stages. First, the localization uncertainty is evaluated with a simple probabilistic robot model by the Space Exploration to find a path corridor with sufficient localization quality for the desired motion accuracy. Then, a trajectory controller is modeled with nonholonomic kinematics for the belief propagation of a robot state with primitive motions. The dynamic model and the control feedback are approximated in a close neighborhood of the reference trajectory. In this case, the Heuristic Search can propagate the state uncertainty as a normal distribution in the search tree to guarantee a high probability of safety and to achieve the required final accuracy. The belief-based SEHS is evaluated in several simulated scenarios. Compared to the basic SEHS method that assumes perfection, motions with higher execution successful rate are produced, especially the human-like behaviors for driving through narrow passages and precise parking. This confirms the major contribution of this work in exploiting the uncertainties for motion planning in autonomous driving.
Keywords: robotics; autonomous driving; path planning

Software Deployment Analysis for Mixed Reliability Automotive Systems - Becker, Klaus (TU München, 2017)
Safety critical systems require rising dependability due to increasing autonomy. Fault-tolerance is necessary, but failures may cause system resources to become insufficient to provide all intended functional features. We introduce an approach to formally analyze failure scenarios in mixed criticality systems, combined with the synthesis of valid deployments of software to hardware, incorporating adequate redundancy to address mixed reliability. Based on a formal system model, we provide a structural analysis of necessary degradations and failovers in failure scenarios, while ensuring the fulfillment of fail-operational requirements.
Keywords: Fault Tolerance; Graceful Degradation; Fail-Operational; Dependability; Reliability; Mixed Criticality; Safety; Deployment; Redundancy; Synthesis; Automotive; Formal Methods; Model-based Systems Engineering; MbSE

A web-based system architecture for ontology-based data integration in the domain of IT benchmarking - Pfaff, Matthias; Krcmar, Helmut (Enterprise Information Systems, 2017)
In the domain of IT benchmarking (ITBM), a variety of data and information are collected. Although these data serve as the basis for business analyses, no unified semantic representation of such data yet exists. Consequently, data analysis across different distributed data sets and different benchmarks is almost impossible. This paper presents a system architecture and prototypical implementation for an integrated data management of distributed databases based on a domain-specific ontology. To preserve the semantic meaning of the data, the ITBM ontology is linked to data sources and functions as the central concept for database access. Thus, additional databases can be integrated by linking them to this domain-specific ontology and are directly available for further business analyses. Moreover, the web-based system supports the process of mapping ontology concepts to external databases by introducing a semi-automatic mapping recommender and by visualizing possible mapping candidates. The system also provides a natural language interface to easily query linked databases. The expected result of this ontology-based approach of knowledge representation and data access is an increase in knowledge and data sharing in this domain, which will enhance existing business analysis methods.
Keywords: BMSE; Semantic Web; Ontology

Just Formal Enough? Automated Analysis of EARS Requirements - Lúcio, Levi; Rahman, Salman; Cheng, Chih-Hong; Mavin, Alistair (NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings, 2017)
EARS is a technique used by Rolls-Royce and many other organizations around the world to capture requirements in natural language in a precise manner. In this paper we describe the EARS-CTRL tool for writing and analyzing EARS requirements for controllers. We provide two levels of analysis of requirements written in EARS-CTRL: firstly our editor uses projectional editing as well as typing (based on a glossary of controller terms) to ensure as far as possible well-formedness by construction of the requirements; secondly we have used a controller synthesis tool to check whether a set of EARS-CTRL requirements is realizable as an actual controller. In the positive case, the tool synthesizes and displays the controller as a synchronous dataflow diagram. This information can be used to examine the specified behavior and to iteratively correct, improve or complete a set of EARS-CTRL requirements.
Keywords: Natural Language; Linear Temporal Logic; Requirement Engineer; Controller Synthesis; Model-based Systems Engineering; MbSE

Seamless Model-based Requirements Engineering: Models, Guidelines, Tools - Teufl, Sabine (Technische Universität München, 2017)
A practical model-based approach for requirements engineering (RE) should address all of the following challenges: Textual documentation; analysis, validation and verification of requirements; the integration of RE into a comprehensive development approach; guidance and tool support. These challenges have previously been studied in isolation. This work examines these challenges holisticly, selects models, guidelines and tool support, and integrates them into a seamless model-based RE approach.
Keywords: AutoFOCUS3; MIRA; model-based requirements engineering; model-based systems engineering; MbSE

An Exact Solver for Geometric Constraints with Inequalities - Somani, Nikhil; Rickert, Markus; Knoll, Alois (IEEE Robotics and Automation Letters, 2017)
CAD/CAM approaches have been used in the manufacturing industry for a long time, and their use in robotic systems is becoming more popular. One common element in these approaches is the use of geometric constraints to define relative object poses. Hence, approaches for solving these geometric constraints are critical to their performance. In this work, we present an exact solver for geometric constraints. Our approach is based on mathematical models of constraints and geometric properties of constraint nullspaces. Our constraint solver supports non-linear constraints with inequalities, and also mixed transformation manifolds, i.e., cases where the rotation and translation components of the constraints are not independent. Through several applications, we show how inequality constraints and mixed transformation manifolds increase the expressive power of constraint-based task definitions. The exact solver provides repeatable solutions with deterministic runtimes and our experiments show that it is also much faster than comparable iterative solvers.
Accepted for presentation at ICRA 2017
Keywords: robotics

Connecting Artificial Brains to Robots in a Comprehensive Simulation Framework: The Neurorobotics Platform - Falotico, Egidio; Vannucci, Lorenzo; Ambrosano, Alessandro; Albanese, Ugo; Ulbrich, Stefan; Vasquez Tieck, Juan Camilo; Hinkel, Georg; Kirtay, Murat; Peric, Igor; Denninger, Oliver; Cauli, Nino; Roennau, Arne; et al. (Frontiers in Neurorobotics, 2017)
Combined efforts in the fields of neuroscience, computer science, and biology allowed to design biologically realistic models of the brain based on spiking neural networks. For a proper validation of these models, an embodiment in a dynamic and rich sensory environment, where the model is exposed to a realistic sensory-motor task, is needed. Due to the complexity of these brain models that, at the current stage, cannot deal with real-time constraints, it is not possible to embed them into a real-world task. Rather, the embodiment has to be simulated as well. While adequate tools exist to simulate either complex neural networks or robots and their environments, there is so far no tool that allows to easily establish a communication between brain and body models. The Neurorobotics Platform is a new web-based environment that aims to fill this gap by offering scientists and technology developers a software infrastructure allowing them to connect brain models to detailed simulations of robot bodies and environments and to use the resulting neurorobotic systems for in silico experimentation. In order to simplify the workflow and reduce the level of the required programming skills, the platform provides editors for the specification of experimental sequences and conditions, environments, robots, and brain–body connectors. In addition to that, a variety of existing robots and environments are provided. This work presents the architecture of the first release of the Neurorobotics Platform developed in subproject 10 “Neurorobotics” of the Human Brain Project (HBP).1 At the current state, the Neurorobotics Platform allows researchers to design and run basic experiments in neurorobotics using simulated robots and simulated environments linked to simplified versions of brain models. We illustrate the capabilities of the platform with three example experiments: a Braitenberg task implemented on a mobile robot, a sensory-motor learning task based on a robotic controller, and a visual tracking embedding a retina model on the iCub humanoid robot. These use-cases allow to assess the applicability of the Neurorobotics Platform for robotic tasks as well as in neuroscientific experiments.
Keywords: robotics; software architectures; robot programming; web technologies; human brain project; HBP; neurorobotics; neuromorphics; brain simulation; spiking neural networks; NRP; robot simulation

A Framework for Analyzing Adaptive Autonomous Aerial Vehicles - Mason, Ian; Nigam, Vivek; Talcott, Carolyn; Vasconcelos De Brito, Alisson (Software Engineering and Formal Methods - SEFM 2017 Collocated Workshops: DataMod, FAACS, MSE, CoSim-CPS, and FOCLASA, Trento, Italy, September 4-5, 2017, Revised Selected Papers, 2017)
Unmanned aerial vehicles (UAVs), a.k.a. drones, are becoming increasingly popular due to great advancements in their control mechanisms and price reduction. UAVs are being used in applications such as package delivery, plantation and railroad track monitoring, where UAVs carry out tasks in an automated fashion. Devising how UAVs achieve a task is challenging as the environment where UAVs are deployed is normally unpredictable, for example, due to winds. Formal methods can help engineers to specify flight strategies and to evaluate how well UAVs are going to perform to achieve a task. This paper proposes a formal framework where engineers can raise the confidence in their UAV specification by using symbolic, simulation and statistical and model checking methods. Our framework is constructed over three main components: the behavior of UAVs and the environment are specified in a formal executable language; the UAV's physical model is specified by a simulator; and statistical model checking algorithms are used for the analysis of system behaviors. We demonstrate the effectiveness of our framework by means of several scenarios involving multiple drones.

A rewriting framework and logic for activities subject to regulations - Kanovich, Max; Ban Kirigin, Tajana; Nigam, Vivek; Scedrov, Andre; Perovic, Ranko; Talcott, Carolyn (Mathematical Structures in Computer Science, 2017)
Activities such as clinical investigations (CIs) or financial processes are subject to regulations to ensure quality of results and avoid negative consequences. Regulations may be imposed by multiple governmental agencies as well as by institutional policies and protocols. Due to the complexity of both regulations and activities, there is great potential for violation due to human error, misunderstanding, or even intent. Executable formal models of regulations, protocols and activities can form the foundation for automated assistants to aid planning, monitoring and compliance checking. We propose a model based on multiset rewriting where time is discrete and is specified by timestamps attached to facts. Actions, as well as initial, goal and critical states may be constrained by means of relative time constraints. Moreover, actions may have non-deterministic effects, i.e. they may have different outcomes whenever applied. We present a formal semantics of our model based on focused proofs of linear logic with definitions. We also determine the computational complexity of various planning problems. Plan compliance problem, for example, is the problem of finding a plan that leads from an initial state to a desired goal state without reaching any undesired critical state. We consider all actions to be balanced, i.e. their pre- and post-conditions have the same number of facts. Under this assumption on actions, we show that the plan compliance problem is PSPACE-complete when all actions have only deterministic effects and is EXPTIME-complete when actions may have non-deterministic effects. Finally, we show that the restrictions on the form of actions and time constraints taken in the specification of our model are necessary for decidability of the planning problems.

Analysis of design strategies for unmanned aerial vehicles using co-simulation - Barros, Jose de Sousa; Oliveira, Thyago; Nigam, Vivek; Brito, Alisson (Design Autom. for Emb. Sys., 2017)
Designing critical embedded systems, like UAVs is not a trivial task because it brings the challenge of dealing with the uncertainty that is inherent to this type of systems, e.g., winds, GPS uncertainty, etc. Simulation and verification tools that provide a level of confidence can help design such systems and increase the safety of specified cyber-physical systems before deployment. This paper presents a framework for evaluating flight strategies of UAVs. Our framework is constructed by integrating, using high-level architecture, Ptolemy, a high level specification tool, and SITL/Ardupilot, a domain specific UAV simulator. It allows to evaluate flight strategies under the presence of uncertainty, such as winds, with a level of confidence by constructing a sufficiently large number of simulations. Its effectiveness is demonstrated by testing two different flight strategies in two scenarios under different wind intensities. We measure the flight quality providing quantitative information about the quality of the tested flight strategy, such as distance traveled, with a confidence of 95% and error of 8%.

Arguing from Hazard Analysis in Safety Cases: A Modular Argument Pattern - Gleirscher, Mario; Cârlan, Carmen (2017 IEEE 18th International Symposium on High Assurance Systems Engineering (HASE), 2017)
We observed that safety arguments are prone tostay too abstract, e.g. solutions refer to large packages, argumentstrategies to complex reasoning steps, contexts and assumptionslack traceability. These issues can reduce the confidence werequire of such arguments. In this paper, we investigate theconstruction of confident arguments from (i) hazard analysis(HA) results and (ii) the design of safety measures, i.e., bothused for confidence evaluation. We present an argument patternintegrating three HA techniques, i.e., FTA, FMEA, and STPA, aswell as the reactions on the results of these analyses, i.e., safetyrequirements and design increments. We provide an example ofhow our pattern can help in argument construction and discusssteps towards using our pattern in formal analysis and computer-assisted construction of safety cases.
Keywords: Model-based systems engineering; MbSE

Arguing on Software-Level Verification Techniques Appropriateness - Cârlan, Carmen; Gallina, Barbara; Kacianka, Severin; Breu, Ruth (Proceedings of the International Conference on Computer Safety, Reliability, and Security (SAFECOMP), 2017)
In this paper, we investigate the pondered selection of innovative software verification technology in the safety-critical domain and its implications. Verification tools perform analyses, testing or simulation activities. The compliance of the techniques implemented by these tools to fulfill standard-mandated objectives (i.e., to be means of compliance in the context of DO-178C and related supplements) should be explained to the certification body. It is thereby difficult for practitioners to use novel techniques, without a systematic method for arguing their appropriateness. Thus, we offer a method for arguing the appropriate application of a certain verification technique (potentially in combination with other techniques) to produce the evidence needed to satisfy certification objectives regarding fault detection and mitigation in a realistic avionics application via safety cases. We use this method for the choice of an appropriate compiler to support the development of a drone.
Keywords: Model-based Systems Engineering; MbSE

autoCode4: Structural Controller Synthesis - Cheng, Chih-Hong; Lee, Edward A.; Rueß, Harald (Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS, 2017)

Erstellung einer Referenzarchitektur anhand von individuellen Unternehmensanforderungen - Reidt, Andreas; Duchon, Markus; Krcmar, Helmut (Abschlussveröffentlichung S-CPS: Ressourcen-Cockpit für Sozio-Cyber-Physische Systeme, 2017)

Evaluating Software-defined Networking for Deterministic Communication in Distributed Industrial Automation Systems - Schneider, Ben; Zoitl, Alois; Wenger, Monika; Blech, Jan Olaf (IEEE International Conference on Emerging Technologies And Factory Automation (ETFA), 2017)
As networks continuously grow (keyword Internet of Things) the configuration and management of industrial networks gets more complex. Additionally the trend towards Ethernet networks in the domain of industrial automation leads to the adoption of new Ethernet based technologies for factory automation. One of these technologies is Software Defined Networking (SDN), which provides a programmable and more flexible method for network control through an abstract network view. This work focuses on the evaluation of SDN in the field of industrial automation. It provides the implementation of a prototype SDN controller for direct multicast routing of industrial traffic in a cyclic switched Ethernet network using the Ryu SDN framework. For evaluation, experiments about the performance penalty introduced by switch-controller-communication are performed. An IEC 61499 compliant development environment is used for the experiment definition. The experiment results and the prototype implementation of the SDN controller showed that SDN provides great opportunities for a flexible and reliable network setup in the automation industry and is suited for real-time traffic.
Keywords: software defined networking; SDN; UDP multicast routing; Ryu; IEC 61499; switched industrial Ethernet

Increasing Control Application Reusability through Generic Device Configuration Model - Eisenmenger, Waldemar; Meßmer, Johannes; Wenger, Monika; Zoitl, Alois (IEEE International Conference on Emerging Technologies And Factory Automation (ETFA), 2017)

Living Safety Arguments for Open Systems - Cârlan, Carmen (Proceedings of the 2017 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), 2017)
In recent years, there has been a shift from closed systems, with clearly defined borders, whose behavior is completely determined a priori, towards open systems. An open system is an independently developed system, which is able to communicate and cooperate with other open systems in an ad-hoc manner, at runtime. Moreover, due to their openness, such systems may be used in various contexts. Whenever open systems collaborate in a safety-critical context at runtime, the functional safety of both the individual open systems and emerged system of open systems needs to be assured. More and more regulations nowadays require a safety argumentation of the system. I thereby propose an approach for automatically adapting the safety argumentation built manually, during design time, according to the new operational environment information. To evaluate and validate the proposed solution, the approach will be applied to 1) a system of autonomous drones cooperating for intelligent intersection management, and 2) a system of cooperative transport robots in an industrial setting.
Keywords: Model-based Systems Engineering; MbSE

Maximum Resilience of Artificial Neural Networks - Cheng, Chih-Hong; Nührenberg, Georg; Rueß, Harald (Automated Technology for Verification and Analysis - 15rd International Symposium , ATVA, 2017)

Minimizing Test Suites with Unfoldings of Multithreaded Programs - Saarikivi, Olli; Ponce de León, Hernán; Kähkönen, Kari; Heljanko, Keijo; Esparza, Javier (ACM Trans. Embedded Comput. Syst., 2017)
This article focuses on computing minimal test suites for multithreaded programs. Based on previous work on test case generation for multithreaded programs using unfoldings, this article shows how this unfolding can be used to generate minimal test suites covering all local states of the program. Generating such minimal test suites is shown to be NP-complete in the size of the unfolding. We propose an SMT encoding for this problem and two methods based on heuristics which only approximate the solution, but scale better in practice. Finally, we apply our methods to compute the minimal test suites for several benchmarks.
Keywords: Model-based Systems Engineering; MbSE

Modeling and verifying behavioral constraints for automation systems - Brandenbourger, Benjamin; Vathoopan, Milan; Zoitl, Alois (Industrial Informatics (INDIN), 2017 IEEE 15th International Conference on, 2017)

Modular Transformation from AF3 to nuXmv - Kanav, Sudeep; Aravantinos, Vincent (Proceedings of MODELS 2017 Satellite Event: Workshops (ModComp, ME, EXE, COMMitMDE, MRT, MULTI, GEMOC, MoDeVVa, MDETools, FlexMDE, MDEbug), Posters, Doctoral Symposium, Educator Symposium, ACM Student Research Competition, and Tools and Demonstrations, 2017)
AutoFOCUS3 (AF3) supports formal verification of its models using the nuXmv model checker. This requires a model transformation from AF3 to nuXmv models. In this paper we present this behavior transformation. It is a two way transformation between a high-level and a low-level model involving intricate cases typical of behavior transformations whose solutions can therefore be beneficial to the community.
Keywords: AutoFOCUS3; formal verification; model-based systems engineering; MbSE

Multi vehicle trajectory coordination for automated parking - Kessler, Tobias; Knoll, Alois (IEEE Intelligent Vehicles Symposium (IV), 2017)

On subexponentials, focusing and modalities in concurrent systems - Nigam, Vivek; Olarte, Carlos; Pimentel, Elaine (Theor. Comput. Sci., 2017)
In this work we present the focused proof system SELLF⋒, which extends intuitionistic linear logic with subexponentials with the ability of quantifying over them, hence allowing for the use of an arbitrary number of modalities. We show that the view of subexponentials as specific modalities is general enough to give a modular encoding of different flavors of Concurrent Constraint Programming (CCP), a simple and powerful model of concurrency. More precisely, we encode CCP calculi capturing time, spatial and epistemic behaviors into SELLF⋒, thus providing a proof theoretic foundation for those calculi and, at the same time, setting SELLF⋒ as a general framework for specifying such systems.

Ontology-Based Traffic Scene Modeling, Traffic Regulations Dependent Situational Awareness and Decision-Making for Automated Vehicles - Buechel, Martin; Hinz, Gereon Michael; Ruehl, Frederik; Schroth, Hans; Gyoeri, Csaba; Knoll, Alois (IEEE Intelligent Vehicles Symposium (IV) 2017, 2017)
accepted

Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Models - Ponce de León, Hernán; Furbach, Florian; Heljanko, Keijo; Meyer, Roland (SAS, 2017)
We present PORTHOS, the first tool that discovers porting bugs in performance-critical code. PORTHOS takes as input a program and the memory models of the source architecture for which the program has been developed and the target model to which it is ported. If the code is not portable, PORTHOS finds a bug in the form of an unexpected execution
Keywords: Model-based Systems Engineering; MbSE

Referenzarchitektur eines Ressourcen-Cockpits zur Unterstützung der Instandhaltung - Reidt, Andreas; Duchon, Markus; Krcmar, Helmut (Abschlussveröffentlichung S-CPS: Ressourcen-Cockpit für Sozio-Cyber-Physische Systeme, 2017)

Slow TCAM Exhaustion DDoS Attack - Pascoal, Tulio; Dantas, Yuri Gil; Fonseca, Iguatemi; Nigam, Vivek (ICT Systems Security and Privacy Protection - 32nd IFIP TC 11 International Conference, SEC 2017, Rome, Italy, May 29-31, 2017, Proceedings, 2017)
Software Defined Networks (SDN) facilitate network management by decoupling the data plane which forwards packets using efficient switches from the control plane by leaving the decisions on how packets should be forwarded to a (centralized) controller. However, due to limitations on the number of forwarding rules a switch can store in its TCAM memory, SDN networks have been subject to saturation and TCAM exhaustion attacks where the attacker is able to deny service by forcing a target switch to install a great number of rules. An underlying assumption is that these attacks are carried out by sending a high rate of unique packets. This paper shows that this assumption is not necessarily true and that SDNs are vulnerable to Slow TCAM exhaustion attacks (Slow-TCAM). We analyse this attack arguing that existing defenses for saturation and TCAM exhaustion attacks are not able to mitigate Slow-TCAM due to its relatively low traffic rate. We then propose a novel defense called SIFT based on selective strategies demonstrating its effectiveness against the Slow-TCAM attack.

Systematically comparing control approaches in the presence of actuator errors - Kessler, Tobias; Minnerup, Pascal; Lenz, David; Knoll, Alois (IEEE Intelligent Vehicles Symposium (IV), 2017)

Time, computational complexity, and probability in the analysis of distance-bounding protocols - Kanovich, Max; Nigam, Vivek; Scedrov, Andre; Talcott, Carolyn; Ban Kirigin, Tajana (Journal of Computer Security, 2017)
Many security protocols rely on the assumptions on the physical properties in which its protocol sessions will be carried out. For instance, Distance Bounding Protocols take into account the round trip time of messages and the transmission velocity to infer an upper bound of the distance between two agents. We classify such security protocols as Cyber-Physical. Time plays a key role in design and analysis of many of these protocols. This paper investigates the foundational differences and the impacts on the analysis when using models with discrete time and models with dense time. We show that there are attacks that can be found by models using dense time, but not when using discrete time. We illustrate this with an attack that can be carried out on most Distance Bounding Protocols. In this attack, one exploits the execution delay of instructions during one clock cycle to convince a verifier that he is in a location different from his actual position. We additionally present a probabilistic analysis of this novel attack. As a formal model for representing and analyzing Cyber-Physical properties, we propose a Multiset Rewriting model with dense time suitable for specifying cyber-physical security protocols. We introduce Circle-Configurations and show that they can be used to symbolically solve the reachability problem for our model, and show that for the important class of balanced theories the reachability problem is PSPACE-complete. We also show how our model can be implemented using the computational rewriting tool Maude, the machinery that automatically searches for such attacks.

Tool Support for Live Formal Verification - Aravantinos, Vincent; Kanav, Sudeep (2017 ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MODELS), 2017)
Despite an increasing interest from industry (e.g., DO333 standard [1]), formal verification is still not widely used in production for safety critical systems. This has been recognized for a while and various causes have been identified, one of them being the lack for scalable and cost effective tools. Many such tools exist for formal verification, but few of them are userfriendly: using formal verification generally still requires such an effort that the time spent on the tool prevents the integration of the method in an industrial setting. This paper presents a tool prototype aiming at supporting non-experts in using formal verification. The tooling approach is meant to be cost effective and change-supportive: user-friendliness is designed not only for the non-expert, but also to require minimum effort so that formal verification is triggered even for the non-enthusiast who is not willing to push a button. To do so, we trigger, in a background task, pre-defined formal verification checks at (almost) every change of the model. We only display error messages in case of problem: the user is not disturbed if no problem is detected. To prevent checks to be triggered all the time, we decide to consider only local analyses (i.e., only checks which do not require knowledge of elements in a remote position in the model). This restricts the sort of formal verification that we support, but this is a conscious choice: our motto is ”Let us first make basic techniques very user-friendly; more powerful ones will be considered only when at least the basic techniques have proven to be accepted”.
Keywords: program verification; software tools; formal verification; safety critical systems; automata; component architectures; AutoFOCUS3; formal verification; model-based systems engineering; MbSE

Towards a Model-driven Performance Prediction Approach for Internet of Things Architectures - Kroß, Johannes; Voss, Sebastian; Krcmar, Helmut (Open Journal of Internet Of Things, 2017)
Indisputable, security and interoperability play major concerns in Internet of Things (IoT) architectures and applications. In this paper, however, we emphasize the role and importance of performance and scalability as additional, crucial aspects in planning and building sustainable IoT solutions. IoT architectures are complicated system-of-systems that include different developer roles, development processes, organizational units, and a multilateral governance. Its performance is often neglected during development but becomes a major concern at the end of development and results in supplemental efforts, costs, and refactoring. It should not be relied on linearly scaling for such systems only by using up-to-date technologies that may promote such behavior. Furthermore, different security or interoperability choices also have a considerable impact on performance and may result in unforeseen trade-offs. Therefore, we propose and pursue the vision of a model-driven approach to predict and evaluate the performance of IoT architectures early in the system lifecylce in order to guarantee efficient and scalable systems reaching from sensors to business applications.
Keywords: Model-based Systems Engineering; MbSE

Towards an Industry 4.0 Compliant Control Software Architecture Using IEC 61499 & OPC UA - Terzimehić, Tarik; Wenger, Monika; Zoitl, Alois; Bayha, Andreas; Becker, Klaus; Müller, Thorsten; Schauerte, Hubertus (IEEE International Conference on Emerging Technologies And Factory Automation (ETFA), 2017)
The fourth industrial revolution introduced additional requirements on the industrial systems' control software in order to cope with current manufacturing systems' flexibility demands. These requirements include, among others, a dynamic reconfigurability, software reusability and an external service orchestration. This work presents the design of an industry 4.0 compliant control software architecture resulting from an iterative design process. The architecture is based on the reconfiguration services of the IEC 61499 standard and the service orchestration via OPC UA. We demonstrate the software architecture's compliance to the industry 4.0 requirements on an aluminum cold rolling mill plant demonstrator.
Keywords: Industry 4.0; MbSE; model-based systems engineering; OPC UA; IEC 61499

Towards an integrated plant engineering process using a data conversion tool for AutomationML - Vathoopan, Milan; Brandenbourger, Benjamin; George, Amil; Zoitl, Alois (Industrial Technology (ICIT), 2017 IEEE International Conference on, 2017)

embSFI: An Approach for Software Fault Isolation in Embedded Systems - Ruhland, Andreas; Prehofer, Christian; Horst, Oliver (1st Workshop on Security and Dependability of Critical Embedded Real-Time Systems, 2016)
co-located with the IEEE Real-Time Systems Symposium 2016

Comparably Evaluating Communication Performance within Mixed-Criticality Systems - Napier, Keegan; Horst, Oliver; Prehofer, Christian (4th International Workshop on Mixed Criticality Systems (WMC), 2016)

Modeling and Simulating Apache Spark Streaming Applications - Kroß, Johannes; Krcmar, Helmut (Softwaretechnik-Trends, 2016)
Stream processing systems are used to analyze big data streams with low latency. The performance in terms of response time and throughput is crucial to ensure all arriving data are processed in time. This depends on various factors such as the complexity of used algorithms and configurations of such distributed systems and applications. To ensure a desired system behavior, performance evaluations should be conducted to determine the throughput and required resources in advance. In this paper, we present an approach to predict the response time of Apache Spark Streaming applications by modeling and simulating them. In a preliminary controlled experiment, our simulation results suggest accurate prediction values for an upscaling scenario.

Decomposition of Design Space Exploration Problems in the Context of model-based Development - Zverlov, Sergey (Proceedings of the Doctoral Symposium at the 19th ACM/IEEE International Conference of Model-Driven Engineering Languages and Systems (MODELS 2016), 2016)
During the development process of complex embedded systems there typically is a large number of architectural decisions that engineers are facing. Each of them can influence the properties of the end result (ie: cost, performance, etc.). A systematic process that supports this decision making is often referred to as Design Space Exploration (DSE). The need for computer-aided DSE methods was recognized by the research community which resulted in a large number of publications in this area. The contribution of this PhD project is two-fold: First contribution is a classification of typical DSE problems that arise during the development process of embedded systems. Due their high popularity in this area the focus of this work lies on the model-based approaches. The second contribution is two provide a decomposition approach for complex DSE problems. The decomposition strategy is thereby based on the previously identified DSE problem classes.
Keywords: Design Space Exploration; Model-Based Systems Engineering; MbSE; Decomposition; Architecture Optimization

Intuitive Instruction of Industrial Robots: Semantic Process Descriptions for Small Lot Production - Perzylo, Alexander; Somani, Nikhil; Profanter, Stefan; Kessler, Ingmar; Rickert, Markus; Knoll, Alois (Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), 2016)
In this paper, we introduce a novel robot programming paradigm. It focuses on reducing the required expertise in robotics to a level that allows shop floor workers to use robots in their application domain without the need of extensive training. Our approach is user-centric and can interpret underspecified robot tasks, enabling communication on an abstract level. Such high-level task descriptions make the system amenable for users that are experts in a particular domain, but have limited knowledge about robotics and are thus not able to specify low-level details and instructions. Semantic models for all involved entities, i.e., processes, workpieces, and workcells, enable automatic reasoning about underspecified tasks and missing pieces of information. We showcase and evaluate this methodology on two industrial use cases from the domains of assembly and woodworking, comparing it to state-of-the-art solutions provided by robot manufacturers.
Keywords: robotics; smerobotics

Sicherheitsaspekte von Industrie 4.0 - Reidt, Andreas; Duchon, Markus; Krcmar, Helmut (Tagungsband Smarte Fabrik & Smarte Arbeit – Industrie 4.0 gewinnt Kontur VPP2016 – Vernetzt planen und produzieren, 2016)

Task Level Robot Programming using Prioritized Non-Linear Inequality Constraints - Somani, Nikhil; Rickert, Markus; Gaschler, Andre; Cai, Caixia; Perzylo, Alexander; Knoll, Alois (Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), 2016)
In this paper, we propose a framework for prioritized constraint-based specification of robot tasks. This framework is integrated with a cognitive robotic system based on semantic models of processes, objects, and workcells. The target is to enable intuitive (re-)programming of robot tasks, in a way that is suitable for non-expert users typically found in SMEs. Using CAD semantics, robot tasks are specified as geometric interrelational constraints. During execution, these are combined with constraints from the environment and the workcell, and solved in real-time. Our constraint model and solving approach supports a variety of constraint functions that can be non-linear and also include bounds in the form of inequalities, e.g., geometric interrelations, distance, collision avoidance and posture constraints. It is a hierarchical approach where priority levels can be specified for the constraints, and the nullspace of higher priority constraints is exploited to optimize the lower priority constraints. The presented approach has been applied to several typical industrial robotic use-cases to highlight its advantages compared to other state-of-the-art approaches.
Keywords: robotics; smerobotics

Usable Design Space Exploration in AutoFOCUS3 - Eder, Johannes; Voss, Sebastian (Joint Proceedings of the 12th Educators Symposium (EduSymp 2016) and 3rd International Workshop on Open Source Software for Model Driven Engineering (OSS4MDE 2016) co-located with MODELS 2016, 2016)
Software-intensive embedded systems are characterized by an increasing number of features that implement complex functionalities. To effectively manage this complexity, development processes in general, and model-based approaches in particular, support the development of such systems as model-based approaches have been considered a central design approach to deal with increasing complexity in software and hardware development. A valid system design and configuration, especially a safety-critical system design, has to fulfill a corresponding set of requirements describing all desired system constraints and objectives. In general, these constraints may be contradicting and correspond to different dimensions (e.g. timing, safety, energy, cost, etc.). Thus, considering all system constraints during system design is a manually unsolvable task. To support the system designer, usable Design Space Exploration methods are needed. Therefore, a proper tool implementation is needed that supports the usability. In this paper, we describe a Design Space Exploration process which aims to explore the architectural design space during system design. This process has been implemented in the open source CASE tool AutoFOCUS3 with the focus on usability.
Keywords: AutoFOCUS3; design-space exploration; DSE; model-based systems engineering; MbSE

An Adaptive Nonlinear Model Predictive Controller for Longitudinal Motion of Automated Vehicles - Buechel, Martin; Knoll, Alois (2016 IEEE Conference on Control Applications (CCA), 2016)
Keywords: Automated Vehicles; Autonomous Vehicles; Adaptive Control; Model Predictive Control; Nonlinear Control; Longitudinal Control

Building Product-lines of Mixed-Criticality Systems - Barner, Simon; Diewald, Alexander; Eizaguirre, Fernando; Vasilevskiy, Anatoly; Chauvel, Franck (Proceedings of the Forum on Specification and Design Languages (FDL 2016), 2016)
Mixed-Criticality Systems (MCS) reconcile safety-critical requirements with multi-core architectures, by offering spatial and temporal isolation while preserving other extra-functional properties such as optimised energy consumption or minimised latencies. MCS designers struggle to manually balance the offered functionalities with pertinent implementation choices in order to ensure that the system eventually meets all constraints. Existing attempts to further automate this process focus on specific concerns, and fail to account for variation in system functionalities. Our contribution is to integrate product-lines that capture functional variations with evolutionary optimisation to explore possible implementations and their impact on extra-functional properties. Our solution is a model-driven process (and a tool prototype) to automatically select functionally different products that balance well the various concerns of interest. We illustrate how this process applies to the construction of wind turbines.
Keywords: Product-lines; cyber-physical systems; MCS; evolutionary optimisation; mixed-criticality systems; multicore architectures; wind turbines; Energy consumption; AutoFOCUS3; design-space exploration; DSE; architecture synthesis; HW/SW co-design; model-based systems engineering; MbSE

Interconnecting Product and Process Information to Enable Personalized Production - Walzel, Hendrik; Keddis, Nadine (Procedia CIRP, 2016)
Manufacturing paradigms are currently shifting from mass production towards mass customization and personalized products. Customers demand individual, high quality products that are tailored to their needs at a low cost and reasonable delivery times. The shoe and fashion industry is one example. Currently, mass customizing textile products is possible but comes with long delivery times due to fragmented supply chains that are distributed all over the world. Therefore, companies are under the pressure to reduce their time to market and to respond to the dynamic requirements regarding lot sizes, lead times, and cost. Moreover, companies will shift to regional production to be closer to the customer to flexibly react to the market and reduce delivery times. This paper presents an approach to model personalized products and interconnect this knowledge with information about the manufacturing system and production processes. The approach allows using product information to assist the worker during the manufacturing process to enable quickly switching between different products. Connecting the shop floor with the supervisory control facilitates adapting to new products. The approach is evaluated using an experimental setup. Results and future research directions are illustrated here.
The Sixth International Conference on Changeable, Agile, Reconfigurable and Virtual Production (CARV2016)

Referenzarchitektur eines Ressourcen-Cockpits zur Unterstützung der Instandhaltung - Reidt, Andreas; Duchon, Markus; Krcmar, Helmut (fortiss GmbH, 2016)

Experimental Evaluation of the Accuracy at the C-Arm Pose Estimation with X-Ray Images - Thürauf, Sabine; Vogt, Florian; Hornung, Oliver; Körner, Mario; Nasseri, M. Ali; Knoll, Alois (Proceedings of the International Conference of the IEEE Engineering in Medicine and Biology Society (EMBC), 2016)
C-arm X-ray systems need a high spatial accuracy for applications like cone beam computed tomography and 2D/3D overlay. One way to achieve the needed precision is a model-based calibration of the C-arm system. For such a calibration a kinematic and dynamic model of the system is constructed whose parameters are computed by pose measurements of the C-arm. Instead of common measurement systems used for a model-based calibration for robots like laser trackers, we use X-ray images of a calibration phantom to measure the C-arm pose. By the direct use of the imaging system, we overcome registration errors between the measurement device and the C-arm system. The C-arm pose measurement by X-ray imaging, the new measurement technique, has to be evaluated to check if the measurement accuracy is sufficient for the modelbased calibration regarding the two mentioned applications. The scope of this work is a real world evaluation of the C-arm pose measurement accuracy with X-ray images of a calibration phantom using relative phantom movements and a laser tracker as ground truth.
Keywords: robotics; roboterröntgen

A Realistic X-Ray Simulation for C-Arm Geometry Calibration - Thürauf, Sabine; Wolf, Markus; Körner, Mario; Vogt, Florian; Hornung, Oliver; Nasseri, M. Ali; Knoll, Alois (Proceedings of the IEEE International Conference on Biomedical Robotics and Biomechatronics (BioRob), 2016)
Applications like cone beam computed tomographies (CBCTs) or 2D-3D overlays need a high geometrical accuracy of the C-arm system. In order to achieve this, geometry calibrations are performed to increase the accuracy given by the kinematics of the system. Commonly X-ray images of a phantom with known geometry are taken for the calibration. The images, together with a 3D model of the phantom, serve as input for an optimizer, which estimates the pose of the C-arm relative to the phantom. Afterwards, the estimates are used to increase the geometrical accuracy of the system. Inaccuracies due to real world effects appear, e.g. manufacturing or assembly inaccuracies of the phantom, the position of the X-ray tube, or the pose of the detector. To evaluate these factors separately a simulation is helpful, which needs to be as realistic as possible. To achieve this we defined three requirements, which have to be fulfilled: realistic noise, realistic absolute errors and similar error distributions within the working volume. By means of these criteria we investigate if our simulation mirrors a real world C-arm pose measurement for C-arm geometry calibration sufficiently.
Keywords: robotics; roboterröntgen

Combining Task and Motion Planning for Intersection Assistance Systems - Chen, Chao; Rickert, Markus; Knoll, Alois (Proceedings of the IEEE Intelligent Vehicles Symposium, 2016)
A hybrid planning approach is developed for intersection assistance systems up to fully automated driving through intersections. Route planning, task planning and motion planning methods are integrated in a hierarchical planning framework to deal with the various information and constraints in different layers. The navigation agent provides a global driving direction at an intersection according to the selected route. The task planner decides a sequence of actions to accomplish the driving mission taking into consideration traffic rules and semantic conditions. The motion planner generates detailed trajectories to execute the tasks. Meanwhile, the task sequence and the motion trajectory are verified periodically against the actual traffic situation, and re-planning is triggered when necessary in the motion planning or task planning level. The hierarchical planning framework is evaluated in several intersection scenarios. The result shows that it can handle the complex planning problems with dynamic objects and provide a modular solution for automated driving that can be easily extended for different traffic rules and applications.
Keywords: autonomous driving

On Cognitive Robot Woodworking in SMErobotics - Haage, Mathias; Profanter, Stefan; Kessler, Ingmar; Perzylo, Alexander; Somani, Nikhil; Sörnmo, Olof; Karlsson, Martin; Gestegård Robertz, Sven; Nilsson, Klas; Resch, Ludovic; Marti, Michael (Proceedings of the International Symposium on Robotics (ISR), 2016)
This paper details and discusses work performed at the woodworking SME Mivelaz Techniques Bois SA within the EU FP7 project SMErobotics. The aim is to improve non-expert handling of the cell by introduction of cognitive abilities in the robot system. Three areas are considered; intuitive programming, process adaptation and system integration. Proposed cognitive components are described together with experiments performed.
Keywords: robotics; smerobotics

Industrieroboter für KMU: Flexible und intuitive Prozessbeschreibung - Rickert, Markus; Perzylo, Alexander (Industrie Management, 2016)
Die Produktion in kleinen und mittelständischen Unternehmen (KMU) findet oft im Rahmen von Kleinserien oder sogar Einzelfertigung statt. Um diese KMU durch Roboter-basierte Automatisierung zu unterstützen, bedarf es eines Umdenkens in der Ausgestaltung der Bedienkonzepte. In diesen Anwendungsszenarien gewinnt die effiziente Programmierung und Adaption enorm an Stellenwert. Zudem muss das benötigte Vorwissen im Umgang mit Robotern soweit reduziert werden, dass Facharbeiter ohne großen Ausbildungsaufwand Robotersysteme selbst bedienen können. In diesem Beitrag stellen wir einen wissensbasierten Ansatz vor, der die genannten Herausforderungen behandelt.
Keywords: robotics; smerobotics

Schedule synthesis for multi-period SW components - Voss, Sebastian; Eder, Johannes; Schätz, Bernhard (SAE 2016 World Congress and Exhibition, 2016)
The growing complexity of functionalities in automotive vehicles and their safety-criticality, including timing requirements, demands sound and scalable approaches to deal with the increasing design space. Most often, such complex automotive systems are composed of a set of functions that are characterized by multi-period timing behaviors, e.g., due to environment constraints limiting sensing/acting frequencies, or various worst case execution times of software components.As safety-critical systems must perform the desired behavior within guaranteed time bounds, a valid system configuration is needed including a time-correct schedule that fulfills all timing requirements. This contribution proposes a systematic and correct schedule synthesis of complex multi-rate automotive software systems that ensures precise timing behavior of software components.The proposed synthesis approach - guaranteeing given timing requirements, based on preemptive, time-triggered scheduling - optimizes non-harmonic task sets by minimizing context switches between these tasks. This approach is integrated into the AUTOFOCUS 3 tool-chain, using its models of a software component architecture as well as of a hardware platform, combined with precalculated interrupt sets and a symbolic encoding scheme to synthesize schedules meeting the given multi-rate timing requirements. The approach is demonstrated using an Adaptive Cruise Control System.
Keywords: AutoFOCUS3; design-space exploration; DSE; scheduling; model-based systems engineering; MbSE