Showing 1–50 of 69 results for author: Legay, A

Compatibility of Fairness Metrics with EU Non-Discrimination Laws: Demographic Parity & Conditional Demographic Disparity

Authors: Lisa Koutsoviti Koumeri, Magali Legast, Yasaman Yousefi, Koen Vanhoof, Axel Legay, Christoph Schommer

Abstract: Empirical evidence suggests that algorithmic decisions driven by Machine Learning (ML) techniques threaten to discriminate against legally protected groups or create new sources of unfairness. This work supports the contextual approach to fairness in EU non-discrimination legal framework and aims at assessing up to what point we can assure legal fairness through fairness metrics and under fairness… ▽ More Empirical evidence suggests that algorithmic decisions driven by Machine Learning (ML) techniques threaten to discriminate against legally protected groups or create new sources of unfairness. This work supports the contextual approach to fairness in EU non-discrimination legal framework and aims at assessing up to what point we can assure legal fairness through fairness metrics and under fairness constraints. For that, we analyze the legal notion of non-discrimination and differential treatment with the fairness definition Demographic Parity (DP) through Conditional Demographic Disparity (CDD). We train and compare different classifiers with fairness constraints to assess whether it is possible to reduce bias in the prediction while enabling the contextual approach to judicial interpretation practiced under EU non-discrimination laws. Our experimental results on three scenarios show that the in-processing bias mitigation algorithm leads to different performances in each of them. Our experiments and analysis suggest that AI-assisted decision-making can be fair from a legal perspective depending on the case at hand and the legal justification. These preliminary results encourage future work which will involve further case studies, metrics, and fairness notions. △ Less

Submitted 14 June, 2023; originally announced June 2023.

Comments: Submitted at the 19th International Conference on Artificial Intelligence and Law - ICAIL 2023. Expected decision date is July 18, 2023

Experimental Toolkit for Manipulating Executable Packing

Authors: Alexandre D'Hondt, Charles-Henry Bertrand Van Ouytsel, Axel Legay

Abstract: Be it for a malicious or legitimate purpose, packing, a transformation that consists in applying various operations like compression or encryption to a binary file, i.e. for making reverse engineering harder or obfuscating code, is widely employed since decades already. Particularly in the field of malware analysis where a stumbling block is evasion, it has proven effective and still gives a hard… ▽ More Be it for a malicious or legitimate purpose, packing, a transformation that consists in applying various operations like compression or encryption to a binary file, i.e. for making reverse engineering harder or obfuscating code, is widely employed since decades already. Particularly in the field of malware analysis where a stumbling block is evasion, it has proven effective and still gives a hard time to scientists who want to efficiently detect it. While already extensively covered in the scientific literature, it remains an open issue especially when considering its detection time and accuracy trade-off. Many approaches, including machine learning, have been proposed but most studies often restrict their scope (i.e. malware and PE files), rely on uncertain datasets (i.e. built based on a super-detector or using labels from an questionable source) and do no provide any open implementation, which makes comparing state-of-the-art solutions tedious. Considering the many challenges that packing implies, there exists room for improvement in the way it is addressed, especially when dealing with static detection techniques. In order to tackle with these challenges, we propose an experimental toolkit, aptly called the Packing Box, leveraging automation and containerization in an open source platform that brings a unified solution to the research community and we showcase it with some experiments including unbiased ground truth generation, data visualization, machine learning pipeline automation and performance of open source packing static detectors. △ Less

Submitted 18 February, 2023; originally announced February 2023.

Timed I/O Automata: It is never too late to complete your timed specification theory

Authors: Martijn A. Goorden, Kim G. Larsen, Axel Legay, Florian Lorber, Ulrik Nyman, Andrzej Wasowski

Abstract: 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 f… ▽ More 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 backed by rigorous proofs and is being implemented in the open-source tool ECDAR. △ Less

Submitted 13 July, 2023; v1 submitted 9 February, 2023; originally announced February 2023.

Comments: Version submitted for review

Symbolic analysis meets federated learning to enhance malware identifier

Authors: Khanh Huu The Dam, Charles-Henry Bertrand Van Ouytsel, Axel Legay

Abstract: Over past years, the manually methods to create detection rules were no longer practical in the anti-malware product since the number of malware threats has been growing. Thus, the turn to the machine learning approaches is a promising way to make the malware recognition more efficient. The traditional centralized machine learning requires a large amount of data to train a model with excellent per… ▽ More Over past years, the manually methods to create detection rules were no longer practical in the anti-malware product since the number of malware threats has been growing. Thus, the turn to the machine learning approaches is a promising way to make the 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 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 malwares through the behavioural graphs, i.e., system call dependency graphs. It is based on a deep learning model including a graph autoencoder and a multi-classifier module. This model is trained by a secure learning protocol among clients to preserve the private data against the inference attacks. Using the model to identify malwares, we achieve the accuracy of 85\% for the homogeneous graph data and 93\% for the inhomogeneous graph data. △ Less

Submitted 29 April, 2022; originally announced April 2022.

Malware Analysis with Symbolic Execution and Graph Kernel

Authors: Charles-Henry Bertrand Van Ouytsel, Axel Legay

Abstract: Malware analysis techniques are divided into static and dynamic analysis. Both techniques can be bypassed by circumvention techniques such as obfuscation. In a series of works, the authors have promoted the use of symbolic executions combined with machine learning to avoid such traps. Most of those works rely on natural graph-based representations that can then be plugged into graph-based learning… ▽ More Malware analysis techniques are divided into static and dynamic analysis. Both techniques can be bypassed by circumvention techniques such as obfuscation. In a series of works, the authors have promoted the use of symbolic executions combined with machine learning to avoid such traps. Most of those works rely on natural graph-based representations that can then be plugged into graph-based learning algorithms such as Gspan. There are two main problems with this approach. The first one is in the cost of computing the graph. Indeed, working with graphs requires one to compute and representing the entire state-space of the file under analysis. As such computation is too cumbersome, the techniques often rely on develo** strategies to compute a representative subgraph of the behaviors. Unfortunately, efficient graph-building strategies remain weakly explored. The second problem is in the classification itself. Graph-based machine learning algorithms rely on comparing the biggest common structures. This sidelines small but specific parts of the malware signature. In addition, it does not allow us to work with efficient algorithms such as support vector machine. We propose a new efficient open source toolchain for machine learning-based classification. We also explore how graph-kernel techniques can be used in the process. We focus on the 1-dimensional Weisfeiler-Lehman kernel, which can capture local similarities between graphs. Our experimental results show that our approach outperforms existing ones by an impressive factor. △ Less

