603

A common phenomenon in software development is that as a system is being built and incremented with new features, certain quality aspects of the system begin to deteriorate. Therefore, it is important to be able to accurately analyze and determine the quality implications of each change and increment to a system. To address this topic, the multinational SmartDelta project develops automated solutions for quality assessment of product deltas in a continuous engineering environment. The project will provide smart analytics from development artifacts and system executions, offering insights into quality degradation or improvements across different product versions, and providing recommendations for next builds.

Abstract A computational system is called autonomous if it is able to make its own decisions, or take its own actions, without human supervision or control. The capability and spread of such systems have reached the point where they are beginning to touch much of everyday life. However, regulators grapple with how to deal with autonomous systems, for example how could we certify an Unmanned Aerial System for autonomous use in civilian airspace? We here analyse what is needed in order to provide verified reliable behaviour of an autonomous system, analyse what can be done as the state-of-the-art in automated verification, and propose a roadmap towards developing regulatory guidelines, including articulating challenges to researchers, to engineers, and to regulators. Case studies in seven distinct domains illustrate the article.

This special issue contains articles selected from CS&P 2018, the 27th Workshop on Concurrency, Specification, and Programming.CS&P deals with formal specification of concurrent and parallel systems, mathematical models for describing such systems, and programming and verification concepts for their implementation.The workshop is one of a series of events organised every even year by Humboldt University of Berlin and every odd year by Warsaw University.Dating back to the midseventies, CS&P has become an important forum for researchers from European and Asian countries.CS&P 2018 was held at Humboldt University Berlin-Adlershof, Germany, in September 24-26, 2018, and featured 20 papers accepted for presentation by the program committee.After the conference, six outstanding papers were selected by the Steering Committee based on the previous reviews and the quality of the presentations.Their authors were given time to integrate the reviewer's and audience's feedback, as well as to substantially improve and extend their contributions.After the second round of reviewing by additional experts, during the pandemic year of 2020 the authors polished and finalized their contributions, to yield the mature articles which can be found in this special issue.

This special issue of Fundamenta Informaticae is dedicated to papers selected from the 26 th International Workshop on CONCURRENCY, SPECIFICATION, AND PROGRAMMING (CS&P 2017), which took place in Warsaw, Poland, in

Runtime verification is a lightweight formal method that checks whether an execution of a system satisfies a given property. A challenge in building a runtime verification system is to define a suitable monitoring specification language, i.e., a language that is expressive, of reasonable complexity, and easy to understand. In this paper, we extend live sequence charts (LSCs, [1]) for the specification of properties in systems monitoring. We define Parametrized extended LSCs (PeLSCs) by introducing the notions of necessary prechart, concatenation, and condition- and assignment-structure. With these PeLSCs, necessary and sufficient conditions of certain observations, and parametric properties can be specified in an intuitive way. We prove some results about the expressiveness of extended LSCs. In particular, we show that LSCs with necessary precharts are strictly more expressive than standard LSCs, and that iteration-free extended LSCs have the same expressive power as linear temporal logic (LTL). To generate monitors, we develop translations of PeLSCs into hybrid logic. We show that the complexity of the word problem of PeLSCs is linear with respect to the length of input traces, thus our formalism is well-suited for online monitoring of communicating systems.

Testing is one of the most important quality assurance techniques for software. Automating the test design allows for automatically creating test suites from high-level system descriptions or test descriptions. Furthermore, it enables testers to automatically adapt the test suites to potentially recently changed descriptions. In model-based testing, models are used to automatically create test cases. Case studies report of an effort reduction in test design between 20 and 85 percent. In this paper, we report on a pilot project for introducing model-based testing in an industrial context. For such a pilot project, it is necessary to adapt the existing workflows and tool chains, to train the staff, and to adapt the assets of the company. The goal is to show the full applicability of the technique at the customer site. We present the evaluations, the lessons learned, and compare the efforts of model-based and manual test design for this example. This paper is not 'generally valid' in the sense that the results are reproducible for other projects and domains. Instead, our intention is to provide guidance for setting up similar evaluations.

We address the question of how to select test cases in a controlled model-based software product line development process. CVL, the common variability language, provides a framework for materialization of product models from a given variability model and resolution model. Reflecting common practice, we assume that test case development for product line is independent from product development. In such a setting, the question arises which test cases can be applied to which products. To this end, we describe a procedure and tool set for assigning the outcome of a test case on an arbitrary member of a software product line using UML base and CVL variability models. As a case study, we demonstrate our approach with the example of a product line of automatic espresso machines.

