Grammars can serve as producers for structured test inputs that are syntactically correct by construction. A probabilistic grammar assigns probabilities to individual productions, thus controlling the distribution of input elements. Using the grammars as input parsers, we show how to leant input distributions from input samples, allowing to create inputs that are similar to the sample; by inverting the probabilities, we can create inputs that are dissimilar to the sample. This allows for three test generation strategies: 1) "Common inputs"-by learning from common inputs, we can create inputs that are similar to the sample; this is useful for regression testing. 2) "Uncommon inputs"-learning from common inputs and inverting probabilities yields inputs that are strongly dissimilar to the sample; this is useful for completing a test suite with "inputs from hell" that test uncommon features, yet are syntactically valid. 3) "Failure-inducing inputs"-learning from inputs that caused failures in the past gives us inputs that share similar features and thus also have a high chance of triggering bugs; this is useful for testing the completeness of fixes. Our evaluation on three common input formats (JSON, JavaScript, CSS) shows the effectiveness of these approaches. Results show that "common inputs" reproduced 96 percent of the methods induced by the samples. In contrast, for almost all subjects (95 percent), the "uncommon inputs" covered significantly different methods from the samples. Learning from failure-inducing samples reproduced all exceptions (100 percent) triggered by the failure-inducing samples and discovered new exceptions not found in any of the samples learned from.

In this article, we introduce a probabilistic verification algorithm for stochastic regular expressions over a probabilistic extension of the Action based Computation Tree Logic (ACTL*). The main results include a novel model checking algorithm and a semantics on the probabilistic action logic for stochastic regular expressions (SREs). Specific to our model checking algorithm is that SREs are defined via local probabilistic functions. Such functions are beneficial since they enable to verify properties locally for sub-components. This ability provides a flexibility to reuse the local results for the global verification of the system; hence, the framework can be used for iterative verification. We demonstrate how to model a system with an SRE and how to verify it with the probabilistic action based logic and present a preliminary performance evaluation with respect to the execution time of the reachability algorithm.

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.

Generating structured input files to test programs can be performed by techniques that produce them from a grammar that serves as the specification for syntactically correct input files. Two interesting scenarios then arise for effective testing. In the first scenario, software engineers would like to generate inputs that are as similar as possible to the inputs in common usage of the program, to test the reliability of the program. More interesting is the second scenario where inputs should be as dissimilar as possible from normal usage. This is useful for robustness testing and exploring yet uncovered behavior. To provide test cases for both scenarios, we leverage a context-free grammar to parse a set of sample input files that represent the program's common usage, and determine probabilities for individual grammar production as they occur during parsing the inputs. Replicating these probabilities during grammar-based test input generation, we obtain inputs that are close to the samples. Inverting these probabilities yields inputs that are strongly dissimilar to common inputs, yet still valid with respect to the grammar. Our evaluation on three common input formats (JSON, JavaScript, CSS) shows the effectiveness of these approaches in obtaining instances from both sets of inputs.

In this work, we present a tool that systematically discovers and tests the user-observable states of an Android application. We define an appropriate notion of test coverage, and we show the tool's potential by applying it to several publicly available applications.

Model-based reliability estimation of systems can provide useful insights early in the development process. However, computational complexity of estimating metrics such as mean time to first failure (MTTFF), turnaround time (TAT), or other domain-based quantitative measures can be prohibitive both in time, space, and precision. In this article, we present an alternative to exhaustive model exploration, as in probabilistic model checking, and partial random exploration, as in statistical model checking. Our hypothesis is that a (carefully crafted) partial systematic exploration of a system model can provide better bounds for these quantitative model metrics at lower computation cost. We present a novel automated technique for metric estimation that combines simulation, invariant inference, and probabilistic model checking. Simulation produces a probabilistically relevant set of traces from which a state invariant is inferred. The invariant characterises a partial model, which is then exhaustively explored using probabilistic model checking. We report on experiments that suggest that metric estimation using this technique (for both fully probabilistic models and those exhibiting nondeterminism) can be more effective than (full-model) probabilistic and statistical model checking, especially for system models for which the events of interest are rare.

