The security of satellites has become critical in recent years due to their important role in modern society. However, numerous challenges, including limited computing resources, evolving cyber threats, and the isolated nature of satellites, hinder the development of effective security solutions. Different solutions should be implemented and combined to protect space assets: encryption, access control, zero-trust architecture, etc. This vision presents the challenges and aspects to consider for implementing an Intrusion Detection System (IDS) tailored to improve the security of satellite systems. Our approach uses a multi-level structure to define rule-based and machine-learning security approaches that address the challenges associated with different mission types. By strategically placing IDS components and considering the trade-offs of each location, we improve detection reliability. Additionally, we present an ontology-based method for visualizing the IDS configuration, which provides clear insight into system capabilities, enhances situational awareness, and facilitates identification and response to potential threats. We also provide strategies for updating the IDS while maintaining efficiency and security. This vision helps improve the cybersecurity measures of satellite operations and increase their resilience to cyberattacks.

Internet service providers (ISPs) strive to provide the best possible services to their customers. Service outages, or incidents, due to technical failures are inevitable, so the aim of ISPs must be to respond as quickly as possible to error notifications. However, services may rely on thousands of devices and components that are interconnected and managed by different teams (network administrators, technicians, etc.). Identifying the team to which an incident ticket should be assigned becomes a tedious task that slows down recovery time.In this paper we focus on the problem of finding the right team when an incident occurs. We group teams into logical team groups and use machine learning models that we train on previous resolved incidents to predict the most appropriate team group from a failure description. Using a large dataset from a national ISP and telecommunication company, we demonstrate that, even with a small amount of information available at the beginning of the incident, machine learning models can achieve an accuracy of 88.52% and an F1 score of 90.17%. With more complete information about the incident, the accuracy and F1 score increase to 90.52% and 91.7%.

Mission planning for multi-agent autonomous systems aims to generate feasible and optimal mission plans that satisfy given requirements. In this article, we propose a tool-supported mission-planning methodology that combines (i) a path-planning algorithm for synthesizing path plans that are safe in environments with complex road conditions, and (ii) a task-scheduling method for synthesizing task plans that schedule the tasks in the right and fastest order, taking into account the planned paths. The task-scheduling method is based on model checking, which provides means of automatically generating task execution orders that satisfy the requirements and ensure the correctness and efficiency of the plans by construction. We implement our approach in a tool named MALTA, which offers a user-friendly GUI for configuring mission requirements, a module for path planning, an integration with the model checker UPPAAL, and functions for automatic generation of formal models, and parsing of the execution traces of models. Experiments with the tool demonstrate its applicability and performance in various configurations of an industrial case study of an autonomous quarry. We also show the adaptability of our tool by employing it in a special case of an industrial case study.

Owing to the pervasiveness of software in our modern lives, software systems have evolved to be highly configurable. Combinatorial testing has emerged as a dominant paradigm for testing highly configurable systems. Often constraints are employed to define the environments where a given system is expected to work. Therefore, there has been a sustained interest in designing constraint-based test suite generation techniques. A significant goal of test suite generation techniques is to achieve$t$-wise coverage for higher values of$t$. Therefore, designing scalable techniques that can estimate$t$-wise coverage for a given set of tests and/or the estimation of maximum achievable$t$-wise coverage under a given set of constraints is of crucial importance. The existing estimation techniques face significant scalability hurdles. We designed scalable algorithms with mathematical guarantees to estimate (i)$t$-wise coverage for a given set of tests, and (ii) maximum$t$-wise coverage for a given set of constraints. In particular,$\mathsf{ApproxCov}$takes in a test set$\mathcal{U}$and returns an estimate of the$t$-wise coverage of$\mathcal{U}$that is guaranteed to be within$(1\pm\varepsilon)$-factor of the ground truth with probability at least$1-\delta$for a given tolerance parameter$\varepsilon$and a confidence parameter$\delta$. A scalable framework${\mathsf{ApproxMaxCov}}$for a given formula${\mathsf{F}}$outputs an approximation which is guaranteed to be within$(1\pm\varepsilon)$factor of the maximum achievable$t$-wise coverage under${\mathsf{F}}$, with probability$\geq 1-\delta$for a given tolerance parameter$\varepsilon$and a confidence parameter$\delta$. Our comprehensive evaluation demonstrates that$\mathsf{ApproxCov}$and${\mathsf{ApproxMaxCov}}$can handle benchmarks that are beyond the reach of current state-of-the-art approaches. In this paper we present proofs of correctness of$\mathsf{ApproxCov}$,${\mathsf{ApproxMaxCov}}$, and of their generalizations. We show how the algorithms can improve the scalability of a test suite generator while maintaining its effectiveness. In addition, we compare several test suite generators on different feature combination sizes$t$.

An efficient machine learning model for malware detection requires a large dataset to train. Yet it is not easy to collect such a large dataset without violating or leaving vulnerable to potential violation various aspects of data privacy. Our work proposes a federated learning framework that permits multiple parties to collaborate on learning behavioral graphs for malware detection. Our proposed graph classification framework allows the participating parties to freely decide their preferred classifier model without acknowledging their preferences to the others involved. This mitigates the chance of any data poisoning attacks. In our experiments, our classification model using the partially federated learning achieved the F1-score of 0.97, close to the performance of the centralized data training models. Moreover, the impact of the label flipping attack against our model is less than 0.02.

Rule-based expert systems (RBES) use knowledge about a specific topic, represented as rules, in order to solve particular problems that would otherwise require a human expert.The creation and maintenance of the rule sets used come with several challenges in order to guarantee that they remain free of any error, which could reduce performances or lead to erroneous results.In this paper, we present a methodology to provide an automated assistance for domain experts creating and maintaining rules for RBES.This assistance takes the form of automated detection of relationships between rules that can lead to redundancies or conflicts.By reducing the weight borne by the human experts in the verification of the rules, it reduces the chance of errors, which helps increase the relevance of the rule set.To complete the theoretical methodology, we have implemented a functional prototype allowing for the management of a rule set and the visual highlight of redundancies and potential conflicts.Our approach, developed in the context of a case study, can be used for rules in any domain as long as they can be described in the same format.The approach can also be extended or modified to account for other types of relationships between rules.Index Terms-rule-based expert system, rule set

We propose mutation model checking as an approach to strengthen formal specifications used for model checking. Inspired by mutation testing, our approach concludes that specifications are not strong enough if they fail to detect faults in purposely mutated models. Our preliminary experiments on two case studies confirm the relevance of the problem: their specification can only detect 40% and 60% of randomly generated mutants. As a result, we propose a framework to strengthen the original specification, such that the original model satisfies the strengthened specification but the mutants do not.

The manual methods to create detection rules are no longer practical in the anti-malware product since the number of malware threats has been growing over past years. Thus, the turn to machine learning approaches is a promising way to make malware recognition more efficient. The traditional centralized machine learning requires a large amount of data to train a model with excellent performance. To boost the malware detection, the training data might be on various kind of data sources such as data on the host, network, and cloud-based anti-malware components, or even, data from different enterprises. To avoid the expenses of data collection as well as the leakage of private data, we present a federated learning system to identify malware through behavioral graphs, i.e., system call dependency graphs. It is based on a deep learning model including a graph autoencoder and a multiclass classifier module. This model is trained by a secure learning protocol among clients to preserve the private data against inference attacks. Using the model to identify malware, we achieve the accuracy of for homogeneous graph data and for inhomogeneous graph data.

