Hermann Kaindl

Safety verification of robot applications is extremely challenging due to the complexity of the environment that a robot typically operates in. Formal verification with model-checking provides guarantees but it may often take too long or even fail for complex models of the environment. A usual solution approach is abstraction, more precisely behavioral abstraction. Our new approach introduces structural abstraction instead, which we investigated in the context of voxel representation of the robot environment. This kind of abstraction leads to abstract voxels. We also propose a complete and automated verification workflow, which is based on an already existing methodology for robot applications, and inspired by the key ideas behind counterexample-guided abstraction refinement (CEGAR) - performing an initial abstraction and successively introducing refinements based on counterexamples, intertwined with model-checker runs. Hence, our approach uses selective refinement of structural abstractions to improve the runtime efficiency of model-checking. A fully-automated implementation of our approach showed its feasibility, since counterexamples have been found for a realistic scenario with a fairly high (maximal) resolution in a few minutes, while direct model-checker runs led to a crash after a couple of days.

Software product lines can generate significant cost-efficiencies but managing their evolution is becoming more difficult. There are several reasons. The volume, variety and velocity of products is increasing particularly as customers demand personalized products. The corporate memory about the product line's history and development recedes as the personnel that manage and develop the product line ebb and flow from the organization. The economic, environmental, regulatory and social contexts into which the products were launched also continues to evolve. A significant challenge of the management task is product comparison. Product comparison is important for gauging whether (i) to build a new product or not (ii) a product aligns with the corporate brand (iii) a product falls within legislative and regulatory boundaries (iv) a product line platform needs to be reorganized. Product comparison can be of value during product-line scoping, domain engineering and application engineering. We will discuss two different approaches to address this challenge. One is grounded in feature modelling, the other in case-based reasoning. We will also describe a specific product comparison approach using similarity matching, in which a product configured from a product line feature model is represented as a weighted binary string. Weighted binary strings can represent product features and a binary string metric can be used to evaluate product and feature similarity (where 1 represents a feature's presence, 0 its absence, and the weight represents its relative importance to the product). Binary strings map easily to feature selection processes, are low on storage requirements and enable fast comparison computations with existing similarity metrics and measuring tools. For large feature trees, the deployment of weights for each feature is only feasible if the initial allocation is done automatically. The overall similarity between products can be compared using a binary string metric, and the significance of individual feature combinations for product similarity can be explored by modifying the weights. We will illustrate our ideas with a mobile phone example, and discuss some of the benefits and limitations of this approach.

Efficient charging of electric vehicles (EVs) on highways is important for ensuring e-mobility because of the comparably limited range of EVs and the potentially very long charging times during longer trips. For reducing the carbon footprint of EVs, matching demand with availability of renewable energy matters, i.e., the latter should be used when available. Hence, we opt for dynamic 'anytime' optimization of the allocation of EVs to charging sites preferably at time slots where renewable energy is predicted to be available, while taking into account charging properties of batteries as well. This paper outlines a genetic algorithm approach for this optimization task, which takes these objectives into account as well as charging station availability and the number of yet unscheduled EVs. Our algorithm integrates with Eclipse SUMO (Simulation of Urban MObility) for simulating the real-world environment. The proposed algorithm operates on a real highway network (the one in Austria) and offers efficient and sustainable solutions for reducing the environmental impact of EVs.

Applications for mobile devices (apps) have facilitated the success of smartphones and tablets. By using apps, the multipurpose hardware of modern devices can be utilized to the full extent. Despite much progress in development methods, software development kits, and frameworks, app development poses many challenges. This is even more so for novel mobile devices such as wearables and for the hardware that constitutes the Internet-of-Things (IoT) and Cyber-Physical Systems (CPS). Compatibility, performance, battery-saving, and security and safety are only some of the issues that are mainly driven by the quality of the used software. A satisfying level of this quality in many cases is very hard to achieve and proper techniques for testing and formal verification are needed.

Process models in general, and those specifying process-oriented software in particular, should be formally verified. While activity-oriented process models have been verified against object life cycles, formally specified semantic specifications of actions were not involved. Hence, previous approaches for the verification of process models did not make use of declaratively represented knowledge of actions. This paper presents a new approach for verification of consistency between process models, object life cycles, and context-dependent semantic action specifications. This approach involves declarative specifications of all the actions of a process, which also depend on the context of use of the actions. These context-dependent specifications define the ‘logic’ of the process flow, which is grounded in (extended) object life cycles. Since a subtyping relation is enforced, reuse is facilitated through substitutability. Our extension of object life cycles makes them applicable to processes including non-monotonicity, and even to model communication based on physical interaction in cyber-physical systems. As a consequence, this formal consistency verification ensures that all the involved specifications ‘fit together’, both procedurally and logically.