Submitted 12 April, 2022; originally announced April 2022.

Test Scenario Generation for Context-Oriented Programs

Authors: Pierre Martou, Kim Mens, Benoît Duhoux, Axel Legay

Abstract: Their highly adaptive nature and the combinatorial explosion of possible configurations makes testing context-oriented programs hard. We propose a methodology to automate the generation of test scenarios for developers of feature-based context-oriented programs. By using combinatorial interaction testing we generate a covering array from which a small but representative set of test scenarios can b… ▽ More Their highly adaptive nature and the combinatorial explosion of possible configurations makes testing context-oriented programs hard. We propose a methodology to automate the generation of test scenarios for developers of feature-based context-oriented programs. By using combinatorial interaction testing we generate a covering array from which a small but representative set of test scenarios can be inferred. By taking advantage of the explicit separation of contexts and features in such context-oriented programs, we can further rearrange the generated test scenarios to minimise the reconfiguration cost between subsequent scenarios. Finally, we explore how a previously generated test suite can be adapted incrementally when the system evolves to a new version. By validating these algorithms on a small use case, our initial results show that the proposed test generation approach is efficient and beneficial to developers to test and improve the design of context-oriented programs. △ Less

Submitted 24 September, 2021; originally announced September 2021.

Analysis of Source Code Using UPPAAL

Authors: Mitja Kulczynski, Axel Legay, Dirk Nowotka, Danny Bøgsted Poulsen

Abstract: In recent years there has been a considerable effort in optimising formal methods for application to code. This has been driven by tools such as CPAChecker, DIVINE, and CBMC. At the same time tools such as Uppaal have been massively expanding the realm of more traditional model checking technologies to include strategy synthesis algorithms - an aspect becoming more and more needed as software beco… ▽ More In recent years there has been a considerable effort in optimising formal methods for application to code. This has been driven by tools such as CPAChecker, DIVINE, and CBMC. At the same time tools such as Uppaal have been massively expanding the realm of more traditional model checking technologies to include strategy synthesis algorithms - an aspect becoming more and more needed as software becomes increasingly parallel. Instead of reimplementing the advances made by Uppaal in this area, we suggest in this paper to develop a bridge between the source code and the engine of Uppaal. Our approach uses the widespread intermediate language LLVM and makes recent advances of the Uppaal ecosystem readily available to analysis of source code. △ Less

Submitted 6 August, 2021; originally announced August 2021.

Comments: In Proceedings F-IDE 2021, arXiv:2108.02369

Journal ref: EPTCS 338, 2021, pp. 31-38

Analysis of Machine Learning Approaches to Packing Detection

Authors: Charles-Henry Bertrand Van Ouytsel, Thomas Given-Wilson, Jeremy Minet, Julian Roussieau, Axel Legay

Abstract: Packing is an obfuscation technique widely used by malware to hide the content and behavior of a program. Much prior research has explored how to detect whether a program is packed. This research includes a broad variety of approaches such as entropy analysis, syntactic signatures and more recently machine learning classifiers using various features. However, no robust results have indicated which… ▽ More Packing is an obfuscation technique widely used by malware to hide the content and behavior of a program. Much prior research has explored how to detect whether a program is packed. This research includes a broad variety of approaches such as entropy analysis, syntactic signatures and more recently machine learning classifiers using various features. However, no robust results have indicated which algorithms perform best, or which features are most significant. This is complicated by considering how to evaluate the results since accuracy, cost, generalization capabilities, and other measures are all reasonable. This work explores eleven different machine learning approaches using 119 features to understand: which features are most significant for packing detection; which algorithms offer the best performance; and which algorithms are most economical. △ Less

Submitted 2 May, 2021; originally announced May 2021.

Quantitative Security Risk Modeling and Analysis with RisQFLan

Authors: Maurice H. ter Beek, Axel Legay, Alberto Lluch Lafuente, Andrea Vandin

Abstract: 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 mod… ▽ More 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. △ Less

Submitted 21 January, 2021; originally announced January 2021.

A Decision Tree Lifted Domain for Analyzing Program Families with Numerical Features (Extended Version)