Owing to the pervasiveness of software in our modern lives, software systems have evolved to be highly configurable. Combinatorial testing has emerged as a dominant paradigm for testing highly configurable systems. Often constraints are employed to define the environments where a given system under test (SUT) is expected to work. Therefore, there has been a sustained interest in designing constraint-based test suite generation techniques. A significant goal of test suite generation techniques is to achieve t-wise coverage for higher values of t. Therefore, designing scalable techniques that can estimate t-wise coverage for a given set of tests and/or the estimation of maximum achievable t-wise coverage under a given set of constraints is of crucial importance. The existing estimation techniques face significant scalability hurdles.

Abstract We propose a simulation-based approach to verify Variability-Intensive Systems (VISs) with stochastic behaviour. Given an LTL formula and a model of the VIS behaviour, our method estimates the probability for each variant to satisfy the formula. This allows us to learn the products of the VIS for which the probability stands above a certain threshold. To achieve this, our method samples VIS executions from all variants at once and keeps track of the occurrence probability of these executions in any given variant. The efficiency of this algorithm relies on Algebraic Decision Diagram (ADD), a dedicated data structure that enables orthogonal treatment of variability, stochasticity and property satisfaction. We implemented our approach as an extension of the ProVeLines model checker. Our experiments validate that our method can produce accurate estimations of the probability for the variants to satisfy the given properties.

Abstract Model-based mutation testing has the potential to effectively drive test generation to reveal faults in software systems. However, it faces a typical efficiency issue since it could produce many mutants that are equivalent to the original system model, making it impossible to generate test cases from them. We consider this problem when model-based mutation testing is applied to real-time system product lines, represented as timed automata. We define novel, time-specific mutation operators and formulate the equivalent mutant problem in the frame of timed refinement relations. Further, we study in which cases a mutation yields an equivalent mutant. Our theoretical results provide guidance to system engineers, allowing them to eliminate mutations from which no test case can be produced. Our empirical evaluation, based on a proof-of-concept implementation and a set of benchmarks from the literature, confirms the validity of our theory and demonstrates that in general our approach can avoid the generation of a significant amount of the equivalent mutants.

The concept of decomposition in computer science and engineering is considered a fundamental component of computational thinking and is prevalent in design of algorithms, software construction, hardware design, and more. We propose a simple and natural formalization of sequential decomposition, in which a task is decomposed into two sequential sub-tasks, with the first sub-task to be executed before the second sub-task is executed. These tasks are specified by means of input/output relations. We define and study decomposition problems, which is to decide whether a given specification can be sequentially decomposed. Our main result is that decomposition itself is a difficult computational problem. More specifically, we study decomposition problems in three settings: where the input task is specified explicitly, by means of Boolean circuits, and by means of automatic relations. We show that in the first setting decomposition is NP-complete, in the second setting it is NEXPTIME-complete, and in the third setting there is evidence to suggest that it is undecidable. Our results indicate that the intuitive idea of decomposition as a system-design approach requires further investigation. In particular, we show that adding a human to the loop by asking for a decomposition hint lowers the complexity of decomposition problems considerably.

Smart homes are IoT systems enabling the automation of household operation. The unrestricted collection and processing of data by smart home systems raises legitimate privacy concerns for their users. Over the past decade, there has been significant interest in privacy-enhancing technologies applied at the level of a local smart hub physically located in the home and acting as a gateway between sensors, applications, platform providers, and services in the cloud. The number and variety of projects and research proposals can, however, make their comparison a daunting and unnecessarily complex task. We systematize existing knowledge in this field through the analysis and categorization of 10 industrial and community-contributed systems and 37 research proposals from the literature of the past 11 years. Our results shed light on the diversity of system and trust models considered in the state-of-the-art and on the associated privacy-enhancing technologies. We further identify open research problems and promising approaches that would benefit the smart home hub model and the protection of smart home users’ privacy.

Abstract Shift2Rail is a joint undertaking funded by the EU via its Horizon 2020 program and by main railway stakeholders. Several Shift2Rail projects aim to investigate the application of formal methods to new ERTMS/ETCS railway signalling systems that promise to move European railway forward by guaranteeing high capacity, low cost and improved reliability. We explore the ERTMS/ETCS level 3 full moving block specifications stemming from different Shift2Rail projects using Uppaal and statistical model checking. The results range from novel rigorously formalised requirements to an operational model formally verified against scenarios with multiple trains on a single railway line. From the gained experience, we have distilled future research goals to improve the formal specification and verification of real-time systems, and we discuss some barriers concerning a possible uptake of formal methods and tools in the railway industry.