In this paper, we deal with coverage criteria for boundary testing. We focus on the automatic generation of boundary tests based on OCL expressions and evaluate the quality of these tests with established coverage criteria like MC/DC. We define and apply new coverage criteria, evaluate their efficiency via mutation testing, and substantiate all explanations by an example, part of a model of an elevator control.

In this paper, we develop a testing theory for specification-based software product line development. Starting with a framework for the evaluation of test cases with respect to formal specifications, we develop a notion of enhancement, which allows to re-use test cases in a horizontal systems development process. In such a process, more and more features are added to an existing software product. For specification-based testing, this means that the corresponding specifications are enhanced more and more, and that new test cases must be added to an existing test suite in order to test the additional features. We formally define an enhancement relation between Csp-CASL specifications, describe a test evaluation method for software product lines based on Csp-CASL specifications, and prove several preservation results which allow to re-use test cases in a horizontal development. We illustrate our approach with the example of a product line of remote control units for consumer products.

The development of reliable systems is still a major challenge for software industry. Construction of such a system requires both process and product based quality assurance. Many process improvement models have been suggested in industry and found appropriate for achieving high quality products. Examples of such process improvement models are CMM/CMMI, Agile, SPICE, the ISO 9000 family etc. However, implementation of these process improvement models often adds significant extra efforts. To minimize process implementation costs we propose a formal specification based product development model which integrates product and process quality. Formal specification methods have been in practice since decades, and have been successful in the development of safety-critical systems. Some formal methods are VDM, Z, LOTOS, CSP and CASL. In particular, we investigate the compliance of CMMI process area with the formal specification language CSP-CASL. CMMI is based on the notion of process area, which is a cluster of best practices with particular goals in a certain area. For each of the relevant process areas, we show how formal specifications can contribute to achieve the specific goals of that process area. This integration is a new result for achieving process compliance parallel with product development. We demonstrate our approach with an industrial case study.

In this paper, we present a theory for the evaluation of test cases with respect to formal specifications. In particular, we use the specification language CSP-CASL to define and evaluate black-box tests for reactive systems. Using loose semantics and three-valued test oracles, our approach is well-suited to deal with the refinement of specifications. In a structured development process of computational systems, abstract specifications are gradually refined into more concrete ones. With our approach, it is possible to develop test cases already from very abstract and basic specifications, and to reuse them later on in more refined systems.

We investigate expressivity and complexity of hybrid logics on linear structures. Hybrid logics are an enrichment of modal logics with certain first-order features which are algorithmically well behaved. Therefore, they are well suited for the specification of certain properties of computational systems. We show that hybrid logics are more expressive than usual modal and temporal logics on linear structures, and exhibit a hierarchy of hybrid languages. We determine the complexities of the satisfiability problem for these languages and define an existential fragment of hybrid logic for which satisfiability is still NP-complete. Finally, we examine the linear time model checking problem for hybrid logics and its complexity.

Conformance has been used as a correctness criterion for asynchronous circuits. In the case of untimed systems, conformance of an implementation to a specification is equivalent to the failure-freeness between the implementation and the mirror of the specification. For bounded-delay systems, in general this property does not hold. In this paper, we define various notions of failures and examine whether the above property holds or not. We then discuss an alternative and effective algorithm for conformance checking of bounded-delay asynchronous circuits.

This paper reports on a case study in the quantitative analysis of safety-critical systems. Although formal methods are becoming more and more accepted in the development of such systems, usually they are used in the verification of qualitative properties. However, in many cases system safety also depends on the fact that certain quantitative requirements are met. Therefore we are interested in statements about quantitative properties, which can be achieved by a rigorous formal method. Our approach is to create a generalized stochastic Petri net (GSPN) model of the system and use it for the analysis of the system. The object of this case study is a fault-tolerant computer (FTC) constructed by Daimler Benz Aerospace (DASA) for the International Space Station (ISS). One part of the FTC is the Avionics Interface (AVI) which connects the FTC with a bus-system. We want to determine the data throughput that can be reached by the AVI and obtain informations about bus-usage-profiles which can cause the rejection of messages. Although such rejections are allowed according to the specification, they can cause a significant deterioration in the overall bus performance. In this article we describe a GSPN model of the AVI software and its environment. This model is used to make predictions about the AVI performability. Since a complete analytical solution of the model is not possible due to its complexity and the infinite state space, a simulation is used to analyse the crucial AVI behavior for several bus-usage-profiles.