Authors: Aleksandar S. Dimovski, Sven Apel, Axel Legay

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… ▽ More 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 big domains, thus admitting astronomic configuration spaces. The key for an efficient lifted analysis is proper handling of variability-specific constructs of the language (e.g., feature-based runtime tests and #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^2Analyzer, for inferring invariants of C programs. It uses existing numerical domains (e.g., intervals, octagons, polyhedra) from the APRON library as parameters. An empirical evaluation on benchmarks from SV-COMP and BusyBox yields promising preliminary results indicating that our decision trees-based approach is effective and outperforms the tuple-based approach, which is used as a baseline lifted analysis based on abstract interpretation. △ Less

Submitted 10 December, 2020; originally announced December 2020.

Behavioral Specification Theories: an Algebraic Taxonomy

Authors: Uli Fahrenberg, Axel Legay

Abstract: We develop a taxonomy of different behavioral specification theories and expose their algebraic properties. We start by clarifying what precisely constitutes a behavioral specification theory and then introduce logical and structural operations and develop the resulting algebraic properties. In order to motivate our developments, we give plenty of examples of behavioral specification theories with… ▽ More We develop a taxonomy of different behavioral specification theories and expose their algebraic properties. We start by clarifying what precisely constitutes a behavioral specification theory and then introduce logical and structural operations and develop the resulting algebraic properties. In order to motivate our developments, we give plenty of examples of behavioral specification theories with different operations. △ Less

Submitted 23 September, 2020; originally announced September 2020.

Automatic Verification of LLVM Code

Authors: Axel Legay, Dirk Nowotka, Danny Bøgsted Poulsen

Abstract: In this work we present our work in develo** a software verification tool for llvm-code - Lodin - that incorporates both explicit-state model checking, statistical model checking and symbolic state model checking algorithms. In this work we present our work in develo** a software verification tool for llvm-code - Lodin - that incorporates both explicit-state model checking, statistical model checking and symbolic state model checking algorithms. △ Less

Submitted 4 June, 2020; originally announced June 2020.

Featured Games

Authors: Uli Fahrenberg, Axel Legay

Abstract: Feature-based SPL analysis 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. In their FASE'20 paper, ter Be… ▽ More Feature-based SPL analysis 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. In their FASE'20 paper, ter Beek et al.\ introduce parity games with variability in order to develop family-based mu-calculus model checking of featured transition systems. We generalize their model to general featured games and show how these may be analysed in a family-based manner. We introduce featured reachability games, featured minimum reachability games, featured discounted games, featured energy games, and featured parity games. We show how to compute winners and values of such games in a family-based manner. We also show that all these featured games admit optimal featured strategies, which project to optimal strategies for any product. Further, we develop family-based algorithms, using late splitting, to compute winners, values, and optimal strategies for all the featured games we have introduced. △ Less

Submitted 13 May, 2020; v1 submitted 12 May, 2020; originally announced May 2020.

Computing Branching Distances Using Quantitative Games

Authors: Uli Fahrenberg, Axel Legay, Karin Quaas

Abstract: We lay out a general method for computing branching distances between labeled transition systems. We translate the quantitative games used for defining these distances to other, path-building games which are amenable to methods from the theory of quantitative games. We then show for all common types of branching distances how the resulting path-building games can be solved. In the end, we achieve… ▽ More We lay out a general method for computing branching distances between labeled transition systems. We translate the quantitative games used for defining these distances to other, path-building games which are amenable to methods from the theory of quantitative games. We then show for all common types of branching distances how the resulting path-building games can be solved. In the end, we achieve a method which can be used to compute all branching distances in the linear-time--branching-time spectrum. △ Less

Submitted 20 October, 2019; originally announced October 2019.

Secure Architectures Implementing Trusted Coalitions for Blockchained Distributed Learning (TCLearn)

Authors: Sebastien Lugan, Paul Desbordes, Luis Xavier Ramos Tormo, Axel Legay, Benoit Macq

Abstract: Distributed learning across a coalition of organizations allows the members of the coalition to train and share a model without sharing the data used to optimize this model. In this paper, we propose new secure architectures that guarantee preservation of data privacy, trustworthy sequence of iterative learning and equitable sharing of the learned model among each member of the coalition by using… ▽ More Distributed learning across a coalition of organizations allows the members of the coalition to train and share a model without sharing the data used to optimize this model. In this paper, we propose new secure architectures that guarantee preservation of data privacy, trustworthy sequence of iterative learning and equitable sharing of the learned model among each member of the coalition by using adequate encryption and blockchain mechanisms. We exemplify its deployment in the case of the distributed optimization of a deep learning convolutional neural network trained on medical images. △ Less

Submitted 18 June, 2019; originally announced June 2019.

Journal ref: IEEE Access, vol. 7, pp. 181789-181799, 2019

Sequential Relational Decomposition

Authors: Dror Fried, Axel Legay, Joël Ouaknine, Moshe Y. Vardi

Abstract: 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 befo… ▽ More 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. △ Less

Submitted 2 March, 2022; v1 submitted 4 March, 2019; originally announced March 2019.

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 1 (March 3, 2022) lmcs:5250

Variability Abstraction and Refinement for Game-based Lifted Model Checking of full CTL (Extended Version)

Authors: Aleksandar S. Dimovski, Axel Legay, Andrzej Wasowski

Abstract: 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 spac… ▽ More 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. △ Less

Submitted 14 February, 2019; originally announced February 2019.

Hybrid Statistical Estimation of Mutual Information and its Application to Information Flow

Authors: Fabrizio Biondi, Yusuke Kawamoto, Axel Legay, Louis-Marie Traonouez

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 exhaustive precise analysis on all executions of the system. To avoid the high computational cost of such an exhaustive search, statistical analysis has been studied to efficiently obtain approximate estimates by analyzing on… ▽ More 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 exhaustive precise analysis on all executions of the system. To avoid the high computational cost of such an exhaustive search, statistical analysis has 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 a hybrid statistical estimation method that 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 new abstraction-then-sampling technique 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. △ Less

Submitted 8 September, 2018; originally announced September 2018.

Comments: Accepted by Formal Aspects of Computing

Journal ref: Formal Aspects of Computing, 31(2), pp.165-206, 2019

Formal Verification of Probabilistic SystemC Models with Statistical Model Checking

Authors: Van Chan Ngo, Axel Legay

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, e.g., random data and unreliable components. It thus is crucial to have both quantitative and qualitative analysis of the probabilities of system properties. Such analysis can be condu… ▽ More 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, e.g., random data and unreliable components. It thus is 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 (PMC). 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 (SMC) to carry out 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 (BLTL) 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 BLTL. 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 (MUV), the mechanism for automatically instrumenting the MUV, and the interaction with statistical model checking algorithms. △ Less

Submitted 4 December, 2017; originally announced December 2017.

Comments: Journal of Software: Evolution and Process. Wiley, 2017. arXiv admin note: substantial text overlap with arXiv:1507.08187

A framework for quantitative modeling and analysis of highly (re)configurable systems

Authors: Maurice H. ter Beek, Axel Legay, Alberto Lluch Lafuente, Andrea Vandin

Abstract: 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 fe… ▽ More 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. △ Less

Submitted 4 April, 2018; v1 submitted 26 July, 2017; originally announced July 2017.

Comments: major revision

Featured Weighted Automata

Authors: Uli Fahrenberg, Axel Legay

Abstract: A featured transition system is a transition system in which the transitions are annotated with feature expressions: Boolean expressions on a finite number of given features. Depending on its feature expression, each individual transition can be enabled when some features are present, and disabled for other sets of features. The behavior of a featured transition system hence depends on a given set… ▽ More A featured transition system is a transition system in which the transitions are annotated with feature expressions: Boolean expressions on a finite number of given features. Depending on its feature expression, each individual transition can be enabled when some features are present, and disabled for other sets of features. The behavior of a featured transition system hence depends on a given set of features. There are algorithms for featured transition systems which can check their properties for all sets of features at once, for example for LTL or CTL properties. Here we introduce a model of featured weighted automata which combines featured transition systems and (semiring-) weighted automata. We show that methods and techniques from weighted automata extend to featured weighted automata and devise algorithms to compute quantitative properties of featured weighted automata for all sets of features at once. We show applications to minimum reachability and to energy properties. △ Less

Submitted 27 February, 2017; v1 submitted 24 February, 2017; originally announced February 2017.

An $ω$-Algebra for Real-Time Energy Problems

Authors: David Cachera, Uli Fahrenberg, Axel Legay

Abstract: We develop a $^*$-continuous Kleene $ω$-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 $ω$-algebras and computability of certain manipulations on real-time energy functions, it follows that rea… ▽ More We develop a $^*$-continuous Kleene $ω$-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 $ω$-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. △ Less

Submitted 23 May, 2019; v1 submitted 30 January, 2017; originally announced January 2017.

Journal ref: Logical Methods in Computer Science, Volume 15, Issue 2 (May 24, 2019) lmcs:2677

Verification of interlocking systems using statistical model checking

Authors: Quentin Cappart, Christophe Limbree, Pierre Schaus, Jean Quilbeuf, Louis-Marie Traonouez, Axel Legay

Abstract: In the railway domain, an interlocking is the system ensuring safe train traffic inside a station by controlling its active elements such as the signals or points. Modern interlockings are configured using particular data, called application data, reflecting the track layout and defining the actions that the interlocking can take. The safety of the train traffic relies thereby on application data… ▽ More In the railway domain, an interlocking is the system ensuring safe train traffic inside a station by controlling its active elements such as the signals or points. Modern interlockings are configured using particular data, called application data, reflecting the track layout and defining the actions that the interlocking can take. The safety of the train traffic relies thereby on application data correctness, errors inside them can cause safety issues such as derailments or collisions. Given the high level of safety required by such a system, its verification is a critical concern. In addition to the safety, an interlocking must also ensure that availability properties, stating that no train would be stopped forever in a station, are satisfied. Most of the research dealing with this verification relies on model checking. However, due to the state space explosion problem, this approach does not scale for large stations. More recently, a discrete event simulation approach limiting the verification to a set of likely scenarios, was proposed. The simulation enables the verification of larger stations, but with no proof that all the interesting scenarios are covered by the simulation. In this paper, we apply an intermediate statistical model checking approach, offering both the advantages of model checking and simulation. Even if exhaustiveness is not obtained, statistical model checking evaluates with a parametrizable confidence the reliability and the availability of the entire system. △ Less

Submitted 4 August, 2017; v1 submitted 9 May, 2016; originally announced May 2016.

Comments: 12 pages, 3 figures, 2 tables

Journal ref: IEEE 18th International Symposium on High Assurance Systems Engineering (HASE), Singapore, pp. 61-68 (2017)

Long-Term Average Cost in Featured Transition Systems

Authors: Rafael Olaechea, Uli Fahrenberg, Joanne M. Atlee, Axel Legay

Abstract: 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 p… ▽ More 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 this paper we adapt the standard algorithm for computing limit average cost of a weighted transition system to software product lines. Limit average is a useful and popular measure for the long-term average behavior of a quality attribute such as performance or energy consumption, but has hitherto not been available for family-based analysis of software product lines. Our algorithm operates on weighted featured transition systems, at a symbolic level, and computes limit average cost for all products in a software product line at the same time. We have implemented the algorithm and evaluated it on several examples. △ Less

Submitted 22 April, 2016; originally announced April 2016.

A Linear-Time Branching-Time Spectrum for Behavioral Specification Theories

Authors: Uli Fahrenberg, Axel Legay

Abstract: We propose behavioral specification theories for most equivalences in the linear-time--branching-time spectrum. Almost all previous work on specification theories focuses on bisimilarity, but there is a clear interest in specification theories for other preorders and equivalences. We show that specification theories for preorders cannot exist and develop a general scheme which allows us to define… ▽ More We propose behavioral specification theories for most equivalences in the linear-time--branching-time spectrum. Almost all previous work on specification theories focuses on bisimilarity, but there is a clear interest in specification theories for other preorders and equivalences. We show that specification theories for preorders cannot exist and develop a general scheme which allows us to define behavioral specification theories, based on disjunctive modal transition systems, for most equivalences in the linear-time--branching-time spectrum. △ Less

Submitted 18 October, 2019; v1 submitted 21 April, 2016; originally announced April 2016.

*-Continuous Kleene $ω$-Algebras for Energy Problems

Authors: Zoltán Ésik, Uli Fahrenberg, Axel Legay

Abstract: Energy problems are important in the formal analysis of embedded or autonomous systems. Using recent results on star-continuous Kleene omega-algebras, we show here that energy problems can be solved by algebraic manipulations on the transition matrix of energy automata. To this end, we prove general results about certain classes of finitely additive functions on complete lattices which should be… ▽ More Energy problems are important in the formal analysis of embedded or autonomous systems. Using recent results on star-continuous Kleene omega-algebras, we show here that energy problems can be solved by algebraic manipulations on the transition matrix of energy automata. To this end, we prove general results about certain classes of finitely additive functions on complete lattices which should be of a more general interest. △ Less

Submitted 10 September, 2015; originally announced September 2015.

Comments: In Proceedings FICS 2015, arXiv:1509.02826

Journal ref: EPTCS 191, 2015, pp. 48-59

On the Expressiveness of Joining

Authors: Thomas Given-Wilson, Axel Legay

Abstract: The expressiveness of communication primitives has been explored in a common framework based on the pi-calculus by considering four features: synchronism (asynchronous vs synchronous), arity (monadic vs polyadic data), communication medium (shared dataspaces vs channel-based), and pattern-matching (binding to a name vs testing name equality vs intensionality). Here another dimension coordination i… ▽ More The expressiveness of communication primitives has been explored in a common framework based on the pi-calculus by considering four features: synchronism (asynchronous vs synchronous), arity (monadic vs polyadic data), communication medium (shared dataspaces vs channel-based), and pattern-matching (binding to a name vs testing name equality vs intensionality). Here another dimension coordination is considered that accounts for the number of processes required for an interaction to occur. Coordination generalises binary languages such as pi-calculus to joining languages that combine inputs such as the Join Calculus and general rendezvous calculus. By means of possibility/impossibility of encodings, this paper shows coordination is unrelated to the other features. That is, joining languages are more expressive than binary languages, and no combination of the other features can encode a joining language into a binary language. Further, joining is not able to encode any of the other features unless they could be encoded otherwise. △ Less

Submitted 19 August, 2015; originally announced August 2015.

Comments: In Proceedings ICE 2015, arXiv:1508.04595. arXiv admin note: substantial text overlap with arXiv:1408.1455

ACM Class: F.1.2; D.3.3

Journal ref: EPTCS 189, 2015, pp. 99-113

Dependability Analysis of Control Systems using SystemC and Statistical Model Checking

Authors: Van Chan Ngo, Axel Legay

Abstract: Stochastic Petri nets are commonly used for modeling distributed systems in order to study their performance and dependability. This paper proposes a realization of stochastic Petri nets in SystemC for modeling large embedded control systems. Then statistical model checking is used to analyze the dependability of the constructed model. Our verification framework allows users to express a wide rang… ▽ More Stochastic Petri nets are commonly used for modeling distributed systems in order to study their performance and dependability. This paper proposes a realization of stochastic Petri nets in SystemC for modeling large embedded control systems. Then statistical model checking is used to analyze the dependability of the constructed model. Our verification framework allows users to express a wide range of useful properties to be verified which is illustrated through a case study. △ Less

Submitted 25 February, 2016; v1 submitted 29 July, 2015; originally announced July 2015.

Model Checking as Control: Feedback Control for Statistical Model Checking of Cyber-Physical Systems

Authors: Kenan Kalajdzic, Cyrille Jegourel, Ezio Bartocci, Axel Legay, Scott A. Smolka, Radu Grosu

Abstract: We introduce feedback-control statistical system checking (FC-SSC), a new approach to statistical model checking that exploits principles of feedback-control for the analysis of cyber-physical systems (CPS). FC-SSC uses stochastic system identification to learn a CPS model, importance sampling to estimate the CPS state, and importance splitting to control the CPS so that the probability that the C… ▽ More We introduce feedback-control statistical system checking (FC-SSC), a new approach to statistical model checking that exploits principles of feedback-control for the analysis of cyber-physical systems (CPS). FC-SSC uses stochastic system identification to learn a CPS model, importance sampling to estimate the CPS state, and importance splitting to control the CPS so that the probability that the CPS satisfies a given property can be efficiently inferred. We illustrate the utility of FC-SSC on two example applications, each of which is simple enough to be easily understood, yet complex enough to exhibit all of FC-SCC's features. To the best of our knowledge, FC-SSC is the first statistical system checker to efficiently estimate the probability of rare events in realistic CPS applications or in any complex probabilistic program whose model is either not available, or is infeasible to derive through static-analysis techniques. △ Less

Submitted 12 June, 2015; v1 submitted 24 April, 2015; originally announced April 2015.

Comments: There are somethings to be checked more carefully

Quantitative Analysis of Probabilistic Models of Software Product Lines with Statistical Model Checking

Authors: Maurice H. ter Beek, Axel Legay, Alberto Lluch Lafuente, Andrea Vandin

Abstract: We investigate the suitability of statistical model checking techniques for analysing quantitative properties of software product line models with probabilistic aspects. For this purpose, we enrich the feature-oriented language FLan with action rates, which specify the likelihood of exhibiting particular behaviour or of installing features at a specific moment or in a specific order. The enriche… ▽ More We investigate the suitability of statistical model checking techniques for analysing quantitative properties of software product line models with probabilistic aspects. For this purpose, we enrich the feature-oriented language FLan with action rates, which specify the likelihood of exhibiting particular behaviour or of installing features at a specific moment or in a specific order. The enriched language (called PFLan) allows us to specify models of software product lines with probabilistic configurations and behaviour, e.g. by considering a PFLan semantics based on discrete-time Markov chains. The Maude implementation of PFLan is combined with the distributed statistical model checker MultiVeStA to perform quantitative analyses of a simple product line case study. The presented analyses include the likelihood of certain behaviour of interest (e.g. product malfunctioning) and the expected average cost of products. △ Less

Submitted 14 April, 2015; originally announced April 2015.

Comments: In Proceedings FMSPLE 2015, arXiv:1504.03014

ACM Class: D.2.4; F.3.1; F.3.2; G.3

Journal ref: EPTCS 182, 2015, pp. 56-70

Distributed Verification of Rare Properties using Importance Splitting Observers

Authors: Cyrille Jegourel, Axel Legay, Sean Sedwards, Louis-Marie Traonouez

Abstract: Rare properties remain a challenge for statistical model checking (SMC) due to the quadratic scaling of variance with rarity. We address this with a variance reduction framework based on lightweight importance splitting observers. These expose the model-property automaton to allow the construction of score functions for high performance algorithms. The confidence intervals defined for importance… ▽ More Rare properties remain a challenge for statistical model checking (SMC) due to the quadratic scaling of variance with rarity. We address this with a variance reduction framework based on lightweight importance splitting observers. These expose the model-property automaton to allow the construction of score functions for high performance algorithms. The confidence intervals defined for importance splitting make it appealing for SMC, but optimising its performance in the standard way makes distribution inefficient. We show how it is possible to achieve equivalently good results in less time by distributing simpler algorithms. We first explore the challenges posed by importance splitting and present an algorithm optimised for distribution. We then define a specific bounded time logic that is compiled into memory-efficient observers to monitor executions. Finally, we demonstrate our framework on a number of challenging case studies. △ Less

Submitted 28 April, 2015; v1 submitted 6 February, 2015; originally announced February 2015.

*-Continuous Kleene $ω$-Algebras

Authors: Zoltán Ésik, Uli Fahrenberg, Axel Legay

Abstract: We define and study basic properties of *-continuous Kleene $ω$-algebras that involve a *-continuous Kleene algebra with a *-continuous action on a semimodule and an infinite product operation that is also *-continuous. We show that *-continuous Kleene $ω$-algebras give rise to iteration semiring-semimodule pairs. We show how our work can be applied to solve certain energy problems for hybrid syst… ▽ More We define and study basic properties of *-continuous Kleene $ω$-algebras that involve a *-continuous Kleene algebra with a *-continuous action on a semimodule and an infinite product operation that is also *-continuous. We show that *-continuous Kleene $ω$-algebras give rise to iteration semiring-semimodule pairs. We show how our work can be applied to solve certain energy problems for hybrid systems. △ Less

Submitted 6 January, 2015; originally announced January 2015.

Dynamic Verification of SystemC with Statistical Model Checking

Authors: Van Chan Ngo, Axel Legay, Jean Quilbeuf

Abstract: Many embedded and real-time systems have a inherent probabilistic behaviour (sensors data, unreliable hardware,...). In that context, it is crucial to evaluate system properties such as "the probability that a particular hardware fails". Such properties can be evaluated by using probabilistic model checking. However, this technique fails on models representing realistic embedded and real-time syst… ▽ More Many embedded and real-time systems have a inherent probabilistic behaviour (sensors data, unreliable hardware,...). In that context, it is crucial to evaluate system properties such as "the probability that a particular hardware fails". Such properties can be evaluated by using probabilistic model checking. However, this technique fails on models representing realistic embedded and real-time systems because of the state space explosion. To overcome this problem, we propose a verification framework based on Statistical Model Checking. Our framework is able to evaluate probabilistic and temporal properties on large systems modelled in SystemC, a standard system-level modelling language. It is fully implemented as an extension of the Plasma-lab statistical model checker. We illustrate our approach on a multi-lift system case study. △ Less

Submitted 21 September, 2015; v1 submitted 2 December, 2014; originally announced December 2014.

Lightweight Monte Carlo Verification of Markov Decision Processes with Rewards

Authors: Axel Legay, Sean Sedwards, Louis-Marie Traonouez

Abstract: Markov decision processes are useful models of concurrency optimisation problems, but are often intractable for exhaustive verification methods. Recent work has introduced lightweight approximative techniques that sample directly from scheduler space, bringing the prospect of scalable alternatives to standard numerical model checking algorithms. The focus so far has been on optimising the probabil… ▽ More Markov decision processes are useful models of concurrency optimisation problems, but are often intractable for exhaustive verification methods. Recent work has introduced lightweight approximative techniques that sample directly from scheduler space, bringing the prospect of scalable alternatives to standard numerical model checking algorithms. The focus so far has been on optimising the probability of a property, but many problems require quantitative analysis of rewards. In this work we therefore present lightweight statistical model checking algorithms to optimise the rewards of Markov decision processes. We consider the standard definitions of rewards used in model checking, introducing an auxiliary hypothesis test to accommodate reachability rewards. We demonstrate the performance of our approach on a number of standard case studies. △ Less

Submitted 23 March, 2015; v1 submitted 20 October, 2014; originally announced October 2014.

Comments: 16 pages, 4 figures, 1 table

Homotopy Bisimilarity for Higher-Dimensional Automata

Authors: Uli Fahrenberg, Axel Legay

Abstract: We introduce a new category of higher-dimensional automata in which the morphisms are functional homotopy simulations, i.e. functional simulations up to concurrency of independent events. For this, we use unfoldings of higher-dimensional automata into higher-dimensional trees. Using a notion of open maps in this category, we define homotopy bisimilarity. We show that homotopy bisimilarity is equiv… ▽ More We introduce a new category of higher-dimensional automata in which the morphisms are functional homotopy simulations, i.e. functional simulations up to concurrency of independent events. For this, we use unfoldings of higher-dimensional automata into higher-dimensional trees. Using a notion of open maps in this category, we define homotopy bisimilarity. We show that homotopy bisimilarity is equivalent to a straight-forward generalization of standard bisimilarity to higher dimensions, and that it is finer than split bisimilarity and incomparable with history-preserving bisimilarity. △ Less

Submitted 20 September, 2014; originally announced September 2014.

Comments: Heavily revised version of arXiv:1209.4927

Smart Sampling for Lightweight Verification of Markov Decision Processes

Authors: Pedro D'Argenio, Axel Legay, Sean Sedwards, Louis-Marie Traonouez

Abstract: Markov decision processes (MDP) are useful to model optimisation problems in concurrent systems. To verify MDPs with efficient Monte Carlo techniques requires that their nondeterminism be resolved by a scheduler. Recent work has introduced the elements of lightweight techniques to sample directly from scheduler space, but finding optimal schedulers by simple sampling may be inefficient. Here we de… ▽ More Markov decision processes (MDP) are useful to model optimisation problems in concurrent systems. To verify MDPs with efficient Monte Carlo techniques requires that their nondeterminism be resolved by a scheduler. Recent work has introduced the elements of lightweight techniques to sample directly from scheduler space, but finding optimal schedulers by simple sampling may be inefficient. Here we describe "smart" sampling algorithms that can make substantial improvements in performance. △ Less

Submitted 4 February, 2015; v1 submitted 7 September, 2014; originally announced September 2014.

Comments: IEEE conference style, 11 pages, 5 algorithms, 11 figures, 1 table

Compositionality for Quantitative Specifications

Authors: Uli Fahrenberg, Jan Křetínský, Axel Legay, Louis-Marie Traonouez

Abstract: We provide a framework for compositional and iterative design and verification of systems with quantitative information, such as rewards, time or energy. It is based on disjunctive modal transition systems where we allow actions to bear various types of quantitative information. Throughout the design process the actions can be further refined and the information made more precise. We show how to c… ▽ More We provide a framework for compositional and iterative design and verification of systems with quantitative information, such as rewards, time or energy. It is based on disjunctive modal transition systems where we allow actions to bear various types of quantitative information. Throughout the design process the actions can be further refined and the information made more precise. We show how to compute the results of standard operations on the systems, including the quotient (residual), which has not been previously considered for quantitative non-deterministic systems. Our quantitative framework has close connections to the modal nu-calculus and is compositional with respect to general notions of distances between systems and the standard operations. △ Less

Submitted 8 February, 2017; v1 submitted 6 August, 2014; originally announced August 2014.

State Machine Flattening: Map** Study and Assessment

Authors: Xavier Devroey, Gilles Perrouin, Maxime Cordy, Axel Legay, Pierre-Yves Schobbens, Patrick Heymans

Abstract: State machine formalisms equipped with hierarchy and parallelism allow to compactly model complex system behaviours. Such models can then be transformed into executable code or inputs for model-based testing and verification techniques. Generated artifacts are mostly flat descriptions of system behaviour. \emph{Flattening} is thus an essential step of these transformations. To assess the importanc… ▽ More State machine formalisms equipped with hierarchy and parallelism allow to compactly model complex system behaviours. Such models can then be transformed into executable code or inputs for model-based testing and verification techniques. Generated artifacts are mostly flat descriptions of system behaviour. \emph{Flattening} is thus an essential step of these transformations. To assess the importance of flattening, we have defined and applied a systematic map** process and 30 publications were finally selected. However, it appeared that flattening is rarely the sole focus of the publications and that care devoted to the description and validation of flattening techniques varies greatly. Preliminary assessment of associated tool support indicated limited tool availability and scalability on challenging models. We see this initial investigation as a first step towards generic flattening techniques and scalable tool support, cornerstones of reliable model-based behavioural development. △ Less

Submitted 21 March, 2014; originally announced March 2014.

Measuring Global Similarity between Texts

Authors: Uli Fahrenberg, Fabrizio Biondi, Kevin Corre, Cyrille Jegourel, Simon Kongshøj, Axel Legay

Abstract: We propose a new similarity measure between texts which, contrary to the current state-of-the-art approaches, takes a global view of the texts to be compared. We have implemented a tool to compute our textual distance and conducted experiments on several corpuses of texts. The experiments show that our methods can reliably identify different global types of texts. We propose a new similarity measure between texts which, contrary to the current state-of-the-art approaches, takes a global view of the texts to be compared. We have implemented a tool to compute our textual distance and conducted experiments on several corpuses of texts. The experiments show that our methods can reliably identify different global types of texts. △ Less

Submitted 14 May, 2014; v1 submitted 17 March, 2014; originally announced March 2014.

Comments: Submitted to SLSP 2014

Structural Refinement for the Modal nu-Calculus

Authors: Uli Fahrenberg, Axel Legay, Louis-Marie Traonouez

Abstract: We introduce a new notion of structural refinement, a sound abstraction of logical implication, for the modal nu-calculus. Using new translations between the modal nu-calculus and disjunctive modal transition systems, we show that these two specification formalisms are structurally equivalent. Using our translations, we also transfer the structural operations of composition and quotient from dis… ▽ More We introduce a new notion of structural refinement, a sound abstraction of logical implication, for the modal nu-calculus. Using new translations between the modal nu-calculus and disjunctive modal transition systems, we show that these two specification formalisms are structurally equivalent. Using our translations, we also transfer the structural operations of composition and quotient from disjunctive modal transition systems to the modal nu-calculus. This shows that the modal nu-calculus supports composition and decomposition of specifications. △ Less

Submitted 10 June, 2014; v1 submitted 10 February, 2014; originally announced February 2014.

Comments: Accepted at ICTAC 2014

SoS contract verification using statistical model checking

Authors: Alessandro Mignogna, Leonardo Mangeruca, Benoît Boyer, Axel Legay, Alexandre Arnold

Abstract: Exhaustive formal verification for systems of systems (SoS) is impractical and cannot be applied on a large scale. In this paper we propose to use statistical model checking for efficient verification of SoS. We address three relevant aspects for systems of systems: 1) the model of the SoS, which includes stochastic aspects; 2) the formalization of the SoS requirements in the form of contracts; 3)… ▽ More Exhaustive formal verification for systems of systems (SoS) is impractical and cannot be applied on a large scale. In this paper we propose to use statistical model checking for efficient verification of SoS. We address three relevant aspects for systems of systems: 1) the model of the SoS, which includes stochastic aspects; 2) the formalization of the SoS requirements in the form of contracts; 3) the tool-chain to support statistical model checking for SoS. We adapt the SMC technique for application to heterogeneous SoS. We extend the UPDM/SysML specification language to express the SoS requirements that the implemented strategies over the SoS must satisfy. The requirements are specified with a new contract language specifically designed for SoS, targeting a high-level English- pattern language, but relying on an accurate semantics given by the standard temporal logics. The contracts are verified against the UPDM/SysML specification using the Statistical Model Checker (SMC) PLASMA combined with the simulation engine DESYRE, which integrates heterogeneous behavioral models through the functional mock-up interface (FMI) standard. The tool-chain allows computing an estimation of the satisfiability of the contracts by the SoS. The results help the system architect to trade-off different solutions to guide the evolution of the SoS. △ Less

