Search

This position paper on the (meta-)theory of Structural Operational Semantic (SOS) is motivated by the following two questions: (1) Is the (meta-)theory of SOS dying out as a research field? (2) If so, is it possible to rejuvenate this field with a redefined purpose? In this article, we will consider possible answers to those questions by first analysing the history of the EXPRESS/SOS workshops and the data concerning the authors and the presentations featured in the editions of those workshops as well as their subject matters. The results of our quantitative and qualitative analyses all indicate a diminishing interest in the theory of SOS as a field of research. Even though `all good things must come to an end', we strive to finish this position paper on an upbeat note by addressing our second motivating question with some optimism. To this end, we use our personal reflections and an analysis of recent trends in two of the flagship conferences in the field of Programming Languages (namely POPL and PDLI) to draw some conclusions on possible future directions that may rejuvenate research on the (meta-)theory of SOS. We hope that our musings will entice members of the research community to breathe new life into a field of research that has been kind to three of the authors of this article., Comment: In Proceedings EXPRESS/SOS2023, arXiv:2309.05788

Behavioral models enable the analysis of the functionality of software product lines (SPL), e.g., model checking and model-based testing. Model learning aims at constructing behavioral models for software systems in some form of a finite state machine. Due to the commonalities among the products of an SPL, it is possible to reuse the previously learned models during the model learning process. In this paper, an adaptive approach (the $\text{PL}^*$ method) for learning the product models of an SPL is presented based on the well-known $L^*$ algorithm. In this method, after model learning of each product, the sequences in the final observation table are stored in a repository which will be used to initialize the observation table of the remaining products to be learned. The proposed algorithm is evaluated on two open-source SPLs and the total learning cost is measured in terms of the number of rounds, the total number of resets and input symbols. The results show that for complex SPLs, the total learning cost for the $\text{PL}^*$ method is significantly lower than that of the non-adaptive learning method in terms of all three metrics. Furthermore, it is observed that the order in which the products are learned affects the efficiency of the $\text{PL}^*$ method. Based on this observation, we introduced a heuristic to determine an ordering which reduces the total cost of adaptive learning in both case studies., Comment: 12 pages, 10 figures, Paper accepted in the Research Track of the 26th ACM International Systems and Software Product Line Conference (SPLC 2022)

As autonomous systems (AS) increasingly become part of our daily lives, ensuring their trustworthiness is crucial. In order to demonstrate the trustworthiness of an AS, we first need to specify what is required for an AS to be considered trustworthy. This roadmap paper identifies key challenges for specifying for trustworthiness in AS, as identified during the "Specifying for Trustworthiness" workshop held as part of the UK Research and Innovation (UKRI) Trustworthy Autonomous Systems (TAS) programme. We look across a range of AS domains with consideration of the resilience, trust, functionality, verifiability, security, and governance and regulation of AS and identify some of the key specification challenges in these domains. We then highlight the intellectual challenges that are involved with specifying for trustworthiness in AS that cut across domains and are exacerbated by the inherent uncertainty involved with the environments in which AS need to operate., Comment: Accepted version of paper. 13 pages, 1 table, 1 figure

Behavioral models are the key enablers for behavioral analysis of Software Product Lines (SPL), including testing and model checking. Active model learning comes to the rescue when family behavioral models are non-existent or outdated. A key challenge on active model learning is to detect commonalities and variability efficiently and combine them into concise family models. Benchmarks and their associated metrics will play a key role in shaping the research agenda in this promising field and provide an effective means for comparing and identifying relative strengths and weaknesses in the forthcoming techniques. In this challenge, we seek benchmarks to evaluate the efficiency (e.g., learning time and memory footprint) and effectiveness (e.g., conciseness and accuracy of family models) of active model learning methods in the software product line context. These benchmark sets must contain the structural and behavioral variability models of at least one SPL. Each SPL in a benchmark must contain products that requires more than one round of model learning with respect to the basic active learning $L^{*}$ algorithm. Alternatively, tools supporting the synthesis of artificial benchmark models are also welcome., Comment: 5 pages, 3 figures, Paper accepted in the Challenge Cases Track of the 26th ACM International Systems and Software Product Line Conference (SPLC 2022)

We present a novel and generalised notion of doping cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. As a formal basis for monitoring conformance-based cleanness, we develop the temporal logic HyperSTL*, an extension of Signal Temporal Logics with trace quantifiers and a freeze operator. We show that our generalised definitions are essential in a data-driven method for doping detection and apply our definitions to a case study concerning diesel emission tests.

Several notions of conformance have been proposed for checking the behavior of cyber-physical systems against their hybrid systems models. In this paper, we explore the initial idea of a notion of approximate conformance that allows for comparison of both observable discrete actions and (sampled) continuous trajectories. As such, this notion will consolidate two earlier notions, namely the notion of Hybrid Input-Output Conformance (HIOCO) by M. van Osch and the notion of Hybrid Conformance by H. Abbas and G.E. Fainekos. We prove that our proposed notion of conformance satisfies a semi-transitivity property, which makes it suitable for a step-wise proof of conformance or refinement., Comment: In Proceedings V2CPS-16, arXiv:1612.04023

In this paper we introduce a notion of counterfactual causality in the Halpern and Pearl sense that is compositional with respect to the interleaving of transition systems. The formal framework for reasoning on what caused the violation of a safety property is established in the context of labeled transition systems and Hennessy Milner logic. The compositionality results are devised for non-communicating systems., Comment: In Proceedings CREST 2016, arXiv:1608.07398

A major challenge in testing software product lines is efficiency. In particular, testing a product line should take less effort than testing each and every product individually. We address this issue in the context of input-output conformance testing, which is a formal theory of model-based testing. We extend the notion of conformance testing on input-output featured transition systems with the novel concept of spinal test suites. We show how this concept dispenses with retesting the common behavior among different, but similar, products of a software product line., Comment: In Proceedings MBT 2014, arXiv:1403.7044

There exists a rich literature of rule formats guaranteeing different algebraic properties for formalisms with a Structural Operational Semantics. Moreover, there exist a few approaches for automatically deriving axiomatizations characterizing strong bisimilarity of processes. To our knowledge, this literature has never been extended to the setting with data (e.g. to model storage and memory). We show how the rule formats for algebraic properties can be exploited in a generic manner in the setting with data. Moreover, we introduce a new approach for deriving sound and ground-complete axiom schemata for a notion of bisimilarity with data, called stateless bisimilarity, based on intuitive auxiliary function symbols for handling the store component. We do restrict, however, the axiomatization to the setting where the store component is only given in terms of constants., Comment: In Proceedings EXPRESS/SOS 2013, arXiv:1307.6903

We study the problem of deriving a specification for a third-party component, based on the specification of the system and the environment in which the component is supposed to reside. Particularly, we are interested in using component specifications for conformance testing of black-box components, using the theory of input-output conformance (ioco) testing. We propose and prove sufficient criteria for decompositionality, i.e., that components conforming to the derived specification will always compose to produce a correct system with respect to the system specification. We also study the criteria for strong decomposability, by which we can ensure that only those components conforming to the derived specification can lead to a correct system., Comment: In Proceedings MBT 2013, arXiv:1303.0379

Process algebra provides abstract and rigorous means for studying communicating concurrent systems. Coordination languages also provide abstract means for the specifying and programming communication of components. Hence, the two fields seem to have very much in common and the link between these two research areas have been established formally by means of several translations, mainly from coordination languages to process algebras. There have also been proposals of process algebras whose communication policy is inspired by the one underlying coordination languages. The aim of this workshop was to push the state of the art in the study of the connections between process algebra and coordination languages by bringing together experts as well as young researchers from the two fields to communicate their ideas and findings. It includes both contributed and invited papers that have been presented during the one day meeting on Process Algebra and Coordination (PACO 2011) which took place on June 9, 2011 in Reykjavik, Iceland.

Computation nowadays is becoming inherently concurrent, either because of characteristics of the hardware (with multicore processors becoming omnipresent) or due to the ubiquitous presence of distributed systems (incarnated in the Internet). Computational systems are therefore typically distributed, concurrent, mobile, and often involve composition of heterogeneous components. To specify and reason about such systems and go beyond the functional correctness proofs, e.g., by supporting reusability and improving maintainability, approaches such as coordination languages and software architecture are recognised as fundamental. The goal of the this workshop is to put together researchers and practitioners of the aforementioned fields, to share and identify common problems, and to devise general solutions in the context of coordination languages and software architectures., Comment: EPTCS 58, 2011