Model-based reliability estimation of systems can provide useful insights early in the development process. However, computational complexity of estimating metrics such as mean time to first failure (MTTFF), turnaround time (TAT), or other domain-based quantitative measures can be prohibitive both in time, space, and precision. In this article, we present an alternative to exhaustive model exploration, as in probabilistic model checking, and partial random exploration, as in statistical model checking. Our hypothesis is that a (carefully crafted) partial systematic exploration of a system model can provide better bounds for these quantitative model metrics at lower computation cost. We present a novel automated technique for metric estimation that combines simulation, invariant inference, and probabilistic model checking. Simulation produces a probabilistically relevant set of traces from which a state invariant is inferred. The invariant characterises a partial model, which is then exhaustively explored using probabilistic model checking. We report on experiments that suggest that metric estimation using this technique (for both fully probabilistic models and those exhibiting nondeterminism) can be more effective than (full-model) probabilistic and statistical model checking, especially for system models for which the events of interest are rare.

Model-based reliability estimation of systems can provide useful insights early in the development process. However, computational complexity of estimating metrics such as mean time to first failure (MTTFF), turnaround time (TAT), or other domain-based quantitative measures can be prohibitive both in time, space, and precision. In this article, we present an alternative to exhaustive model exploration, as in probabilistic model checking, and partial random exploration, as in statistical model checking. Our hypothesis is that a (carefully crafted) partial systematic exploration of a system model can provide better bounds for these quantitative model metrics at lower computation cost. We present a novel automated technique for metric estimation that combines simulation, invariant inference, and probabilistic model checking. Simulation produces a probabilistically relevant set of traces from which a state invariant is inferred. The invariant characterises a partial model, which is then exhaustively explored using probabilistic model checking. We report on experiments that suggest that metric estimation using this technique (for both fully probabilistic models and those exhibiting nondeterminism) can be more effective than (full-model) probabilistic and statistical model checking, especially for system models for which the events of interest are rare.

System specifications have long been expressed through automata-based languages, which allow for compositional construction of complex models and enable automated verification techniques such as model checking. Automata-based verification has been extensively used in the analysis of systems, where they are able to provide yes/no answers to queries regarding their temporal properties. Probabilistic modelling and checking aim at enriching this binary, qualitative information with quantitative information, more suitable to approaches such as reliability engineering. Compositional construction of software specifications reduces the specification effort, allowing the engineer to focus on specifying individual component behaviour to then analyse the composite system behaviour. Compositional construction also reduces the validation effort, since the validity of the composite specification should be dependent on the validity of the components. These component models are smaller and thus easier to validate. Compositional construction poses additional challenges in a probabilistic setting. Numerical annotations of probabilistically independent events must be contrasted against estimations or measurements, taking care of not compounding this quantification with exogenous factors, in particular the behaviour of other system components. Thus, the validity of compositionally constructed system specifications requires that the validated probabilistic behaviour of each component continues to be preserved in the composite system. However, existing probabilistic automata-based formalisms do not support specification of non-deterministic and probabilistic component behaviour which, when observed through logics such as pCTL, is preserved in the composite system. In this paper we present a probabilistic extension to Interface Automata which preserves pCTL properties under probabilistic fairness by ensuring a probabilistic branching simulation between component and composite automata. The extension not only supports probabilistic behaviour but also allows for weaker prerequisites to interfacing composition, that supports delayed synchronisation that may be required because of internal component behaviour. These results are equally applicable as an extension to non-probabilistic Interface Automata.