Abstract Lifted (family-based) static analysis by abstract interpretation is capable of analyzing all variants of a program family simultaneously, in a single run without generating any of the variants explicitly. The elements of the underlying lifted analysis domain are tuples, which maintain one property per variant. Still, explicit property enumeration in tuples, one by one for all variants, immediately yields combinatorial explosion. This is particularly apparent in the case of program families that, apart from Boolean features, contain also numerical features with large domains, thus giving rise to astronomical configuration spaces. The key for an efficient lifted analysis is a proper handling of variability-specific constructs of the language (e.g., feature-based runtime tests and $$\texttt {\#if}$$ # if directives). In this work, we introduce a new symbolic representation of the lifted abstract domain that can efficiently analyze program families with numerical features. This makes sharing between property elements corresponding to different variants explicitly possible. The elements of the new lifted domain are constraint-based decision trees, where decision nodes are labeled with linear constraints defined over numerical features and the leaf nodes belong to an existing single-program analysis domain. To illustrate the potential of this representation, we have implemented an experimental lifted static analyzer, called SPLNum $$^2$$ 2 Analyzer, for inferring invariants of C programs. An empirical evaluation on BusyBox and on benchmarks from SV-COMP yields promising preliminary results indicating that our decision trees-based approach is effective and outperforms the baseline tuple-based approach.

Internet of Things (IoT) device software frequently handles sensitive data. This software has to be resistant to faults to prevent leakage and ensure data privacy and security. Source code hardening is a common way to make software fault-tolerant. However, the effectiveness and performance impact of a chosen hardening technique are not always obvious. Moreover, it becomes increasingly difficult to predict potential attack vectors and implement proper countermeasures. To assist in this task, we developed Chaos Duck, an automatic tool for IoT software fault-tolerance analysis. Chaos Duck emulates various fault types and provides statistics on their impact on software security and stability. We present a case study in which we use Chaos Duck to compare five software hardening techniques applied to the PRESENT block cipher implementation. We show that some simple hardening techniques may improve fault-tolerance, while others can instead reduce overall security and introduce new vulnerabilities. Our contributions are twofold: we offer a software fault-tolerance analysis tool to IoT developers seeking to make their software secure and robust, and we shed light on the efficiency of various hardening techniques.

Feature-based analysis of software product lines and family-based model checking have seen rapid development. Many model checking problems can be reduced to two-player games on finite graphs. A prominent example is mu-calculus model checking, which is generally done by translating to parity games, but also many quantitative model-checking problems can be reduced to (quantitative) games. As part of a program to make game-based model checking available for software product lines, we introduce featured reachability games, featured minimum reachability games, featured discounted games, featured energy games, and featured parity games. We show that all these admit optimal featured strategies, which project to optimal strategies for any product, and how to compute winners and values of such games in a family-based manner.

Domain-specific quantitative modeling and analysis approaches are fundamental in scenarios in which qualitative approaches are inappropriate or unfeasible. In this paper, we present a tool-supported approach to quantitative graph-based security risk modeling and analysis based on attack-defense trees. Our approach is based on QFLan, a successful domain-specific approach to support quantitative modeling and analysis of highly configurable systems, whose domain-specific components have been decoupled to facilitate the instantiation of the QFLan approach in the domain of graph-based security risk modeling and analysis. Our approach incorporates distinctive features from three popular kinds of attack trees, namely enhanced attack trees, capabilities-based attack trees and attack countermeasure trees, into the domain-specific modeling language. The result is a new framework, called RisQFLan, to support quantitative security risk modeling and analysis based on attack-defense diagrams. By offering either exact or statistical verification of probabilistic attack scenarios, RisQFLan constitutes a significant novel contribution to the existing toolsets in that domain. We validate our approach by highlighting the additional features offered by RisQFLan in three illustrative case studies from seminal approaches to graph-based security risk modeling analysis based on attack trees.

Abstract We propose a new Statistical Model Checking (SMC) method to identify bugs in variability-intensive systems (VIS). The state-space of such systems is exponential in the number of variants, which makes the verification problem harder than for classical systems. To reduce verification time, we propose to combine SMC with featured transition systems (FTS)—a model that represents jointly the state spaces of all variants. Our new methods allow the sampling of executions from one or more (potentially all) variants. We investigate their utility in two complementary use cases. The first case considers the problem of finding all variants that violate a given property expressed in Linear-Time Logic (LTL) within a given simulation budget. To achieve this, we perform random walks in the featured transition system seeking accepting lassos. We show that our method allows us to find bugs much faster (up to 16 times according to our experiments) than exhaustive methods. As any simulation-based approach, however, the risk of Type-1 error exists. We provide a lower bound and an upper bound for the number of simulations to perform to achieve the desired level of confidence. Our empirical study involving 59 properties over three case studies reveals that our method manages to discover all variants violating 41 of the properties. This indicates that SMC can act as a coarse-grained analysis method to quickly identify the set of buggy variants. The second case complements the first one. In case the coarse-grained analysis reveals that no variant can guarantee to satisfy an intended property in all their executions, one should identify the variant that minimizes the probability of violating this property. Thus, we propose a fine-grained SMC method that quickly identifies promising variants and accurately estimates their violation probability. We evaluate different selection strategies and reveal that a genetic algorithm combined with elitist selection yields the best results.

Fault injection is widely used as a method to evaluate the robustness and security of a system against many kinds of faults and attacks. Recent works have considered many ways to demonstrate security risks and viable attacks using fault injection, and some have also proposed countermeasures. However, no general and formal definition of fault injection or countermeasure has been provided that can be used to reason about such attacks. This leaves significant results in this area to be ad-hoc and without broad applicability. This paper presents formal definitions of both fault injection on an arbitrary system and what an effective countermeasure is. These definitions are used to prove that fault injection attacks cannot in general be prevented (by any countermeasure). An example is presented that demonstrates how to construct an effective countermeasure for a specific fault injection that parallels some well known approaches. Further extensions to account for probabilistic behaviour and systems with time are also presented. These definitions and results demonstrate formal proofs about the security and defences of systems in ways that can be used, thus yielding a broadly applicable approach that can formalise fault injections and countermeasures in the future.

We propose a new Statistical Model Checking (SMC) method to discover bugs in variability-intensive systems (VIS). The state-space of such systems is exponential in the number of variants, which makes the verification problem harder than for classical systems. To reduce verification time, we sample executions from a featured transition system – a model that represents jointly the state spaces of all variants. The combination of this compact representation and the inherent efficiency of SMC allows us to find bugs much faster (up to 16 times according to our experiments) than other methods. As any simulation-based approach, however, the risk of Type-1 error exists. We provide a lower bound and an upper bound for the number of simulations to perform to achieve the desired level of confidence. Our empirical study involving 59 properties over three case studies reveals that our method manages to discover all variants violating 41 of the properties. This indicates that SMC can act as a low-cost-high-reward method for verifying VIS.

The goal of probabilistic static analysis is to quantify the probability that a given program satisfies/violates a required property (assertion). In this work, we use a static analysis by abstract interpretation and model counting to construct probabilistic analysis of deterministic programs with uncertain input data, which can be used for estimating the probabilities of assertions ( program reliability ). In particular, we automatically infer necessary preconditions in order a given assertion to be satisfied/violated at run-time using a combination of forward and backward static analyses. The focus is on numeric properties of variables and numeric abstract domains, such as polyhedra. The obtained preconditions in the form of linear constraints are then analyzed to quantify how likely is an input to satisfy them. Model counting techniques are employed to count the number of solutions that satisfy given linear constraints. These counts are then used to assess the probability that the target assertion is satisfied/violated. We also present how to extend our approach to analyze non-deterministic programs by inferring sufficient preconditions. We built a prototype implementation and evaluate it on several interesting examples.

A crucial aspect that automotive systems need to face before being used in everyday life is the validation of their components. To this end, standard exhaustive methods are inappropriate to validate the probabilistic algorithms widely used in this field and new solutions need to be adopted. In this paper, we present an approach based on Statistical Model Checking (SMC) to validate the collision risk assessment generated by a probabilistic perception system. SMC represents an intermediate between test and exhaustive verification by relying on statistics and evaluates the probability of meeting appropriate Key Performance Indicators (KPIs) based on a large number of simulations. As a case study, a state-of-the-art algorithm is adopted to obtain the collision risk estimations. This algorithm provides an environment representation through Bayesian probabilistic occupancy grids and estimates positions in the near future of every static and dynamic part of the grid. Based on these estimations, time-to-collision probabilities are then associated with the corresponding cells. Using CARLA simulator, a large number of execution traces are then generated, considering both collisions and almost-collisions in realistic urban scenarios. Real experiments complete the analysis and show the reliability of the simulation results.

Smart home technology has gained widespread adoption. However, several instances of massive corporate surveillance and episodes of sensor data breaches have raised many privacy concerns amongst potential consumers. This paper presents PatrIoT, a private-by-design IoT platform for smart home environments. PatrIoT revisits the typical architecture of existing IoT platforms, and provides an alternative design where the home owner retains full ownership and control of smart device generated data. It leverages Intel SGX to prevent unauthorized access to the data by untrusted IoT cloud providers, and offers homeowners an intuitive security abstraction named flowwall which allows them to specify easy-to-use policies for controlling sensitive sensor data flows within their smart homes. We have built and evaluated a PatrIoT prototype. Most of the participants in a field study considered PatrIoT to be easy to use, and the supported policies to be useful in protecting their privacy.

The rise of highly configurable complex software and its widespread usage requires design of efficient testing methodology. t-wise coverage is a leading metric to measure the quality of the testing suite and the underlying test generation engine. While uniform sampling-based test generation is widely believed to be the state of the art approach to achieve t-wise coverage in presence of constraints on the set of configurations, such a scheme often fails to achieve high t-wise coverage in presence of complex constraints. In this work, we propose a novel approach Baital, based on adaptive weighted sampling using literal weighted functions, to generate test sets with high t-wise coverage. We demonstrate that our approach reaches significantly higher t-wise coverage than uniform sampling. The novel usage of literal weighted sampling leaves open several interesting directions, empirical as well as theoretical, for future research.

Software security is a fundamental dimension in the development of mobile applications (apps). Since many apps have access to sensitive data (e.g., collected from a smartphone's sensors), the presence of security vulnerabilities may put that data in danger and lead to privacy violations. Unfortunately, existing security solutions for Android are either too cumbersome to use by common app developers, or may require the modification of Android OS. This paper presents Flowverine, a system for building privacy-sensitive mobile apps for unmodified Android platforms. Flowverine exposes an API based on a dataflow programming model which allows for efficient taint tracking of sensitive data flows within each app. By checking such flows against a security policy, Flowverine can then prevent potential privacy violations. We implemented a prototype of our system. Our evaluation shows that Flowverine can be used to implement mobile applications that handle security-sensitive information flows while preserving compatibility with existing Android OS and incurring small performance overheads.

Service contracts characterise the desired behavioural compliance of a composition of services. Compliance is typically defined by the fulfilment of all service requests through service offers, as dictated by a given Service-Level Agreement (SLA). Contract automata are a recently introduced formalism for specifying and composing service contracts. Based on the notion of synthesis of the most permissive controller from Supervisory Control Theory, a safe orchestration of contract automata can be computed that refines a composition into a compliant one. To model more fine-grained SLA and more adaptive service orchestrations, in this paper we endow contract automata with two orthogonal layers of variability: (i) at the structural level, constraints over service requests and offers define different configurations of a contract automaton, depending on which requests and offers are selected or discarded, and (ii) at the behavioural level, service requests of different levels of criticality can be declared, which induces the novel notion of semi-controllability. The synthesis of orchestrations is thus extended to respect both the structural and the behavioural variability constraints. Finally, we show how to efficiently compute the orchestration of all configurations from only a subset of these configurations. A prototypical tool supports the developed theory.

This paper presents our approach to the quantitative modeling and analysis of highly (re)configurable systems, such as software product lines. Different combinations of the optional features of such a system give rise to combinatorially many individual system variants. We use a formal modeling language that allows us to model systems with probabilistic behavior, possibly subject to quantitative feature constraints, and able to dynamically install, remove or replace features. More precisely, our models are defined in the probabilistic feature-oriented language QFLan, a rich domain specific language (DSL) for systems with variability defined in terms of features. QFLan specifications are automatically encoded in terms of a process algebra whose operational behavior interacts with a store of constraints, and hence allows to separate system configuration from system behavior. The resulting probabilistic configurations and behavior converge seamlessly in a semantics based on discrete-time Markov chains, thus enabling quantitative analysis. Our analysis is based on statistical model checking techniques, which allow us to scale to larger models with respect to precise probabilistic analysis techniques. The analyses we can conduct range from the likelihood of specific behavior to the expected average cost, in terms of feature attributes, of specific system variants. Our approach is supported by a novel Eclipse-based tool which includes state-of-the-art DSL utilities for QFLan based on the Xtext framework as well as analysis plug-ins to seamlessly run statistical model checking analyses. We provide a number of case studies that have driven and validated the development of our framework.

Future-generation healthcare systems will be highly distributed, combining centralised hospital systems with decentralised home-, work-and environment-based monitoring and diagnostics systems. These will reduce costs and injury-related risks whilst both improving quality of service, and reducing the response time for diagnostics and treatments made available to patients. To make this vision possible, medical data must be accessed and shared over a variety of mediums including untrusted networks. In this paper, we present the design and initial implementation of the SERUMS tool-chain for accessing, storing, communicating and analysing highly confidential medical data in a safe, secure and privacy-preserving way. In addition, we describe a data fabrication framework for generating large volumes of synthetic but realistic data, that is used in the design and evaluation of the tool-chain. We demonstrate the present version of our technique on a use case derived from the Edinburgh Cancer Centre, NHS Lothian, where information about the effects of chemotherapy treatments on cancer patients is collected from different distributed databases, analysed and adapted to improve ongoing treatments.

Variability models allow effective building of many custom model variants for various configurations. Lifted model checking for a variability model is capable of verifying all its variants simultaneously in a single run by exploiting the similarities between the variants. The computational cost of lifted model checking still greatly depends on the number of variants (the size of configuration space), which is often huge. One of the most promising approaches to fighting the configuration space explosion problem in lifted model checking are variability abstractions . In this work, we define a novel game-based approach for variability-specific abstraction and refinement for lifted model checking of the full CTL, interpreted over 3-valued semantics. We propose a direct algorithm for solving a 3-valued (abstract) lifted model checking game. In case the result of model checking an abstract variability model is indefinite, we suggest a new notion of refinement, which eliminates indefinite results. This provides an iterative incremental variability-specific abstraction and refinement framework, where refinement is applied only where indefinite results exist and definite results from previous iterations are reused.

Efficient and safe railway signalling systems, together with energy-saving infrastructures, are among the main pillars to guarantee sustainable transportation. ERTMS L3 moving block is one of the next generation railway signalling systems currently under trial deployment, with the promise of increased capacity on railway tracks, reduced costs and improved reliability. We report an experience in modelling a satellite-based ERTMS L3 moving block signalling system from the railway industry with Simulink and Uppaal and analysing the Uppaal model with Uppaal SMC. The lessons learned range from demonstrating the feasibility of applying Uppaal SMC in a moving block railway context, to the offered possibility of fine tuning communication parameters in satellite-based ERTMS L3 moving block railway signalling system models that are fundamental for the reliability of their operational behaviour.

Automotive systems must undergo a strict process of validation before their release on commercial vehicles. With the increased use of probabilistic approaches in autonomous systems, standard validation methods are not applicable to this end. Furthermore, real life validation, when even possible, implies costs which can be obstructive. New methods for validation and testing are thus necessary. In this paper, we propose a generic method to evaluate complex probabilistic frameworks for autonomous driving. The method is based on Statistical Model Checking (SMC), using specifically defined Key Performance Indicators (KPIs), as temporal properties depending on a set of identified metrics. By studying the behavior of these metrics during a large number of simulations via our statistical model checker, we finally evaluate the probability for the system to meet the KPIs. We show how this method can be applied to two different subsystems of an autonomous vehicle: a perception system and a decision-making approach. An overview of these two systems is given to understand related validation challenges. Extensive validation results are then provided for the decision-making case.

Previous analyses of IKEv2 concluded that the protocol was suffering from two authentication vulnerabilities: the penultimate authentication flaw and a vulnerability that leads to a reflection attack. In this paper, we analyze the IKEv2 protocol specification using the Spin model checker. To do so, we extend and improve an existing modeling method that allows analyzing security protocols using Spin. For completeness, we indicate each abstraction we make when writing the model. As a result, we confirm the penultimate authentication flaw and show that the reflection attack is actually not applicable.

Application requirements evolve over time and the underlying protocols need to adapt. Most transport protocols evolve by negotiating protocol extensions during the handshake. Experience with TCP shows that this leads to delays of several years or more to widely deploy standardized extensions. In this paper, we revisit the extensibility paradigm of transport protocols.

Summary Fault injection has increasingly been used both to attack software applications and to test system robustness. Detecting fault injection vulnerabilities has been approached with a variety of different but limited methods. This paper proposes an extension of a recently published general model checking based process to detect fault injection vulnerabilities in binaries. This new extension makes the general process scalable to real‐world implementations, which is demonstrated by detecting vulnerabilities in different cryptographic implementations.

Abstract Analysis of a probabilistic system often requires to learn the joint probability distribution of its random variables. The computation of the exact distribution is usually an exhaustiveprecise analysison all executions of the system. To avoid the high computational cost of such an exhaustive search,statistical analysishas been studied to efficiently obtain approximate estimates by analyzing only a small but representative subset of the system’s behavior. In this paper we propose ahybrid statistical estimation methodthat combines precise and statistical analyses to estimate mutual information, Shannon entropy, and conditional entropy, together with their confidence intervals. We show how to combine the analyses on different components of a discrete system with different accuracy to obtain an estimate for the whole system. The new method performs weighted statistical analysis with different sample sizes over different components and dynamically finds their optimal sample sizes. Moreover, it can reduce sample sizes by using prior knowledge about systems and a newabstraction-then-samplingtechnique based on qualitative analysis. To apply the method to the source code of a system, we show how to decompose the code into components and to determine the analysis method for each component by overviewing the implementation of those techniques in the HyLeak tool. We demonstrate with case studies that the new method outperforms the state of the art in quantifying information leakage.

A fault attack is a well-known technique where the behaviour of a chip is voluntarily disturbed by hardware means in order to undermine the security of the information handled by the target. In this paper, we explore how Electromagnetic fault injection (EMFI) can be used to create vulnerabilities in sound software, targeting a Cortex-M3 microcontroller. Several use-cases are shown experimentally: control flow hijacking, buffer overflow (even with the presence of a canary), covert backdoor insertion and Return Oriented Programming can be achieved even if programs are not vulnerable in a software point of view. These results suggest that the protection of any software against vulnerabilities must take hardware into account as well.

The largest botnet distributed denial of service attacks in history have been executed by devices controlled by the Mirai botnet trojan. To prevent Mirai from spreading, this paper presents and evaluates techniques to classify binary samples as Mirai based on their syntactic and behavioral properties. Syntactic malware detection is shown to have a good detection rate and no false positives, but to be very easy to circumvent. Behavioral malware detection is resistant to simple obfuscation and has better detection rate than syntactic detection, while keeping false positives to zero. This paper demonstrates these results, and concludes by showing how to combine syntactic and behavioral analysis techniques for the detection of Mirai.

The concept of decomposition in computer science and engineering is considered a fundamental component of computational thinking and is prevalent in design of algorithms, software construction, hardware design, and more. We propose a simple and natural formalization of sequential decomposition, in which a task is decomposed into two sequential sub-tasks, with the first sub-task to be executed out before the second sub-task is executed. These tasks are specified by means of input/output relations. We define and study decomposition problems, which is to decide whether a given specification can be sequentially decomposed. Our main result is that decomposition itself is a difficult computational problem. More specifically, we study decomposition problems in three settings: where the input task is specified explicitly, by means of Boolean circuits, and by means of automatic relations. We show that in the first setting decomposition is NP-complete, in the second setting it is NEXPTIME-complete, and in the third setting there is evidence to suggest that it is undecidable. Our results indicate that the intuitive idea of decomposition as a system-design approach requires further investigation. In particular, we show that adding human to the loop by asking for a decomposition hint lowers the complexity of decomposition problems considerably.

We present an algebra of discrete timed input/output automata that may execute in the context of different clock granularities – which we call timed machines; this algebra includes a refinement operator through which a machine can be extended with new states and transitions in order to accommodate a finer clock granularity as required to interoperate with other machines, and an extension of the traditional product of timed input–output automata to the situation in which the granularities of the two machines are not the same. Over this algebra, we then define an algebra of networks of timed machines that includes operations through which networks can be modified at run time, thus offering a model for systems of interconnected components that can dynamically bind to other systems and, therefore, cannot be adjusted at design time to ensure that they operate in a timed homogeneous setting. We investigate important properties of timed machines such as consistency – in the sense that a machine can be ensured to generate a non-empty language, and feasibility – in the sense that a machine can be ensured to generate a non-empty language no matter what inputs it receives, and propose techniques for checking if timed machines are consistent or are feasible. We generalise those properties to networks of timed machines, and investigate how consistency and feasibility of networks can be proved through properties that can be checked at design time without having to compute, at run time, the product of the machines that operate on those networks, which would not be practical.

Abstract Transaction‐level modeling with SystemC has been very successful in describing the behavior of embedded systems by providing high‐level executable models, in which many of them have inherent probabilistic behaviors, eg, random data and unreliable components. It is thus crucial to have both quantitative and qualitative analysis of the probabilities of system properties. Such analysis can be conducted by constructing a formal model of the system under verification and using Probabilistic Model Checking. However, this method is infeasible for large systems, due to the state space explosion. In this article, we demonstrate the successful use of statistical model checking to conduct such analysis directly from large SystemC models and allow designers to express a wide range of useful properties. The first contribution of this work is a framework to verify properties expressed in Bounded Linear Temporal Logic for SystemC models with both timed and probabilistic characteristics. Second, the framework allows users to expose a rich set of user code primitives as atomic propositions in Bounded Linear Temporal Logic. Moreover, users can define their own fine‐grained time resolution rather than the boundary of clock cycles in the SystemC simulation. The third contribution is an implementation of a statistical model checker. It contains an automatic monitor generation for producing execution traces of the model‐under‐verification, the mechanism for automatically instrumenting the model‐under‐verification, and the interaction with statistical model checking algorithms.

While standalone tools for verification and modeling have proven useful, their chosen formalism and description-language can at times be restrictive. We demonstrate how to use U PPAAL SMC to analyze controller systems consisting of Function Mockup Units (FMU) modeled in other tools, such as Matlab and Modelica. Apart from supporting FMI-FMU modules the newly added C interface can call any external function. The only requirement for sound analysis is statelessness and determinism of the external function. We demonstrate the expressive power by implementing the FMI-FMU master algorithm as a timed automata, interfacing with external, non-native and non-trivial Function Mockup Units (FMU). We also model two components in U PPAAL SMC exporting one of them as an FMU while keeping the other as a native component. Furthermore we demonstrate the first simulation environment for the Function Mockup Units, capable of checking bounded MITL properties.

Mutation analysis is a popular test assessment method. It relies on the mutation score, which indicates how many mutants are revealed by a test suite. Yet, there are mutants whose behaviour is equivalent to the original system, wasting analysis resources and preventing the satisfaction of the full (100%) mutation score. For finite behavioural models, the Equivalent Mutant Problem (EMP) can be addressed through language equivalence of non-deterministic finite automata, which is a well-studied, yet computationally expensive, problem in automata theory. In this paper, we report on our preliminary assessment of a state-of-the-art exact language equivalence tool to handle the EMP against 3 models of size up to 15,000 states on 1170 mutants. We introduce random and mutation-biased simulation heuristics as baselines for comparison. Results show that the exact approach is often more than ten times faster in the weak mutation scenario. For strong mutation, our biased simulations are faster for models larger than 300 states. They can be up to 1,000 times faster while limiting the error of misclassifying non-equivalent mutants as equivalent to 10% on average. We therefore conclude that the approaches can be combined for improved efficiency.

Cyber-physical systems (CSPs) are demanding energy-efficient design not only of hardware (HW), but also of software (SW). Dynamic Voltage and Frequency Scaling (DVFS) and Dynamic Power Manage (DPM) are most popular techniques to improve the energy efficiency. However, contemporary complicated HW and SW designs requires more elaborate and sophisticated energy management and efficiency evaluation techniques. This paper is concerned about energy supply planning for real-time scheduling systems (units) of which tasks need to meet deadlines. This paper presents a model-based compositional energy planning technique that computes a minimal ratio of processor frequency that preserves schedulability of independent and preemptive tasks. The minimal ratio of processor frequency can be used to plan the energy supply of real-time components. Our model-based technique is extensible by refining our model with additional features so that energy management techniques and their energy efficiency can be evaluated by model checking techniques. We exploit the compositional framework for hierarchical scheduling systems and provide a new resource model for the frequency computation. As results, our use-case for avionics software components shows that our new method outperforms the classical real-time calculus (RTC) method, requiring 36.21% less frequency ratio on average for scheduling units under RM than the RTC method.

Metric Temporal Logic MTL0,∞ is a timed extension of linear temporal logic, LTL, with time intervals whose left endpoints are zero or whose right endpoints are infinity. Whereas the satisfiability and model-checking problems for MTL0,∞ are both decidable, we note that the controller synthesis problem for MTL0,∞ is unfortunately undecidable. As a remedy of this we propose an approximate method to the synthesis problem, which we demonstrate to be adequate and scalable to practical examples. We define a method for converting MTL0,∞ formulas into (nondeterministic) Timed Game Büchi Automata and furthermore show how to construct determinized over- and underapproximation of a such. For the proposed method, we present a toolchain seamlessly integrating the needed components for practical MTL0,∞ synthesis. Lastly we demonstrate on a pair of case-studies the applicability and scalability of the proposed method.

Model-based mutation analysis is a powerful but expensive testing technique. We tackle its high computation cost by proposing an optimization technique that drastically speeds up the mutant execution process. Central to this approach is the Featured Mutant Model, a modelling framework for mutation analysis inspired by the software product line paradigm. It uses behavioural variability models, viz., Featured Transition Systems, which enable the optimized generation, configuration and execution of mutants. We provide results, based on models with thousands of transitions, suggesting that our technique is fast and scalable. We found that it outperforms previous approaches by several orders of magnitude and that it makes higher-order mutation practically applicable.

By analogy with software product reuse, the ability to reuse (meta)models and model transformations is key to achieve better quality and productivity. To this end, various opportunistic reuse techniques have been developed, such as higher-order transformations, metamodel adaptation, and model types. However, in contrast to software product development that has moved to systematic reuse by adopting (model-driven) software product lines, we are not quite there yet for modelling languages, missing economies of scope and automation opportunities. Our vision is to transpose the product line paradigm at the metamodel level, where reusable assets are formed by metamodel and transformation fragments and "products" are reusable language building blocks (model types). We introduce featured model types to concisely model variability amongst metamodelling elements, enabling configuration, automated analysis, and derivation of tailored model types. We provide a wish list of software engineering activities to work with featured model types.

A software product line is a family of software products that share a common set of mandatory features and whose individual products are differentiated by their variable (optional or alternative) features. Family-based analysis of software product lines takes as input a single model of a complete product line and analyzes all its products at the same time. As the number of products in a software product line may be large, this is generally preferable to analyzing each product on its own. Family-based analysis, however, requires that standard algorithms be adapted to accomodate variability.

In distributed development of modern systems, contracts play a vital role in ensuring interoperability of components and adherence to specifications. It is therefore often desirable to verify the satisfaction of an overall property represented as a contract, given the satisfaction of smaller properties also represented as contracts. When the verification result is negative, designers must face the issue of refining the subproperties and components. This is an instance of the classical synthesis problems: “can we construct a model that satisfies some given specification?” In this work, we propose two strategies enabling designers to synthesize or refine a set of contracts so that their composition satisfies a given contract. We develop a generic algebraic method and show how it can be applied in different contract models to support top-down component-based development of distributed systems.

Building abstract system-level models that faithfully capture performance and functional behavior for embedded systems design is challenging. Unlike functional aspects, performance details are rarely available during the early design phases, and no clear method is known to characterize them. Moreover, once such models are built, they are inherently complex as they mix software models, hardware constraints, and environment abstractions. Their analysis by using traditional performance evaluation methods is reaching the limit. In this article, we present a systematic approach for building stochastic abstract performance models using statistical inference and model calibration, and we propose statistical model checking as a scalable performance evaluation technique for them.

We propose a generalization of higher-dimensional automata, partial HDA. Unlike HDA, and also extending event structures and Petri nets, partial HDA can model phenomena such as priorities or the disabling of an event by another event. Using open maps and unfoldings, we introduce a natural notion of (higher-dimensional) bisimilarity for partial HDA and relate it to history-preserving bisimilarity and split bisimilarity. Higher-dimensional bisimilarity has a game characterization and is decidable in polynomial time.

We develop a *-continuous Kleene omega-algebra of real-time energy functions. Together with corresponding automata, these can be used to model systems which can consume and regain energy (or other types of resources) depending on available time. Using recent results on *-continuous Kleene omega-algebras and computability of certain manipulations on real-time energy functions, it follows that reachability and Büchi acceptance in real-time energy automata can be decided in a static way which only involves manipulations of real-time energy functions.

We investigate the suitability of statistical model checking for the analysis of probabilistic models of software product lines with complex quantitative constraints and advanced feature installation options. Such models are specified in the feature-oriented language QFLan, a rich process algebra whose operational behaviour interacts with a store of constraints, neatly separating product configuration from product behaviour. The resulting probabilistic configurations and behaviour converge seamlessly in a semantics based on DTMCs, thus enabling quantitative analyses ranging from the likelihood of certain behaviour to the expected average cost of products. This is supported by a Maude implementation of QFLan, integrated with the SMT solver Z3 and the distributed statistical model checker MultiVeStA. Our approach is illustrated with a bikes product line case study.

SPLat 2015 workshop aims to provide a forum where various approaches to formal analysis and testing of variability-intensive systems can be presented, evaluated and discussed. In particular, the workshop tries to identify commonalities and variabilities regarding the choice of underlying concepts that capture variability as well as strengths and weaknesses of approaches in their effort to defeat combinatorial explosion. The long term goal of the workshop is to provide guidance to practitioners on where and when to use the aforementioned techniques while validating variability-intensive systems.

In recent years, quantitative security techniques have been providing effective measures of the security of a system against an attacker. Such techniques usually assume that the system produces a finite amount of observations based on a finite amount of secret bits and terminates, and the attack is based on these observations. By modeling systems with Markov chains, we are able to measure the effectiveness of attacks on non-terminating systems. Such systems do not necessarily produce a finite amount of output and are not necessarily based on a finite amount of secret bits. We provide characterizations and algorithms to define meaningful measures of security for non-terminating systems, and to compute them when possible. We also study the bounded versions of the problems, and show examples of non-terminating programs and how their effectiveness in protecting their secret can be measured.

Performance and functional correctness are key for successful design of modern embedded systems. Both aspects must be considered early in the design process to enable founded decision making towards final implementation. Nonetheless, building abstract system-level models that faithfully capture performance information along to functional behavior is a challenging task. In contrast to functional aspects, performance details are rarely available during early design phases and no clear method is known to characterize them. Moreover, once such system-level models are built they are inherently complex as they usually mix software models, hardware architecture constraints and environment abstractions. Their analysis by using traditional performance evaluation methods is reaching the limits and the need for more scalable and accurate techniques is becoming urgent. In this paper, we introduce a systematic method for building stochastic abstract performance models using statistical inference and model calibration and we propose statistical model checking as performance evaluation technique upon the obtained models. We experimented our method on a real-life case study and we were able to verify different timing properties.

The model-checking problem for Software Products Lines (SPLs) is harder than for single systems: variability constitutes a new source of complexity that exacerbates the state-explosion problem. Abstraction techniques have successfully alleviated state explosion in single-system models. However, they need to be adapted to SPLs, to take into account the set of variants that produce a counterexample. In this paper, we apply CEGAR (Counterexample-Guided Abstraction Refinement) and we design new forms of abstraction specifically for SPLs. We carry out experiments to evaluate the efficiency of our new abstractions. The results show that our abstractions, combined with an appropriate refinement strategy, hold the potential to achieve large reductions in verification time, although they sometimes perform worse. We discuss in which cases a given abstraction should be used.

Mutation testing is an effective technique for either improving or generating fault-finding test suites. It creates defective or incorrect program artifacts of the program under test and evaluates the ability of test suites to reveal them. Despite being effective, mutation is costly since it requires assessing the test cases with a large number of defective artifacts. Even worse, some of these artifacts are behaviourally ``equivalent'' to the original one and hence, they unnecessarily increase the testing effort. We adopt a variability perspective on mutation analysis. We model a defective artifact as a transition system with a specific feature selected and consider it as a member of a mutant family. The mutant family is encoded as a Featured Transition System, a compact formalism initially dedicated to model-checking of software product lines. We show how to evaluate a test suite against the set of all candidate defects by using mutant families. We can evaluate all the considered defects at the same time and isolate some equivalent mutants. We can also assist the test generation process and efficiently consider higher-order mutants.

The SPLat 2014 workshop aims to provide a platform for the presentation and positioning of formal analysis tools as used in Software Product Line Engineering for the identification of commonalities and differences of these tools as well as for the inventorying of challenges for their application. SPLat 2014 focuses on the underlying concepts and overall approach, in particular how to mitigate combinatorial explosion.

This paper surveys the main functionalities of the PLASMA statistical model checking platform developed at India.

We present a distance-agnostic approach to quantitative verification. Taking as input an unspecified distance on system traces, or executions, we develop a game-based framework which allows us to define a spectrum of different interesting system distances corresponding to the given trace distance. Thus we extend the classic linear-time–branching-time spectrum to a quantitative setting, parametrized by trace distance. We also prove a general transfer principle which allows us to transfer counterexamples from the qualitative to the quantitative setting, showing that all system distances are mutually topologically inequivalent.

An accurate model of human behaviour is crucial when planning robot motion in human environments. The Social Force Model (SFM) is such a model, having parameters that control both deterministic and stochastic elements. We have constructed an efficient motion planning algorithm by embedding the SFM in a control loop that determines higher level objectives and reacts to environmental changes. Low level predictive modelling is provided by the SFM fed by sensors; high level logic is provided by statistical model checking. To parametrise and improve our motion planning algorithm, we have conducted experiments to consider typical human interactions in crowded environments. We have identified a number of behavioural patterns which may be explicitly incorporated in the SFM to enhance its predictive power. In this paper we describe the results of these experiments and how we parametrise the SFM.

Model checking techniques for software product lines (SPL) are actively researched. A major limitation they currently have is the inability to deal efficiently with non-Boolean features and multi-features. An example of a non-Boolean feature is a numeric attribute such as maximum number of users which can take different numeric values across the range of SPL products. Multi-features are features that can appear several times in the same product, such as processing units which number is variable from one product to another and which can be configured independently. Both constructs are extensively used in practice but currently not supported by existing SPL model checking techniques. To overcome this limitation, we formally define a language that integrates these constructs with SPL behavioural specifications. We generalize SPL model checking algorithms correspondingly and evaluate their applicability. Our results show that the algorithms remain efficient despite the generalization.

Variability is becoming an increasingly important concern in software development but techniques to cost-effectively verify and validate software in the presence of variability have yet to become widespread. This half-day tutorial offers an overview of the state of the art in an emerging discipline at the crossroads of formal methods and software engineering: quality assurance of variability-intensive systems. We will present the most significant results obtained during the last four years or so, ranging from conceptual foundations to readily usable tools. Among the various quality assurance techniques, we focus on model checking, but also extend the discussion to other techniques. With its lightweight usage of mathematics and balance between theory and practice, this tutorial is designed to be accessible to a broad audience. Researchers working in the area, willing to join it, or simply curious, will get a comprehensive picture of the recent developments. Practitioners developing variability-intensive systems are invited to discover the capabilities of our techniques and tools, and to consider integrating them in their processes.

The premise of variability-intensive systems, specifically in software product line engineering, is the ability to produce a large family of different systems efficiently. Many such systems are critical. Thorough quality assurance techniques are thus required. Unfortunately, most quality assurance techniques were not designed with variability in mind. They work for single systems, and are too costly to apply to the whole system family. In this paper, we propose an efficient automata-based approach to linear time logic (LTL) model checking of variability-intensive systems. We build on earlier work in which we proposed featured transitions systems (FTSs), a compact mathematical model for representing the behaviors of a variability-intensive system. The FTS model checking algorithms verify all products of a family at once and pinpoint those that are faulty. This paper complements our earlier work, covering important theoretical aspects such as expressiveness and parallel composition as well as more practical things like vacuity detection and our logic feature LTL. Furthermore, we provide an in-depth treatment of the FTS model checking algorithm. Finally, we present SNIP, a new model checker for variability-intensive systems. The benchmarks conducted with SNIP confirm the speedups reported previously.

This paper surveys well-established/recent tools and techniques developed for the design of rigorous embedded systems. We will first survey UPPAAL and MODEST, two tools capable of dealing with both timed and stochastic aspects. Then, we will overview the BIP framework for modular design and code generation. Finally, model-based testing will be discussed.

Software Product Line (SPL) engineering is a software engineering paradigm that exploits the commonality between similar software products to reduce life cycle costs and time-to-market. Many SPLs are critical and would benefit from efficient verification through model checking. Model checking SPLs is more difficult than for single systems, since the number of different products is potentially huge. In previous work, we introduced Featured Transition Systems (FTS), a formal, compact representation of SPL behaviour, and provided efficient algorithms to verify FTS. Yet, we still face the state explosion problem, like any model checking-based verification. Model abstraction is the most relevant answer to state explosion. In this paper, we define a novel simulation relation for FTS and provide an algorithm to compute it. We extend well-known simulation preservation properties to FTS and thus lay the theoretical foundations for abstraction-based model checking of SPLs. We evaluate our approach by comparing the cost of FTS-based simulation and abstraction with respect to product-by-product methods. Our results show that FTS are a solid foundation for simulation-based model checking of SPL.

In Software Product Line (SPL) engineering, software products are build in families rather than individually. Many critical software are nowadays build as SPLs and most of them obey hard real-time requirements. Formal methods for verifying SPLs are thus crucial and actively studied. The verification problem for SPL is, however, more complicated than for individual systems; the large number of different software products multiplies the complexity of SPL model-checking. Recently, promising model-checking approaches have been developed specifically for SPLs. They leverage the commonality between the products to reduce the verification effort. However, none of them considers real time.

Most model-checking algorithms are based on automata theory. For instance, determining whether or not a transition system satisfies a Linear Temporal Logic (LTL) formula requires computing strongly connected component of its transition graph. In Software Product-Line (SPL) engineering, the model checking problem is more complex due to the huge amount of software products that may compose the line. Indeed, one has to determine the exact subset of those products that do not satisfy an intended property. Efficient dedicated verification methods have been recently developed to answer this problem. However, most of them does not allow incremental verification. In this paper, we introduce an automata-based incremental approach for SPL model checking. Our method makes use of previous results to determine whether or not the addition of conservative features (i.e., features that do not remove behaviour from the system) preserves the satisfaction of properties expressed in LTL. We provide a detailed description of the approach and propose algorithms that implement it. We discuss how our method can be combined with SPL dedicated verification methods, viz. Featured Transition Systems.

Multiweighted modal automata provide a specification theory for multiweighted transition systems that have recently attracted interest in the context of energy games. We propose a simple fragment of CTL that is able to express properties about accumulated weights along maximal runs of multiweighted modal automata. Our logic is equipped with a game-based semantics and guarantees both soundness (formula satisfaction is propagated to the modal refinements) as well as completeness (formula non-satisfaction is propagated to at least one of its implementations). We augment our theory with a summary of decidability and complexity results of the generalized model checking problem, asking whether a specification -- abstracting the whole set of its implementations -- satisfies a given formula.

We introduce a novel formalism of label-structured modal transition systems that combines the classical may/must modalities on transitions with structured labels that represent quantitative aspects of the model. On the one hand, the specification formalism is general enough to include models like weighted modal transition systems and allows system developers to employ more complex label refinement than in previously studied theories. On the other hand, the formalism maintains the desirable properties required by any specification theory supporting compositional reasoning. In particular, we study modal and thorough refinement, determinisation, parallel composition, conjunction, quotient and logical characterisation of label-structured modal transition systems.

We present a distance-agnostic approach to quantitative verification. Taking as input an unspecified distance on system traces, or executions, we develop a game-based framework which allows us to define a spectrum of different interesting system distances corresponding to the given trace distance. Thus we extend the classic linear-time–branching-time spectrum to a quantitative setting, parametrized by trace distance. We also prove a general transfer principle which allows us to transfer counterexamples from the qualitative to the quantitative setting, showing that all system distances are mutually topologically inequivalent.

We study the problem of model checking software product line (SPL) behaviours against temporal properties. This is more difficult than for single systems because an SPL with n features yields up to 2n individual systems to verify. As each individual verification suffers from state explosion, it is crucial to propose efficient formalisms and heuristics.

Concurrent systems are prone to deadlocks that arise from competing access to shared resources and synchronization between the components. At the same time, concurrency leads to a dramatic increase of the possible state space due to interleavings of computations, which makes standard verification techniques often infeasible. Previous work has shown that approximating the state space of component based systems by computing invariants allows to verify much larger systems then standard methods that compute the exact state space. The approach comes with the drawback, though, that not all of the reported specification violations may be reachable in the system. This paper deals with that problem by combining the information from the invariant with model checking techniques and strategies for reducing the memory footprint. The approach is implemented as post processing step for generating the exact set of reachable specification violations along with traces to demonstrate the error.

This paper presents the modal interface theory, a unification of interface automata and modal specifications, two radically dissimilar models for interface theories. Interface automata is a game-based model, which allows the designer to express assum

A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation and a set of operators supporting stepwise design.We develop a complete specification framework for real-time systems using Timed I/O Automata as the specification formalism, with the semantics expressed in terms of Timed I/O Transition Systems.We provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications -all indispensable ingredients of a compositional design methodology.The theory is implemented on top of an engine for timed games, Uppaal-tiga, and illustrated with a small case study.

In product line engineering, systems are developed in families and differences between family members are expressed in terms of features. Formal modelling and verification is an important issue in this context as more and more critical systems are developed this way. Since the number of systems in a family can be exponential in the number of features, two major challenges are the scalable modelling and the efficient verification of system behaviour. Currently, the few attempts to address them fail to recognise the importance of features as a unit of difference, or do not offer means for automated verification.

We consider a compositional method for the verification of component-based systems described in a subset of the BIP language encompassing multi-party interactions. The method is based on the use of two kinds of invariants. Component invariants are over-approximations of components' reach ability sets. Interaction invariants are constraints on the states of components involved in interactions. In this paper we propose fixed point characterization for computing interaction invariants. We also propose a new technique that takes the incremental design of the system into account. In many situations, the technique will help to avoid redoing all the verification process each time an interaction is added in the design. Our two techniques have been implemented as extension of the D-Finder toolset. The result has been applied to check deadlock-freedom on several case studies. Our experiments show that our new methodology is generally much faster than existing ones.

Checking infinite-state systems is frequently done by encoding infinite sets of states as regular languages. Computing such a regular representation of, say, the set of reachable states of a system requires acceleration techniques that can finitely compute the effect of an unbounded number of transitions. Among the acceleration techniques that have been proposed, one finds both specific and generic techniques. Specific techniques exploit the particular type of system being analyzed, for example, a system manipulating queues or integers, whereas generic techniques only assume that the transition relation is represented by a finite-state transducer, which has to be iterated. In this article, we investigate the possibility of using generic techniques in cases where only specific techniques have been exploited so far. Finding that existing generic techniques are often not applicable in cases easily handled by specific techniques, we have developed a new approach to iterating transducers. This new approach builds on earlier work, but exploits a number of new conceptual and algorithmic ideas, often induced with the help of experiments, that give it a broad scope, as well as good performances.

This paper presents a unification of interface automata and modal specifications, two radically dissimilar models for interface theories. Interface automata is a game-based model, which allows to make assumptions on the environment and propose an optimistic view for composition : two components can be composed if there is an environment where they can work together. Modal specification is a language theoretic account of a fragment of the modal mu-calculus logic that is more complete but which does not allow to distinguish between the environment and the component. Partial unifications of these two frameworks have been explored recently. A first attempt by Larsen et al. considers modal interfaces, an extension of modal specifications that deals with compatibility issues in the composition operator. However, this composition operator is incorrect. A second attempt by Raclet et al. gives a different perspective, and emphasises on conjunction and residuation of modal specifications, including when interfaces have dissimilar alphabets, but disregards interface compatibility. The present paper contributes a thorougher unification of the two theories by correcting the modal interface composition operator presented in the paper by Larsen et al., drawing a complete picture of the modal interface algebra, and pushing even further the comparison between interface automata, modal automata and modal interfaces.

We address the problem of alternating simulation refinement for concurrent timed games (\TG). We show that checking timed alternating simulation between\TG is \EXPTIME-complete, and provide a logical characterization of thispreorder in terms of a meaningful fragment of a new logic, \TAMTLSTAR.\TAMTLSTAR is an action-based timed extension of standard alternating-timetemporal logic \ATLSTAR, which allows to quantify on strategies where thedesignated player is not responsible for blocking time. While for full \TAMTLSTAR, model-checking \TG is undecidable, we show that for its fragment \TAMTL, corresponding to the timed version of \ATL, in \EXPTIME.

We present the tool Ticc ( Tool for Interface Compatibility and Composition ). In Ticc , a component interface describes both the behavior of a component, and the component’s assumptions on the environment’s behavior. Ticc can check the compatibility of such interfaces, and analyze their emergent behavior, via a symbolic implementation of game-theoretic algorithms. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Abstract. Checking infinite-state systems is frequently done by encoding infinite sets of states as regular languages. Computing such a regular representation of, say, the reachable set of states of a system requires acceleration techniques that can finitely compute the effect of an unbounded number of transitions. Among the acceleration techniques that have been proposed, one finds both specific and generic techniques. Specific techniques exploit the particular type of system being analyzed, e.g. a system manipulating queues or integers, whereas generic techniques only assume that the transition relation is represented by a finite-state transducer, which has to be iterated. In this paper, we investigate the possibility of using generic techniques in cases where only specific techniques have been exploited so far. Finding that existing generic techniques are often not applicable in cases easily handled by specific techniques, we have developed a new approach to iterating transducers. This new approach builds on earlier work, but exploits a number of new conceptual and algorithmic ideas, often induced with the help of experiments, that give it a broad scope, as well as good performance. 1