Submitted 14 November, 2013; originally announced November 2013.

Comments: In Proceedings AiSoS 2013, arXiv:1311.3195

Journal ref: EPTCS 133, 2013, pp. 67-83

Contracts and Behavioral Patterns for SoS: The EU IP DANSE approach

Authors: Alexandre Arnold, Benoît Boyer, Axel Legay

Abstract: This paper presents some of the results of the first year of DANSE, one of the first EU IP projects dedicated to SoS. Concretely, we offer a tool chain that allows to specify SoS and SoS requirements at high level, and analyse them using powerful toolsets coming from the formal verification area. At the high level, we use UPDM, the system model provided by the british army as well as a new type of… ▽ More This paper presents some of the results of the first year of DANSE, one of the first EU IP projects dedicated to SoS. Concretely, we offer a tool chain that allows to specify SoS and SoS requirements at high level, and analyse them using powerful toolsets coming from the formal verification area. At the high level, we use UPDM, the system model provided by the british army as well as a new type of contract based on behavioral patterns. At low level, we rely on a powerful simulation toolset combined with recent advances from the area of statistical model checking. The approach has been applied to a case study developed at EADS Innovation Works. △ Less

Submitted 14 November, 2013; originally announced November 2013.

Comments: In Proceedings AiSoS 2013, arXiv:1311.3195