Model-based reliability estimation of software systems can provide useful insights early in the development process. However, computational complexity of estimating reliability metrics such as mean time to first failure (MTTF) can be prohibitive both in time, space and precision. In this paper we present an alternative to exhaustive model exploration-as in probabilistic model checking-and partial random exploration-as in statistical model checking. Our hypothesis is that a (carefully crafted) partial systematic exploration of a system model can provide better bounds for reliability metrics at lower computation cost. We present a novel automated technique for reliability estimation that combines simulation, invariant inference and probabilistic model checking. Simulation produces a probabilistically relevant set of traces from which a state invariant is inferred. The invariant characterises a partial model which is then exhaustively explored using probabilistic model checking. We report on experiments that suggest that reliability estimation using this technique can be more effective than (full model) probabilistic and statistical model checking for system models with rare failures.

Clock Difference Diagrams (CDDs), BDD-like data struc- tures for model checking of timed automata, were presented as alterna- tives for classic DBM representation. However, work on them seems to have stopped, although there are still important open questions. CDD definition required that repeated subtrees were aliased, but no clear algo- rithm was presented for producing such compact representation, which seems costly to achieve. In this article we describe our implementation of such aliased subtrees and revisit CDDs by comparing their perfor- mance against DBMs on current case studies, with and without repeated subtrees. Our experiments show that CDDs still require more time and memory than DBMs, suggesting that eliminating repetitions is still not enough. Thus, this article re-opens issues that previous work on the topic considered closed.

System specifications have long been expressed through automata based languages, enabling verification techniques such as model checking. These verification techniques can assess whether a property holds or not, given a system specification. However, model checking techniques suffer from the traditionally called state explosion problem, that is, models which are useful for analysis grow exponentially in size when verifying their concurrent behaviour. This state explosion problem is a serious limitation of model checking techniques, often making the application of tools that apply them infeasible, and limiting techniques to only a partial exploration of the complete state space. In this work we propose a novel approach that could help gather useful, quantified domain-related information from such incomplete explorations, leveraging on the concept of probabilistic behaviour models of the environment, for supporting dependability cases.

System specifications have long been expressed through automata based languages, enabling verification techniques such as model checking. These verification techniques can assess whether a property holds or not, given a system specification. However, model checking techniques suffer from the traditionally called state explosion problem, that is, models which are useful for analysis grow exponentially in size when verifying their concurrent behaviour. This state explosion problem is a serious limitation of model checking techniques, often making the application of tools that apply them infeasible, and limiting techniques to only a partial exploration of the complete state space. In this work we propose a novel approach that could help gather useful, quantified domain-related information from such incomplete explorations, leveraging on the concept of probabilistic behaviour models of the environment, for supporting dependability cases.

System specifications have long been expressed through automata-based languages, enabling verification techniques such as model checking. These verification techniques can assess whether a property holds or not, given a system specification. Quantitative model checking can provide additional information on the probability of these properties holding. We are interested in quantitatively analysing the probability of errors in non-probabilistic system models by composing them with probabilistic models of the environment. Although many probabilistic automata-based formalisms and composition operators exist, these are not adequate for such a setting. In this work we present a formalism inspired on interface automata and a suitable composition operator for these automata that enables validation of environment models in isolation and sound analysis of its composition with the non-probabilistic model of the system-under-analysis.

Clock Di erence Diagrams (CDDs), a BDD-like data structure for model checking of timed automata, were presented in 1999. After the original article the work on them seems to have stopped, although there are still important open questions. The proposed algorithm relied on the traditionally used data structure (DBMs) for most operations. CDDs de nition required that repeated subtrees were aliased, but no clear algorithm was presented for producing such compact representation, which seems costly to achieve. Also, since then, case studies have increased in size. In this article we revisit CDDs by introducing RCDDs, a variation that does not require maximum aliasing. We present the complete set of operations required to perform forward reachability analysis with no need for DBMs. By employing a fully RCDD-based algorithm our experiments show a consistent reduction of time requirements in case studies from the current literature, sometimes up to more than 40%.