Describing a system in a requirements specification demands correctness and conciseness. Requirements are redundant if they are stated multiple times throughout a specification (explicitly or implicitly). In contrast to vacuity, redundancies do not inherently indicate specification defects, and are sometimes even inevitable to adequately follow safety practices. However, intended redundancies have to be managed to avoid subsequent errors. Unintended redundancies often hint to defects in the requirements specification. We present an analysis for redundancies in formal real-time requirements specifications based on automata theoretical model checking. To enable this analysis, we introduce a determinism preserving totalization and complement procedure for the timed automaton model of Phase Event Automata. We state the redundancy check for a set of real-time requirements as a program analysis task. Benchmarks show the viability of our approach to analyse requirements sets of industrial size and complexity: the analysis scales well on industrial sets, interesting redundancies both from requirements and as a formalisation artefact were found.

Abstract Formal pattern languages are used in industry to communicate and analyse requirements, as they are said to be both machine-readable and intuitively understandable for humans. The questions arise to what extent this intuitive understanding of a pattern language is in agreement with its formal semantics and whether this understanding can be increased systematically. We present two consecutive empirical experiments to address these questions. The formal semantics serves as an objective judge on the intuitive understanding. Our experiments confirm the practical usefulness of HanforPL insofar the intuition matches the formal semantics in most practically relevant cases. They also reveal a number of edge cases where even a prior exposure to formal logic is not a guarantee for correct understanding. We present and validate systematic adjustments to the patterns, leading to several large increases in understandability but come at the cost of new, but less impactful ambiguities. We demonstrate how an inquiry on the alignment of the intuitive and formal semantics of a pattern language can help to understand and improve the language. While results regarding the understandability of HanforPL are favourable in commonly used cases, there is potential for improvement. The systematic adaption of patterns shows that small modifications may have large effects on the alignment of formal and intuitive semantics, and that modification must be considered with caution in the context of the respective pattern to avoid unintentionally adding new ambiguities. This article is an extension of our published REFSQ paper.

Instance segmentation of unknown objects from images is regarded as relevant for several robot skills including grasping, tracking and object sorting. Recent results from computer vision have shown that large hand-labeled datasets enable high segmentation performance. To overcome the time-consuming process of manually labeling data for new environments, we present a transfer learning approach for robots that learn to segment objects by interacting with their environment in a self-supervised manner. Our robot pushes unknown objects on a table and uses information from optical flow to create training labels given by object masks. To achieve this, we fine-tune an existing DeepMask instance segmentation network on the self-labeled training data acquired by the robot. We evaluate our trained network (SelfDeepMask) on a set of real images showing challenging and cluttered scenes with novel objects. Here, SelfDeepMask outperforms the DeepMask network trained on the COCO dataset by 8.6% in average precision.