Abstract Automated robotic systems operating in real-world environments require thorough test campaigns before deployment, in which engineers assess whether the system is actually exposed to critical scenarios. A well-established way to judge the efficacy of test campaigns in controlled environments is scenario coverage: It quantifies the quality of recorded data from test campaigns w.r.t. a set of (critical) scenario classes of interest. Challenges arise when transferring coverage from controlled to open environments, as it may no longer be exactly determined to which scenario class the recorded test data belongs to: sensors offer limited observability, e.g., by occlusions or hardware failures, and specifications might be inherently vague, e.g., via imprecise traffic regulations. We leverage the Open World Assumption to formally extend scenario coverage to such ambiguous test data and present algorithms for computing guaranteed lower and upper bounds on coverage. Whereas deciding the lower bound problem is $$D^p$$ D p -complete, the upper bound can be computed in polynomial time. We extend an existing coverage software tool with two approaches for incorporating the Open World Assumption, grounded in LTL f . Our evaluation shows that meaningful statements on scenario coverage are feasible, even under intricacies of the real world.

We present a post-hoc approach for scenario-based testing of automated driving systems, enabling the analysis of safety and correctness for (cooperative) automated driving systems in many scenarios without conducting tests for individual scenarios. The system under test is operated in its physical environment’ and data is recorded during operation. Then, driving scenarios are identified in this data and functional requirements are checked, yielding pass or fail verdicts for individual scenarios. We validate the envisioned post-hoc approach in a single-case mechanism experiment by the example of a platooning controller, identifying a previously unknown bug in the tested system, as well as a functional insufficiency concerning the intended operational design domain.

Abstract This paper proposes a simplicity-oriented approach and framework for language-to-language transformation of, in particular, graphical languages. Key to simplicity is the decomposition of the transformation specification into sub-rule systems that separately specify purpose-specific aspects. We illustrate this approach by employing a variation of Plotkin’s Structural Operational Semantics (SOS) for pattern-based transformations of typed graphs in order to address the aspect ‘computation’ in a graph rewriting fashion. Key to our approach are two generalizations of Plotkin’s structural rules: the use of graph patterns as the matching concept in the rules, and the introduction of node and edge types. Types do not only allow one to easily distinguish between different kinds of dependencies, like control, data, and priority, but may also be used to define a hierarchical layering structure. The resulting Type-based Structural Operational Semantics (TSOS) supports a well-structured and intuitive specification and realization of semantically involved language-to-language transformations adequate for the generation of purpose-specific views or input formats for certain tools, like, e.g., model checkers. A comparison with the general-purpose transformation frameworks ATL and Groove, illustrates along the educational setting of our graphical WebStory language that TSOS provides quite a flexible format for the definition of a family of purpose-specific transformation languages that are easy to use and come with clear guarantees.

We present Pyro, a framework for enabling domain-specific modeling via the internet. Provided with an adequate metamodel specification, Pyro turns your browser into a collaborative, domain-specific, graphical development environment with features reminiscent of desktop IDEs for textual programming languages. The required metamodeling is supported in a high-level, simplicity-driven fashion, and the entire ready-to-run browser-based domain-specific development environment is generated fully automatically. We will illustrate the steps of this development along the realization of a graphical IDE for the Architecture Analysis and Design Language (AADL).

SUMMARY In this article, we present our experience with over a decade of strict simplicity orientation in the development and evolution of plug‐ins. The point of our approach is to enable our graphical modeling framework jABC to capture plug‐in development in a domain‐specific setting. The typically quite tedious and technical plug‐in development is shifted this way from a programming task to the modeling level, where it can be mastered also by application experts without programming expertise. We show how the classical plug‐in development profits from a systematic domain‐specific API design and how the level of abstraction achieved this way can be further enhanced by defining adequate building blocks for high‐level plug‐in modeling. As the resulting plug‐in models can be compiled and deployed automatically, our approach decomposes plug‐in development into three phases where only the realization phase requires plug‐in‐specific effort. By using our modeling framework jABC, this effort boils down to graphical, tool‐supported process modeling. Furthermore, we support the automatic completion of process sketches for executability. All this will be illustrated along the most recent plug‐in‐based evolution of the jABC framework, which witnessed quite some bootstrapping effects. Copyright © 2013 John Wiley & Sons, Ltd.

PROPHETS is our flexible framework for the synthesis of processes from libraries of basic services. In this paper we demonstrate how its synthesis strategy can be tailored to the considered application domain. For this purpose, PROPHETS provides a number of configuration options, such as different data exchange formats (e.g. shared variables and pipe lining) for the resulting process, as well as structural and temporal logic constraints for minimizing the inherent search space. We illustrate the impact of adequate synthesis tailoring by contrasting two real-life case studies with diametric characteristics.

One of the goals of FMICS, the ERCIM Working Group on Formal Methods for Industrial Critical Systems (FMICS) [8], is to transfer and promote the use formal methods technology in industry. The ongoing Verified Software Repository Grand Challenge [11] offers a great opportunity to reach this goal, resulting in a more robust and solid software industry in Europe. We demonstrate here the current status of the FMICS-jETIplatform1, a collaborative demonstrator based on the jETI technology2, that provides as repository a collection of verification tools stemming from the activities of the FMICS working group and facilities to orchestrate them in a remote and simple way. At the same time FMICS-jETI itself is a contribution to the VSR repository and thus to the Grand Challenge.