Journal ref: EPTCS 133, 2013, pp. 47-66

Proceedings 1st Workshop on Advances in Systems of Systems

Authors: Kim G. Larsen, Axel Legay, Ulrik Nyman

Abstract: This volume contains the proceedings of the first workshop on Advances in Systems of Systems (AISOS'13), held in Roma, Italy, March 16. System-of-Systems describes the large scale integration of many independent self-contained systems to satisfy global needs or multi-system requests. Examples are smart grid, intelligent buildings, smart cities, transport systems, etc. There is a need for new mode… ▽ More This volume contains the proceedings of the first workshop on Advances in Systems of Systems (AISOS'13), held in Roma, Italy, March 16. System-of-Systems describes the large scale integration of many independent self-contained systems to satisfy global needs or multi-system requests. Examples are smart grid, intelligent buildings, smart cities, transport systems, etc. There is a need for new modeling formalisms, analysis methods and tools to help make trade-off decisions during design and evolution avoiding leading to sub-optimal design and rework during integration and in service. The workshop should focus on the modeling and analysis of System of Systems. AISOS'13 aims to gather people from different communities in order to encourage exchange of methods and views. △ Less

Submitted 13 November, 2013; originally announced November 2013.

Journal ref: EPTCS 133, 2013

Verification for Reliable Product Lines

