-
ROBUST: 221 Bugs in the Robot Operating System
Authors:
Christopher S. Timperley,
Gijs van der Hoorn,
André Santos,
Harshavardhan Deshpande,
Andrzej Wąsowski
Abstract:
As robotic systems such as autonomous cars and delivery drones assume greater roles and responsibilities within society, the likelihood and impact of catastrophic software failure within those systems is increased.To aid researchers in the development of new methods to measure and assure the safety and quality of robotics software, we systematically curated a dataset of 221 bugs across 7 popular a…
▽ More
As robotic systems such as autonomous cars and delivery drones assume greater roles and responsibilities within society, the likelihood and impact of catastrophic software failure within those systems is increased.To aid researchers in the development of new methods to measure and assure the safety and quality of robotics software, we systematically curated a dataset of 221 bugs across 7 popular and diverse software systems implemented via the Robot Operating System (ROS). We produce historically accurate recreations of each of the 221 defective software versions in the form of Docker images, and use a grounded theory approach to examine and categorize their corresponding faults, failures, and fixes. Finally, we reflect on the implications of our findings and outline future research directions for the community.
△ Less
Submitted 4 April, 2024;
originally announced April 2024.
-
Uncertainty Driven Active Learning for Image Segmentation in Underwater Inspection
Authors:
Luiza Ribeiro Marnet,
Yury Brodskiy,
Stella Grasshof,
Andrzej Wasowski
Abstract:
Active learning aims to select the minimum amount of data to train a model that performs similarly to a model trained with the entire dataset. We study the potential of active learning for image segmentation in underwater infrastructure inspection tasks, where large amounts of data are typically collected. The pipeline inspection images are usually semantically repetitive but with great variations…
▽ More
Active learning aims to select the minimum amount of data to train a model that performs similarly to a model trained with the entire dataset. We study the potential of active learning for image segmentation in underwater infrastructure inspection tasks, where large amounts of data are typically collected. The pipeline inspection images are usually semantically repetitive but with great variations in quality. We use mutual information as the acquisition function, calculated using Monte Carlo dropout. To assess the effectiveness of the framework, DenseNet and HyperSeg are trained with the CamVid dataset using active learning. In addition, HyperSeg is trained with a pipeline inspection dataset of over 50,000 images. For the pipeline dataset, HyperSeg with active learning achieved 67.5% meanIoU using 12.5% of the data, and 61.4% with the same amount of randomly selected images. This shows that using active learning for segmentation models in underwater inspection tasks can lower the cost significantly.
△ Less
Submitted 20 March, 2024;
originally announced March 2024.
-
Exact and Efficient Bayesian Inference for Privacy Risk Quantification (Extended Version)
Authors:
Rasmus C. Rønneberg,
Raúl Pardo,
Andrzej Wąsowski
Abstract:
Data analysis has high value both for commercial and research purposes. However, disclosing analysis results may pose severe privacy risk to individuals. Privug is a method to quantify privacy risks of data analytics programs by analyzing their source code. The method uses probability distributions to model attacker knowledge and Bayesian inference to update said knowledge based on observable outp…
▽ More
Data analysis has high value both for commercial and research purposes. However, disclosing analysis results may pose severe privacy risk to individuals. Privug is a method to quantify privacy risks of data analytics programs by analyzing their source code. The method uses probability distributions to model attacker knowledge and Bayesian inference to update said knowledge based on observable outputs. Currently, Privug uses Markov Chain Monte Carlo (MCMC) to perform inference, which is a flexible but approximate solution. This paper presents an exact Bayesian inference engine based on multivariate Gaussian distributions to accurately and efficiently quantify privacy risks. The inference engine is implemented for a subset of Python programs that can be modeled as multivariate Gaussian models. We evaluate the method by analyzing privacy risks in programs to release public statistics. The evaluation shows that our method accurately and efficiently analyzes privacy risks, and outperforms existing methods. Furthermore, we demonstrate the use of our engine to analyze the effect of differential privacy in public statistics.
△ Less
Submitted 31 August, 2023;
originally announced August 2023.
-
Symbolic Semantics for Probabilistic Programs (extended version)
Authors:
Erik Voogd,
Einar Broch Johnsen,
Alexandra Silva,
Zachary J. Susag,
Andrzej Wąsowski
Abstract:
We present a new symbolic execution semantics of probabilistic programs that include observe statements and sampling from continuous distributions. Building on Kozen's seminal work, this symbolic semantics consists of a countable collection of measurable functions, along with a partition of the state space. We use the new semantics to provide a full correctness proof of symbolic execution for prob…
▽ More
We present a new symbolic execution semantics of probabilistic programs that include observe statements and sampling from continuous distributions. Building on Kozen's seminal work, this symbolic semantics consists of a countable collection of measurable functions, along with a partition of the state space. We use the new semantics to provide a full correctness proof of symbolic execution for probabilistic programs. We also implement this semantics in the tool symProb, and illustrate its use on examples.
△ Less
Submitted 19 July, 2023;
originally announced July 2023.
-
MROS: A framework for robot self-adaptation
Authors:
Gustavo Rezende Silva,
Darko Bozhinoski,
Mario Garzon Oviedo,
Mariano Ramírez Montero,
Nadia Hammoudeh Garcia,
Harshavardhan Deshpande,
Andrzej Wasowski,
Carlos Hernandez Corbato
Abstract:
Self-adaptation can be used in robotics to increase system robustness and reliability. This work describes the Metacontrol method for self-adaptation in robotics. Particularly, it details how the MROS (Metacontrol for ROS Systems) framework implements and packages Metacontrol, and it demonstrate how MROS can be applied in a navigation scenario where a mobile robot navigates in a factory floor. Vid…
▽ More
Self-adaptation can be used in robotics to increase system robustness and reliability. This work describes the Metacontrol method for self-adaptation in robotics. Particularly, it details how the MROS (Metacontrol for ROS Systems) framework implements and packages Metacontrol, and it demonstrate how MROS can be applied in a navigation scenario where a mobile robot navigates in a factory floor. Video: https://www.youtube.com/watch?v=ISe9aMskJuE
△ Less
Submitted 16 March, 2023;
originally announced March 2023.
-
Autonomy Is An Acquired Taste: Exploring Developer Preferences for GitHub Bots
Authors:
Amir Ghorbani,
Nathan Cassee,
Derek Robinson,
Adam Alami,
Neil A. Ernst,
Alexander Serebrenik,
Andrzej Wasowski
Abstract:
Software bots fulfill an important role in collective software development, and their adoption by developers promises increased productivity. Past research has identified that bots that communicate too often can irritate developers, which affects the utility of the bot. However, it is not clear what other properties of human-bot collaboration affect developers' preferences, or what impact these pr…
▽ More
Software bots fulfill an important role in collective software development, and their adoption by developers promises increased productivity. Past research has identified that bots that communicate too often can irritate developers, which affects the utility of the bot. However, it is not clear what other properties of human-bot collaboration affect developers' preferences, or what impact these properties might have. The main idea of this paper is to explore characteristics affecting developer preferences for interactions between humans and bots, in the context of GitHub pull requests. We carried out an exploratory sequential study with interviews and a subsequent vignette-based survey. We find developers generally prefer bots that are personable but show little autonomy, however, more experienced developers tend to prefer more autonomous bots. Based on this empirical evidence, we recommend bot developers increase configuration options for bots so that individual developers and projects can configure bots to best align with their own preferences and project cultures.
△ Less
Submitted 9 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.
-
Privacy with Good Taste: A Case Study in Quantifying Privacy Risks in Genetic Scores
Authors:
Raúl Pardo,
Willard Rafnsson,
Gregor Steinhorn,
Denis Lavrov,
Thomas Lumley,
Christian W. Probst,
Ilze Ziedins,
Andrzej Wąsowski
Abstract:
Analysis of genetic data opens up many opportunities for medical and scientific advances. The use of phenotypic information and polygenic risk scores to analyze genetic data is widespread. Most work on genetic privacy focuses on basic genetic data such as SNP values and specific genotypes. In this paper, we introduce a novel methodology to quantify and prevent privacy risks by focusing on polygeni…
▽ More
Analysis of genetic data opens up many opportunities for medical and scientific advances. The use of phenotypic information and polygenic risk scores to analyze genetic data is widespread. Most work on genetic privacy focuses on basic genetic data such as SNP values and specific genotypes. In this paper, we introduce a novel methodology to quantify and prevent privacy risks by focusing on polygenic scores and phenotypic information. Our methodology is based on the tool-supported privacy risk analysis method Privug. We demonstrate the use of Privug to assess privacy risks posed by disclosing a polygenic trait score for bitter taste receptors, encoded by TAS2R38 and TAS2R16, to a person's privacy in regards to their ethnicity. We provide an extensive privacy risks analysis of different programs for genetic data disclosure: taster phenotype, tasting polygenic score, and a polygenic score distorted with noise. Finally, we discuss the privacy/utility trade-offs of the polygenic score.
△ Less
Submitted 26 August, 2022;
originally announced August 2022.
-
Behavior Trees and State Machines in Robotics Applications
Authors:
Razan Ghzouli,
Thorsten Berger,
Einar Broch Johnsen,
Andrzej Wasowski,
Swaib Dragule
Abstract:
Autonomous robots combine skills to form increasingly complex behaviors, called missions. While skills are often programmed at a relatively low abstraction level, their coordination is architecturally separated and often expressed in higher-level languages or frameworks. State machines have been the go-to language to model behavior for decades, but recently, behavior trees have gained attention am…
▽ More
Autonomous robots combine skills to form increasingly complex behaviors, called missions. While skills are often programmed at a relatively low abstraction level, their coordination is architecturally separated and often expressed in higher-level languages or frameworks. State machines have been the go-to language to model behavior for decades, but recently, behavior trees have gained attention among roboticists. Although several implementations of behavior trees are in use, little is known about their usage and scope in the real world.How do concepts offered by behavior trees relate to traditional languages, such as state machines? How are concepts in behavior trees and state machines used in actual applications? This paper is a study of the key language concepts in behavior trees as realized in domain-specific languages (DSLs), internal and external DSLs offered as libraries, and their use in open-source robotic applications supported by the Robot Operating System (ROS). We analyze behavior-tree DSLs and compare them to the standard language for behavior models in robotics:state machines. We identify DSLs for both behavior-modeling languages, and we analyze five in-depth.We mine open-source repositories for robotic applications that use the analyzed DSLs and analyze their usage. We identify similarities between behavior trees and state machines in terms of language design and the concepts offered to accommodate the needs of the robotics domain. We observed that the usage of behavior-tree DSLs in open-source projects is increasing rapidly. We observed similar usage patterns at model structure and at code reuse in the behavior-tree and state-machine models within the mined open-source projects. We contribute all extracted models as a dataset, ho** to inspire the community to use and further develop behavior trees, associated tools, and analysis techniques.
△ Less
Submitted 6 March, 2023; v1 submitted 8 August, 2022;
originally announced August 2022.
-
A Specification Logic for Programs in the Probabilistic Guarded Command Language (Extended Version)
Authors:
Raúl Pardo,
Einar Broch Johnsen,
Ina Schaefer,
Andrzej Wąsowski
Abstract:
The semantics of probabilistic languages has been extensively studied, but specification languages for their properties have received little attention. This paper introduces the probabilistic dynamic logic pDL, a specification logic for programs in the probabilistic guarded command language (pGCL) of McIver and Morgan. The proposed logic pDL can express both first-order state properties and probab…
▽ More
The semantics of probabilistic languages has been extensively studied, but specification languages for their properties have received little attention. This paper introduces the probabilistic dynamic logic pDL, a specification logic for programs in the probabilistic guarded command language (pGCL) of McIver and Morgan. The proposed logic pDL can express both first-order state properties and probabilistic reachability properties, addressing both the non-deterministic and probabilistic choice operators of pGCL. In order to precisely explain the meaning of specifications, we formally define the satisfaction relation for pDL. Since pDL embeds pGCL programs in its box-modality operator, pDL satisfiability builds on a formal MDP semantics for pGCL programs. The satisfaction relation is modeled after PCTL, but extended from propositional to first-order setting of dynamic logic, and also embedding program fragments. We study basic properties of pDL, such as weakening and distribution, that can support reasoning systems. Finally, we demonstrate the use of pDL to reason about program behavior.
△ Less
Submitted 19 August, 2022; v1 submitted 10 May, 2022;
originally announced May 2022.
-
Privug: Using Probabilistic Programming for Quantifying Leakage in Privacy Risk Analysis
Authors:
Raúl Pardo,
Willard Rafnsson,
Christian Probst,
Andrzej Wąsowski
Abstract:
Disclosure of data analytics results has important scientific and commercial justifications. However, no data shall be disclosed without a diligent investigation of risks for privacy of subjects. Privug is a tool-supported method to explore information leakage properties of data analytics and anonymization programs. In Privug, we reinterpret a program probabilistically, using off-the-shelf tools f…
▽ More
Disclosure of data analytics results has important scientific and commercial justifications. However, no data shall be disclosed without a diligent investigation of risks for privacy of subjects. Privug is a tool-supported method to explore information leakage properties of data analytics and anonymization programs. In Privug, we reinterpret a program probabilistically, using off-the-shelf tools for Bayesian inference to perform information-theoretic analysis of the information flow. For privacy researchers, Privug provides a fast, lightweight way to experiment with privacy protection measures and mechanisms. We show that Privug is accurate, scalable, and applicable to a range of leakage analysis scenarios.
△ Less
Submitted 11 August, 2021; v1 submitted 17 November, 2020;
originally announced November 2020.
-
MROS: Runtime Adaptation For Robot Control Architectures
Authors:
Darko Bozhinoski,
Carlos Hernandez Corbato,
Mario Garzon Oviedo,
Gijs van der Hoorn,
Nadia Hammoudeh Garcia,
Harshavardhan Deshpande,
Jon Tjerngren,
Andrzej Wasowski
Abstract:
Known attempts to build autonomous robots rely on complex control architectures, often implemented with the Robot Operating System platform (ROS). Runtime adaptation is needed in these systems, to cope with component failures and with contingencies arising from dynamic environments-otherwise, these affect the reliability and quality of the mission execution. Existing proposals on how to build self…
▽ More
Known attempts to build autonomous robots rely on complex control architectures, often implemented with the Robot Operating System platform (ROS). Runtime adaptation is needed in these systems, to cope with component failures and with contingencies arising from dynamic environments-otherwise, these affect the reliability and quality of the mission execution. Existing proposals on how to build self-adaptive systems in robotics usually require a major re-design of the control architecture and rely on complex tools unfamiliar to the robotics community. Moreover, they are hard to reuse across applications.
This paper presents MROS: a model-based framework for run-time adaptation of robot control architectures based on ROS. MROS uses a combination of domain-specific languages to model architectural variants and captures mission quality concerns, and an ontology-based implementation of the MAPE-K and meta-control visions for run-time adaptation. The experiment results obtained applying MROS in two realistic ROS-based robotic demonstrators show the benefits of our approach in terms of the quality of the mission execution, and MROS' extensibility and re-usability across robotic applications.
△ Less
Submitted 23 November, 2021; v1 submitted 18 October, 2020;
originally announced October 2020.
-
Behavior Trees in Action: A Study of Robotics Applications
Authors:
Razan Ghzouli,
Thorsten Berger,
Einar Broch Johnsen,
Swaib Dragule,
Andrzej Wąsowski
Abstract:
Autonomous robots combine a variety of skills to form increasingly complex behaviors called missions. While the skills are often programmed at a relatively low level of abstraction, their coordination is architecturally separated and often expressed in higher-level languages or frameworks. Recently, the language of Behavior Trees gained attention among roboticists for this reason. Originally desig…
▽ More
Autonomous robots combine a variety of skills to form increasingly complex behaviors called missions. While the skills are often programmed at a relatively low level of abstraction, their coordination is architecturally separated and often expressed in higher-level languages or frameworks. Recently, the language of Behavior Trees gained attention among roboticists for this reason. Originally designed for computer games to model autonomous actors, Behavior Trees offer an extensible tree-based representation of missions. However, even though, several implementations of the language are in use, little is known about its usage and scope in the real world. How do behavior trees relate to traditional languages for describing behavior? How are behavior tree concepts used in applications? What are the benefits of using them?
We present a study of the key language concepts in Behavior Trees and their use in real-world robotic applications. We identify behavior tree languages and compare their semantics to the most well-known behavior modeling languages: state and activity diagrams. We mine open source repositories for robotics applications that use the language and analyze this usage. We find that Behavior Trees are a pragmatic language, not fully specified, allowing projects to extend it even for just one model. Behavior trees clearly resemble the models-at-runtime paradigm. We contribute a dataset of real-world behavior models, ho** to inspire the community to use and further develop this language, associated tools, and analysis techniques.
△ Less
Submitted 11 November, 2020; v1 submitted 13 October, 2020;
originally announced October 2020.
-
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.
-
Verification of High-Level Transformations with Inductive Refinement Types
Authors:
Ahmad Salim Al-Sibahi,
Thomas P. Jensen,
Aleksandar S. Dimovski,
Andrzej Wasowski
Abstract:
High-level transformation languages like Rascal include expressive features for manipulating large abstract syntax trees: first-class traversals, expressive pattern matching, backtracking and generalized iterators. We present the design and implementation of an abstract interpretation tool, Rabit, for verifying inductive type and shape properties for transformations written in such languages. We d…
▽ More
High-level transformation languages like Rascal include expressive features for manipulating large abstract syntax trees: first-class traversals, expressive pattern matching, backtracking and generalized iterators. We present the design and implementation of an abstract interpretation tool, Rabit, for verifying inductive type and shape properties for transformations written in such languages. We describe how to perform abstract interpretation based on operational semantics, specifically focusing on the challenges arising when analyzing the expressive traversals and pattern matching. Finally, we evaluate Rabit on a series of transformations (normalization, desugaring, refactoring, code generators, type inference, etc.) showing that we can effectively verify stated properties.
△ Less
Submitted 17 September, 2018;
originally announced September 2018.
-
Clafer: Lightweight Modeling of Structure, Behaviour, and Variability
Authors:
Paulius Juodisius,
Atrisha Sarkar,
Raghava Rao Mukkamala,
Michal Antkiewicz,
Krzysztof Czarnecki,
Andrzej Wasowski
Abstract:
Embedded software is growing fast in size and complexity, leading to intimate mixture of complex architectures and complex control. Consequently, software specification requires modeling both structures and behaviour of systems. Unfortunately, existing languages do not integrate these aspects well, usually prioritizing one of them. It is common to develop a separate language for each of these face…
▽ More
Embedded software is growing fast in size and complexity, leading to intimate mixture of complex architectures and complex control. Consequently, software specification requires modeling both structures and behaviour of systems. Unfortunately, existing languages do not integrate these aspects well, usually prioritizing one of them. It is common to develop a separate language for each of these facets. In this paper, we contribute Clafer: a small language that attempts to tackle this challenge. It combines rich structural modeling with state of the art behavioural formalisms. We are not aware of any other modeling language that seamlessly combines these facets common to system and software modeling. We show how Clafer, in a single unified syntax and semantics, allows capturing feature models (variability), component models, discrete control models (automata) and variability encompassing all these aspects. The language is built on top of first order logic with quantifiers over basic entities (for modeling structures) combined with linear temporal logic (for modeling behaviour). On top of this semantic foundation we build a simple but expressive syntax, enriched with carefully selected syntactic expansions that cover hierarchical modeling, associations, automata, scenarios, and Dwyer's property patterns. We evaluate Clafer using a power window case study, and comparing it against other notations that substantially overlap with its scope (SysML, AADL, Temporal OCL and Live Sequence Charts), discussing benefits and perils of using a single notation for the purpose.
△ Less
Submitted 23 July, 2018;
originally announced July 2018.
-
Effective Analysis of C Programs by Rewriting Variability
Authors:
Alexandru Florin Iosif-Lazar,
Jean Melo,
Aleksandar S. Dimovski,
Claus Brabrand,
Andrzej Wasowski
Abstract:
Context. Variability-intensive programs (program families) appear in many application areas and for many reasons today. Different family members, called variants, are derived by switching statically configurable options (features) on and off, while reuse of the common code is maximized.
Inquiry. Verification of program families is challenging since the number of variants is exponential in the nu…
▽ More
Context. Variability-intensive programs (program families) appear in many application areas and for many reasons today. Different family members, called variants, are derived by switching statically configurable options (features) on and off, while reuse of the common code is maximized.
Inquiry. Verification of program families is challenging since the number of variants is exponential in the number of features. Existing single-program analysis and verification tools cannot be applied directly to program families, and designing and implementing the corresponding variability-aware versions is tedious and laborious.
Approach. In this work, we propose a range of variability-related transformations for translating program families into single programs by replacing compile-time variability with run-time variability (non-determinism). The obtained transformed programs can be subsequently analyzed using the conventional off- the-shelf single-program analysis tools such as type checkers, symbolic executors, model checkers, and static analyzers.
Knowledge. Our variability-related transformations are outcome-preserving, which means that the relation between the outcomes in the transformed single program and the union of outcomes of all variants derived from the original program family is equality.
Grounding. We show our transformation rules and their correctness with respect to a minimal core imperative language IMP. Then, we discuss our experience of implementing and using the transformations for efficient and effective analysis and verification of real-world C program families.
Importance. We report some interesting variability-related bugs that we discovered using various state-of-the-art single-program C verification tools, such as Frama-C, Clang, LLBMC.
△ Less
Submitted 27 January, 2017;
originally announced January 2017.
-
Variability Abstractions: Trading Precision for Speed in Family-Based Analyses (Extended Version)
Authors:
Aleksandar S. Dimovski,
Claus Brabrand,
Andrzej Wąsowski
Abstract:
Family-based (lifted) data-flow analysis for Software Product Lines (SPLs) is capable of analyzing all valid products (variants) without generating any of them explicitly. It takes as input only the common code base, which encodes all variants of a SPL, and produces analysis results corresponding to all variants. However, the computational cost of the lifted analysis still depends inherently on th…
▽ More
Family-based (lifted) data-flow analysis for Software Product Lines (SPLs) is capable of analyzing all valid products (variants) without generating any of them explicitly. It takes as input only the common code base, which encodes all variants of a SPL, and produces analysis results corresponding to all variants. However, the computational cost of the lifted analysis still depends inherently on the number of variants (which is exponential in the number of features, in the worst case). For a large number of features, the lifted analysis may be too costly or even infeasible. In this paper, we introduce variability abstractions defined as Galois connections and use abstract interpretation as a formal method for the calculational-based derivation of approximate (abstracted) lifted analyses of SPL programs, which are sound by construction. Moreover, given an abstraction we define a syntactic transformation that translates any SPL program into an abstracted version of it, such that the analysis of the abstracted SPL coincides with the corresponding abstracted analysis of the original SPL. We implement the transformation in a tool, reconfigurator that works on Object-Oriented Java program families, and evaluate the practicality of this approach on three Java SPL benchmarks.
△ Less
Submitted 16 March, 2015;
originally announced March 2015.
-
Refinement for Transition Systems with Responses
Authors:
Marco Carbone,
Thomas Hildebrandt,
Gian Perrone,
Andrzej Wąsowski
Abstract:
Motivated by the response pattern for property specifications and applications within flexible workflow management systems, we report upon an initial study of modal and mixed transition systems in which the must transitions are interpreted as must eventually, and in which implementations can contain may behaviors that are resolved at run-time. We propose Transition Systems with Responses (TSRs) as…
▽ More
Motivated by the response pattern for property specifications and applications within flexible workflow management systems, we report upon an initial study of modal and mixed transition systems in which the must transitions are interpreted as must eventually, and in which implementations can contain may behaviors that are resolved at run-time. We propose Transition Systems with Responses (TSRs) as a suitable model for this study. We prove that TSRs correspond to a restricted class of mixed transition systems, which we refer to as the action-deterministic mixed transition systems. We show that TSRs allow for a natural definition of deadlocked and accepting states. We then transfer the standard definition of refinement for mixed transition systems to TSRs and prove that refinement does not preserve deadlock freedom. This leads to the proposal of safe refinements, which are those that preserve deadlock freedom. We exemplify the use of TSRs and (safe) refinements on a small medication workflow.
△ Less
Submitted 18 July, 2012;
originally announced July 2012.
-
A Few Considerations on Structural and Logical Composition in Specification Theories
Authors:
Axel Legay,
Andrzej Wąsowski
Abstract:
Over the last 20 years a large number of automata-based specification theories have been proposed for modeling of discrete,real-time and probabilistic systems. We have observed a lot of shared algebraic structure between these formalisms. In this short abstract, we collect results of our work in progress on describing and systematizing the algebraic assumptions in specification theories.
Over the last 20 years a large number of automata-based specification theories have been proposed for modeling of discrete,real-time and probabilistic systems. We have observed a lot of shared algebraic structure between these formalisms. In this short abstract, we collect results of our work in progress on describing and systematizing the algebraic assumptions in specification theories.
△ Less
Submitted 25 January, 2011;
originally announced January 2011.