Authors: Maxime Cordy, Patrick Heymans, Pierre-Yves Schobbens, Amir Molzam Sharifloo, Carlo Ghezzi, Axel Legay

Abstract: Many product lines are critical, and therefore reliability is a vital part of their requirements. Reliability is a probabilistic property. We therefore propose a model for feature-aware discrete-time Markov chains as a basis for verifying probabilistic properties of product lines, including reliability. We compare three verification techniques: The enumerative technique uses PRISM, a state-of-the-… ▽ More Many product lines are critical, and therefore reliability is a vital part of their requirements. Reliability is a probabilistic property. We therefore propose a model for feature-aware discrete-time Markov chains as a basis for verifying probabilistic properties of product lines, including reliability. We compare three verification techniques: The enumerative technique uses PRISM, a state-of-the-art symbolic probabilistic model checker, on each product. The parametric technique exploits our recent advances in parametric model checking. Finally, we propose a new bounded technique that performs a single bounded verification for the whole product line, and thus takes advantage of the common behaviours of the product line. Experimental results confirm the advantages of the last two techniques. △ Less

Submitted 6 November, 2013; originally announced November 2013.

Scalable Verification of Markov Decision Processes

Authors: Axel Legay, Sean Sedwards, Louis-Marie Traonouez

Abstract: Markov decision processes (MDP) are useful to model concurrent process optimisation problems, but verifying them with numerical methods is often intractable. Existing approximative approaches do not scale well and are limited to memoryless schedulers. Here we present the basis of scalable verification for MDPSs, using an O(1) memory representation of history-dependent schedulers. We thus facilitat… ▽ More Markov decision processes (MDP) are useful to model concurrent process optimisation problems, but verifying them with numerical methods is often intractable. Existing approximative approaches do not scale well and are limited to memoryless schedulers. Here we present the basis of scalable verification for MDPSs, using an O(1) memory representation of history-dependent schedulers. We thus facilitate scalable learning techniques and the use of massively parallel verification. △ Less

Submitted 17 September, 2014; v1 submitted 14 October, 2013; originally announced October 2013.

Comments: V4: FMDS version, 12 pages, 4 figures

Towards Statistical Prioritization for Software Product Lines Testing

Authors: Xavier Devroey, Maxime Cordy, Gilles Perrouin, Pierre-Yves Schobbens, Axel Legay, Patrick Heymans

Abstract: Software Product Lines (SPL) are inherently difficult to test due to the combinatorial explosion of the number of products to consider. To reduce the number of products to test, sampling techniques such as combinatorial interaction testing have been proposed. They usually start from a feature model and apply a coverage criterion (e.g. pairwise feature interaction or dissimilarity) to generate trac… ▽ More Software Product Lines (SPL) are inherently difficult to test due to the combinatorial explosion of the number of products to consider. To reduce the number of products to test, sampling techniques such as combinatorial interaction testing have been proposed. They usually start from a feature model and apply a coverage criterion (e.g. pairwise feature interaction or dissimilarity) to generate tractable, fault-finding, lists of configurations to be tested. Prioritization can also be used to sort/generate such lists, optimizing coverage criteria or weights assigned to features. However, current sampling/prioritization techniques barely take product behavior into account. We explore how ideas of statistical testing, based on a usage model (a Markov chain), can be used to extract configurations of interest according to the likelihood of their executions. These executions are gathered in featured transition systems, compact representation of SPL behavior. We discuss possible scenarios and give a prioritization procedure illustrated on an example. △ Less

Submitted 23 January, 2014; v1 submitted 9 October, 2013; originally announced October 2013.

Comments: Extended version published at VaMoS '14 (http://dx.doi.org/10.1145/2556624.2556635)

Tropical Fourier-Motzkin elimination, with an application to real-time verification

Authors: Xavier Allamigeon, Uli Fahrenberg, Stéphane Gaubert, Ricardo D. Katz, Axel Legay

Abstract: We introduce a generalization of tropical polyhedra able to express both strict and non-strict inequalities. Such inequalities are handled by means of a semiring of germs (encoding infinitesimal perturbations). We develop a tropical analogue of Fourier-Motzkin elimination from which we derive geometrical properties of these polyhedra. In particular, we show that they coincide with the tropically c… ▽ More We introduce a generalization of tropical polyhedra able to express both strict and non-strict inequalities. Such inequalities are handled by means of a semiring of germs (encoding infinitesimal perturbations). We develop a tropical analogue of Fourier-Motzkin elimination from which we derive geometrical properties of these polyhedra. In particular, we show that they coincide with the tropically convex union of (non-necessarily closed) cells that are convex both classically and tropically. We also prove that the redundant inequalities produced when performing successive elimination steps can be dynamically deleted by reduction to mean payoff game problems. As a complement, we provide a coarser (polynomial time) deletion procedure which is enough to arrive at a simply exponential bound for the total execution time. These algorithms are illustrated by an application to real-time systems (reachability analysis of timed automata). △ Less

Submitted 25 June, 2014; v1 submitted 9 August, 2013; originally announced August 2013.

Comments: 29 pages, 8 figures

MSC Class: 14T05; 52A01; 52B55

Journal ref: International Journal of Algebra and Computation, 24(5) :569-607, 2014

Kleene Algebras and Semimodules for Energy Problems

Authors: Zoltán Ésik, Uli Fahrenberg, Axel Legay, Karin Quaas

Abstract: With the purpose of unifying a number of approaches to energy problems found in the literature, we introduce generalized energy automata. These are finite automata whose edges are labeled with energy functions that define how energy levels evolve during transitions. Uncovering a close connection between energy problems and reachability and Büchi acceptance for semiring-weighted automata, we show t… ▽ More With the purpose of unifying a number of approaches to energy problems found in the literature, we introduce generalized energy automata. These are finite automata whose edges are labeled with energy functions that define how energy levels evolve during transitions. Uncovering a close connection between energy problems and reachability and Büchi acceptance for semiring-weighted automata, we show that these generalized energy problems are decidable. We also provide complexity results for important special cases. △ Less

Submitted 2 July, 2013; originally announced July 2013.

Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory

Authors: Nikola Beneš, Benoît Delahaye, Uli Fahrenberg, Jan Křetínský, Axel Legay

Abstract: There are two fundamentally different approaches to specifying and verifying properties of systems. The logical approach makes use of specifications given as formulae of temporal or modal logics and relies on efficient model checking algorithms; the behavioural approach exploits various equivalence or refinement checking methods, provided the specifications are given in the same formalism as imple… ▽ More There are two fundamentally different approaches to specifying and verifying properties of systems. The logical approach makes use of specifications given as formulae of temporal or modal logics and relies on efficient model checking algorithms; the behavioural approach exploits various equivalence or refinement checking methods, provided the specifications are given in the same formalism as implementations. In this paper we provide translations between the logical formalism of Hennessy-Milner logic with greatest fixed points and the behavioural formalism of disjunctive modal transition systems. We also introduce a new operation of quotient for the above equivalent formalisms, which is adjoint to structural composition and allows synthesis of missing specifications from partial implementations. This is a substantial generalisation of the quotient for deterministic modal transition systems defined in earlier papers. △ Less

Submitted 4 June, 2013; originally announced June 2013.

Refinement and Difference for Probabilistic Automata

Authors: Benoît Delahaye, Uli Fahrenberg, Kim G. Larsen, Axel Legay

Abstract: This paper studies a difference operator for stochastic systems whose specifications are represented by Abstract Probabilistic Automata (APAs). In the case refinement fails between two specifications, the target of this operator is to produce a specification APA that represents all witness PAs of this failure. Our contribution is an algorithm that allows to approximate the difference of two APAs… ▽ More This paper studies a difference operator for stochastic systems whose specifications are represented by Abstract Probabilistic Automata (APAs). In the case refinement fails between two specifications, the target of this operator is to produce a specification APA that represents all witness PAs of this failure. Our contribution is an algorithm that allows to approximate the difference of two APAs with arbitrary precision. Our technique relies on new quantitative notions of distances between APAs used to assess convergence of the approximations, as well as on an in-depth inspection of the refinement relation for APAs. The procedure is effective and not more complex to implement than refinement checking. △ Less

Submitted 25 August, 2014; v1 submitted 18 December, 2012; originally announced December 2012.

Journal ref: Logical Methods in Computer Science, Volume 10, Issue 3 (August 26, 2014) lmcs:942