-
SEArch: an execution infrastructure for service-based software systems
Authors:
Carlos G. Lopez Pombo,
Pablo Montepagano,
Emilio Tuosto
Abstract:
The shift from monolithic applications to composition of distributed software initiated in the early twentieth, is based on the vision of software-as-service. This vision, found in many technologies such as RESTful APIs, advocates globally available services cooperating through an infrastructure providing (access to) distributed computational resources. Choreographies can support this vision by ab…
▽ More
The shift from monolithic applications to composition of distributed software initiated in the early twentieth, is based on the vision of software-as-service. This vision, found in many technologies such as RESTful APIs, advocates globally available services cooperating through an infrastructure providing (access to) distributed computational resources. Choreographies can support this vision by abstracting away local computation and rendering interoperability with message-passing: cooperation is achieved by sending and receiving messages. Following this choreographic paradigm, we develop SEArch, after Service Execution Architecture, a language-independent execution infrastructure capable of performing transparent dynamic reconfiguration of software artefacts. Choreographic mechanisms are used in SEArch to specify interoperability contracts, thus providing the support needed for automatic discovery and binding of services at runtime.
△ Less
Submitted 30 April, 2024;
originally announced April 2024.
-
MoCheQoS: Automated Analysis of Quality of Service Properties of Communicating Systems
Authors:
Carlos G. Lopez Pombo,
Agustín E. Martinez Suñé,
Emilio Tuosto
Abstract:
We present MoCheQoS, a bounded model checker to analyse (QoS) properties of message-passing systems. Building on the dynamic temporal logic, the choreographic model, and the bounded model checking algorithm defined in our ICTAC 2023 paper, MoCheQoS enables the static analysis of QoS properties of systems built out from the composition of services. We consider QoS properties on measurable applicati…
▽ More
We present MoCheQoS, a bounded model checker to analyse (QoS) properties of message-passing systems. Building on the dynamic temporal logic, the choreographic model, and the bounded model checking algorithm defined in our ICTAC 2023 paper, MoCheQoS enables the static analysis of QoS properties of systems built out from the composition of services. We consider QoS properties on measurable application-level attributes as well as resource consumption metrics for example those relating monetary cost to memory usage. The implementation of the tool is accompanied by an experimental evaluation. More precisely, we present two case studies meant to evaluate the applicability of MoCheQoS; the first is based on the AWS cloud while the second analyses a communicating system automatically extracted from code. Additionally, we consider synthetically generated experiments to assess the scalability of MoCheQoS. These experiments showed that our model can faithfully capture and effectively analyse QoS properties in industrial-strength scenarios.
△ Less
Submitted 28 June, 2024; v1 submitted 2 November, 2023;
originally announced November 2023.
-
A Dynamic Temporal Logic for Quality of Service in Choreographic Models
Authors:
Carlos G. Lopez Pombo,
Agustín E. Martinez Suñé,
Emilio Tuosto
Abstract:
We propose a framework for expressing and analyzing the Quality of Service (QoS) of message-passing systems using a choreographic model that consists of g-choreographies and Communicating Finite State machines (CFSMs). The following are our three main contributions: (I) an extension of CFSMs with non-functional contracts to specify quantitative constraints of local computations, (II) a dynamic tem…
▽ More
We propose a framework for expressing and analyzing the Quality of Service (QoS) of message-passing systems using a choreographic model that consists of g-choreographies and Communicating Finite State machines (CFSMs). The following are our three main contributions: (I) an extension of CFSMs with non-functional contracts to specify quantitative constraints of local computations, (II) a dynamic temporal logic capable of expressing QoS, properties of systems relative to the g-choreography that specifies the communication protocol, (III) the semi-decidability of our logic which enables a bounded model-checking approach to verify QoS property of communicating systems.
△ Less
Submitted 6 November, 2023; v1 submitted 2 November, 2023;
originally announced November 2023.
-
Computational limits to the legibility of the imaged human brain
Authors:
James K Ruffle,
Robert J Gray,
Samia Mohinta,
Guilherme Pombo,
Chaitanya Kaul,
Harpreet Hyare,
Geraint Rees,
Parashkev Nachev
Abstract:
Our knowledge of the organisation of the human brain at the population-level is yet to translate into power to predict functional differences at the individual-level, limiting clinical applications, and casting doubt on the generalisability of inferred mechanisms. It remains unknown whether the difficulty arises from the absence of individuating biological patterns within the brain, or from limite…
▽ More
Our knowledge of the organisation of the human brain at the population-level is yet to translate into power to predict functional differences at the individual-level, limiting clinical applications, and casting doubt on the generalisability of inferred mechanisms. It remains unknown whether the difficulty arises from the absence of individuating biological patterns within the brain, or from limited power to access them with the models and compute at our disposal. Here we comprehensively investigate the resolvability of such patterns with data and compute at unprecedented scale. Across 23 810 unique participants from UK Biobank, we systematically evaluate the predictability of 25 individual biological characteristics, from all available combinations of structural and functional neuroimaging data. Over 4526 GPU hours of computation, we train, optimize, and evaluate out-of-sample 700 individual predictive models, including fully-connected feed-forward neural networks of demographic, psychological, serological, chronic disease, and functional connectivity characteristics, and both uni- and multi-modal 3D convolutional neural network models of macro- and micro-structural brain imaging. We find a marked discrepancy between the high predictability of sex (balanced accuracy 99.7%), age (mean absolute error 2.048 years, R2 0.859), and weight (mean absolute error 2.609Kg, R2 0.625), for which we set new state-of-the-art performance, and the surprisingly low predictability of other characteristics. Neither structural nor functional imaging predicted psychology better than the coincidence of chronic disease (p<0.05). Serology predicted chronic disease (p<0.05) and was best predicted by it (p<0.001), followed by structural neuroimaging (p<0.05). Our findings suggest either more informative imaging or more powerful models are needed to decipher individual level characteristics from the human brain.
△ Less
Submitted 2 April, 2024; v1 submitted 23 August, 2023;
originally announced September 2023.
-
The minimal computational substrate of fluid intelligence
Authors:
Amy PK Nelson,
Joe Mole,
Guilherme Pombo,
Robert J Gray,
James K Ruffle,
Edgar Chan,
Geraint E Rees,
Lisa Cipolotti,
Parashkev Nachev
Abstract:
The quantification of cognitive powers rests on identifying a behavioural task that depends on them. Such dependence cannot be assured, for the powers a task invokes cannot be experimentally controlled or constrained a priori, resulting in unknown vulnerability to failure of specificity and generalisability. Evaluating a compact version of Raven's Advanced Progressive Matrices (RAPM), a widely use…
▽ More
The quantification of cognitive powers rests on identifying a behavioural task that depends on them. Such dependence cannot be assured, for the powers a task invokes cannot be experimentally controlled or constrained a priori, resulting in unknown vulnerability to failure of specificity and generalisability. Evaluating a compact version of Raven's Advanced Progressive Matrices (RAPM), a widely used clinical test of fluid intelligence, we show that LaMa, a self-supervised artificial neural network trained solely on the completion of partially masked images of natural environmental scenes, achieves human-level test scores a prima vista, without any task-specific inductive bias or training. Compared with cohorts of healthy and focally lesioned participants, LaMa exhibits human-like variation with item difficulty, and produces errors characteristic of right frontal lobe damage under degradation of its ability to integrate global spatial patterns. LaMa's narrow training and limited capacity -- comparable to the nervous system of the fruit fly -- suggest RAPM may be open to computationally simple solutions that need not necessarily invoke abstract reasoning.
△ Less
Submitted 14 August, 2023;
originally announced August 2023.
-
Deep Variational Lesion-Deficit Map**
Authors:
Guilherme Pombo,
Robert Gray,
Amy P. K. Nelson,
Chris Foulon,
John Ashburner,
Parashkev Nachev
Abstract:
Causal map** of the functional organisation of the human brain requires evidence of \textit{necessity} available at adequate scale only from pathological lesions of natural origin. This demands inferential models with sufficient flexibility to capture both the observable distribution of pathological damage and the unobserved distribution of the neural substrate. Current model frameworks -- both…
▽ More
Causal map** of the functional organisation of the human brain requires evidence of \textit{necessity} available at adequate scale only from pathological lesions of natural origin. This demands inferential models with sufficient flexibility to capture both the observable distribution of pathological damage and the unobserved distribution of the neural substrate. Current model frameworks -- both mass-univariate and multivariate -- either ignore distributed lesion-deficit relations or do not model them explicitly, relying on featurization incidental to a predictive task. Here we initiate the application of deep generative neural network architectures to the task of lesion-deficit inference, formulating it as the estimation of an expressive hierarchical model of the joint lesion and deficit distributions conditioned on a latent neural substrate. We implement such deep lesion deficit inference with variational convolutional volumetric auto-encoders. We introduce a comprehensive framework for lesion-deficit model comparison, incorporating diverse candidate substrates, forms of substrate interactions, sample sizes, noise corruption, and population heterogeneity. Drawing on 5500 volume images of ischaemic stroke, we show that our model outperforms established methods by a substantial margin across all simulation scenarios, including comparatively small-scale and noisy data regimes. Our analysis justifies the widespread adoption of this approach, for which we provide an open source implementation: https://github.com/guilherme-pombo/vae_lesion_deficit
△ Less
Submitted 27 May, 2023;
originally announced May 2023.
-
Individualized prescriptive inference in ischaemic stroke
Authors:
Dominic Giles,
Robert Gray,
Chris Foulon,
Guilherme Pombo,
Tianbo Xu,
H. Rolf Jäger,
Jorge Cardoso,
Sebastien Ourselin,
Geraint Rees,
Ashwani Jha,
Parashkev Nachev
Abstract:
The gold standard in the treatment of ischaemic stroke is set by evidence from randomized controlled trials. Yet the manifest complexity of the brain's functional, connective, and vascular architectures introduces heterogeneity in treatment susceptibility that violates the underlying statistical premisses, potentially leading to substantial errors at both individual and population levels. The coun…
▽ More
The gold standard in the treatment of ischaemic stroke is set by evidence from randomized controlled trials. Yet the manifest complexity of the brain's functional, connective, and vascular architectures introduces heterogeneity in treatment susceptibility that violates the underlying statistical premisses, potentially leading to substantial errors at both individual and population levels. The counterfactual nature of therapeutic inference has made quantifying the impact of this defect difficult. Combining large-scale meta-analytic connective, functional, genetic expression, and receptor distribution data with high-resolution maps of 4 119 acute ischaemic lesions, here we conduct a comprehensive series of semi-synthetic virtual interventional trials, quantifying the fidelity of the traditional approach in inferring individual treatment effects against biologically plausible, empirically informed ground truths, across 103 628 800 distinct simulations. Combining deep generative models expressive enough to capture the observed lesion heterogeneity with flexible causal modelling, we find that the richness of the lesion representation is decisive in determining individual-level fidelity, even where freedom from treatment allocation bias cannot be guaranteed. Our results indicate that complex modelling with richly represented lesion data is critical to individualized prescriptive inference in ischaemic stroke.
△ Less
Submitted 27 February, 2024; v1 submitted 25 January, 2023;
originally announced January 2023.
-
Brain tumour genetic network signatures of survival
Authors:
James K Ruffle,
Samia Mohinta,
Guilherme Pombo,
Robert Gray,
Valeriya Kopanitsa,
Faith Lee,
Sebastian Brandner,
Harpreet Hyare,
Parashkev Nachev
Abstract:
Tumour heterogeneity is increasingly recognized as a major obstacle to therapeutic success across neuro-oncology. Gliomas are characterised by distinct combinations of genetic and epigenetic alterations, resulting in complex interactions across multiple molecular pathways. Predicting disease evolution and prescribing individually optimal treatment requires statistical models complex enough to capt…
▽ More
Tumour heterogeneity is increasingly recognized as a major obstacle to therapeutic success across neuro-oncology. Gliomas are characterised by distinct combinations of genetic and epigenetic alterations, resulting in complex interactions across multiple molecular pathways. Predicting disease evolution and prescribing individually optimal treatment requires statistical models complex enough to capture the intricate (epi)genetic structure underpinning oncogenesis. Here, we formalize this task as the inference of distinct patterns of connectivity within hierarchical latent representations of genetic networks. Evaluating multi-institutional clinical, genetic, and outcome data from 4023 glioma patients over 14 years, across 12 countries, we employ Bayesian generative stochastic block modelling to reveal a hierarchical network structure of tumour genetics spanning molecularly confirmed glioblastoma, IDH- wildtype; oligodendroglioma, IDH-mutant and 1p/19q codeleted; and astrocytoma, IDH- mutant. Our findings illuminate the complex dependence between features across the genetic landscape of brain tumours, and show that generative network models reveal distinct signatures of survival with better prognostic fidelity than current gold standard diagnostic categories.
△ Less
Submitted 5 May, 2023; v1 submitted 15 January, 2023;
originally announced January 2023.
-
Integrating deduction and model finding in a language independent setting
Authors:
Carlos Gustavo Lopez Pombo,
Agustín Eloy Martinez Suñé
Abstract:
Software artifacts are ubiquitous in our lives being an essential part of home appliances, cars, cel phones, and even in more critical activities like aeronautics and health sciences. In this context software failures may produce enormous losses, either economical or, in the extreme, in human lives. Software analysis is an area in software engineering concerned on the application of different tech…
▽ More
Software artifacts are ubiquitous in our lives being an essential part of home appliances, cars, cel phones, and even in more critical activities like aeronautics and health sciences. In this context software failures may produce enormous losses, either economical or, in the extreme, in human lives. Software analysis is an area in software engineering concerned on the application of different techniques in order to prove the (relative) absence of errors in software artifacts. In many cases these methods of analysis are applied by following certain methodological directives that ensure better results. In a previous work we presented the notion of satisfiability calculus as a model theoretical counterpart of Meseguer's proof calculus, providing a formal foundation for a variety of tools that are based on model construction. The present work shows how effective satisfiability sub-calculi, a special type of satisfiability calculi, can be combined with proof calculi, in order to provide foundations to certain methodological approaches to software analysis by relating the construction of finite counterexamples and the absence of proofs, in an abstract categorical setting.
△ Less
Submitted 14 June, 2022;
originally announced June 2022.
-
Probabilistic Quality of Service aware Service Selection
Authors:
Agustín E. Martinez Suñé,
Carlos G. Lopez Pombo
Abstract:
In software-as-a-service paradigms software systems are no longer monolithic pieces of code executing within the boundaries of an organisation, on the contrary, they are conceived as a dynamically changing collection of services, collectively executing, in pursuit of a common business goal. An essential aspect of service selection is determining whether the Quality of Service (QoS) profile of a se…
▽ More
In software-as-a-service paradigms software systems are no longer monolithic pieces of code executing within the boundaries of an organisation, on the contrary, they are conceived as a dynamically changing collection of services, collectively executing, in pursuit of a common business goal. An essential aspect of service selection is determining whether the Quality of Service (QoS) profile of a service satisfies the QoS requirements of a client.
In realistic execution environments, such QoS values might be influenced by external, non-controllable events, making it impossible for the service provider to guarantee that the values characterised by a QoS profile will be met, naturally leading to the need of a probabilistic interpretation of QoS profile.
In this work we propose: 1) a model for describing probabilistic QoS profiles based on multivariate continuous probability distributions, 2) a language for describing probabilistic QoS requirements, and 3) an automatic procedure for assessing whether a probabilistic QoS profile satisfies a probabilistic QoS requirement.
△ Less
Submitted 19 May, 2022;
originally announced May 2022.
-
Equitable modelling of brain imaging by counterfactual augmentation with morphologically constrained 3D deep generative models
Authors:
Guilherme Pombo,
Robert Gray,
Jorge Cardoso,
Sebastien Ourselin,
Geraint Rees,
John Ashburner,
Parashkev Nachev
Abstract:
We describe Countersynth, a conditional generative model of diffeomorphic deformations that induce label-driven, biologically plausible changes in volumetric brain images. The model is intended to synthesise counterfactual training data augmentations for downstream discriminative modelling tasks where fidelity is limited by data imbalance, distributional instability, confounding, or underspecifica…
▽ More
We describe Countersynth, a conditional generative model of diffeomorphic deformations that induce label-driven, biologically plausible changes in volumetric brain images. The model is intended to synthesise counterfactual training data augmentations for downstream discriminative modelling tasks where fidelity is limited by data imbalance, distributional instability, confounding, or underspecification, and exhibits inequitable performance across distinct subpopulations. Focusing on demographic attributes, we evaluate the quality of synthesized counterfactuals with voxel-based morphometry, classification and regression of the conditioning attributes, and the Fréchet inception distance. Examining downstream discriminative performance in the context of engineered demographic imbalance and confounding, we use UK Biobank magnetic resonance imaging data to benchmark CounterSynth augmentation against current solutions to these problems. We achieve state-of-the-art improvements, both in overall fidelity and equity. The source code for CounterSynth is available online.
△ Less
Submitted 29 November, 2021;
originally announced November 2021.
-
A proof theoretic basis for relational semantics
Authors:
Carlos G. Lopez Pombo,
Thomas S. E. Maibaum
Abstract:
Logic has proved essential for formally modeling software based systems. Such formal descriptions, frequently called specifications, have served not only as requirements documentation and formalisation, but also for providing the mathematical foundations for their analysis and the development of automated reasoning tools.
Logic is usually studied in terms of its two inherent aspects: syntax and…
▽ More
Logic has proved essential for formally modeling software based systems. Such formal descriptions, frequently called specifications, have served not only as requirements documentation and formalisation, but also for providing the mathematical foundations for their analysis and the development of automated reasoning tools.
Logic is usually studied in terms of its two inherent aspects: syntax and semantics. The relevance of the latter resides in the fact that producing logical descriptions of real-world phenomena, requires people to agree on how such descriptions are to be interpreted and understood by human beings, so that systems can be built with confidence in accordance with their specification. On the more practical side, the metalogical relation between syntax and semantics, determines important aspects of the conclusions one can draw from the application of certain analysis techniques, like model checking.
Abstract model theory (i.e., the mathematical perspective on semantics of logical languages) is of little practical value to software engineering endeavours. From our point of view, values (those that can be assigned to constants and variables) should not be just points in a platonic domain of interpretation, but elements that can be named by means of terms over the signature of the specification. In a nutshell, we are not interested in properties that require any semantic information not representable using the available syntax.
In this paper we present a framework supporting the proof theoretical formalisation of classes of relational models for behavioural logical languages, whose domains of discourse are guaranteed to be formed exclusively by nameable values.
△ Less
Submitted 17 July, 2021;
originally announced July 2021.
-
On the construction of explosive relation algebras
Authors:
Carlos G. Lopez Pombo,
Marcelo F. Frias,
Thomas S. E. Maibaum
Abstract:
Fork algebras are an extension of relation algebras obtained by extending the set of logical symbols with a binary operator called fork. This class of algebras was introduced by Haeberer and Veloso in the early 90's aiming at enriching relation algebra, an already successful language for program specification, with the capability of expressing some form of parallel computation.
The further study…
▽ More
Fork algebras are an extension of relation algebras obtained by extending the set of logical symbols with a binary operator called fork. This class of algebras was introduced by Haeberer and Veloso in the early 90's aiming at enriching relation algebra, an already successful language for program specification, with the capability of expressing some form of parallel computation.
The further study of this class of algebras led to many meaningful results linked to interesting properties of relation algebras such as representability and finite axiomatizability, among others. Also in the 90's, Veloso introduced a subclass of relation algebras that are expansible to fork algebras, admitting a large number of non-isomorphic expansions, referred to as explosive relation algebras.
In this work we discuss some general techniques for constructing algebras of this type.
△ Less
Submitted 9 September, 2020; v1 submitted 6 September, 2020;
originally announced September 2020.
-
Bayesian Volumetric Autoregressive generative models for better semisupervised learning
Authors:
Guilherme Pombo,
Robert Gray,
Tom Varsavsky,
John Ashburner,
Parashkev Nachev
Abstract:
Deep generative models are rapidly gaining traction in medical imaging. Nonetheless, most generative architectures struggle to capture the underlying probability distributions of volumetric data, exhibit convergence problems, and offer no robust indices of model uncertainty. By comparison, the autoregressive generative model PixelCNN can be extended to volumetric data with relative ease, it readil…
▽ More
Deep generative models are rapidly gaining traction in medical imaging. Nonetheless, most generative architectures struggle to capture the underlying probability distributions of volumetric data, exhibit convergence problems, and offer no robust indices of model uncertainty. By comparison, the autoregressive generative model PixelCNN can be extended to volumetric data with relative ease, it readily attempts to learn the true underlying probability distribution and it still admits a Bayesian reformulation that provides a principled framework for reasoning about model uncertainty. Our contributions in this paper are two fold: first, we extend PixelCNN to work with volumetric brain magnetic resonance imaging data. Second, we show that reformulating this model to approximate a deep Gaussian process yields a measure of uncertainty that improves the performance of semi-supervised learning, in particular classification performance in settings where the proportion of labelled data is low. We quantify this improvement across classification, regression, and semantic segmentation tasks, training and testing on clinical magnetic resonance brain imaging data comprising T1-weighted and diffusion-weighted sequences.
△ Less
Submitted 26 July, 2019;
originally announced July 2019.
-
Communicating machines as a dynamic binding mechanism of services
Authors:
Ignacio Vissani,
Carlos Gustavo Lopez Pombo,
Emilio Tuosto
Abstract:
Distributed software is becoming more and more dynamic to support applications able to respond and adapt to the changes of their execution environment. For instance, service-oriented computing (SOC) envisages applications as services running over globally available computational resources where discovery and binding between them is transparently performed by a middleware. Asynchronous Relational N…
▽ More
Distributed software is becoming more and more dynamic to support applications able to respond and adapt to the changes of their execution environment. For instance, service-oriented computing (SOC) envisages applications as services running over globally available computational resources where discovery and binding between them is transparently performed by a middleware. Asynchronous Relational Networks (ARNs) is a well-known formal orchestration model, based on hypergraphs, for the description of service-oriented software artefacts. Choreography and orchestration are the two main design principles for the development of distributed software. In this work, we propose Communicating Relational Networks (CRNs), which is a variant of ARNs, but relies on choreographies for the characterisation of the communicational aspects of a software artefact, and for making their automated analysis more efficient.
△ Less
Submitted 10 February, 2016;
originally announced February 2016.
-
HeteroGenius: A Framework for Hybrid Analysis of Heterogeneous Software Specifications
Authors:
Manuel Giménez,
Mariano M. Moscato,
Carlos G. Lopez Pombo,
Marcelo F. Frias
Abstract:
Nowadays, software artifacts are ubiquitous in our lives being an essential part of home appliances, cars, cell phones, and even in more critical activities like aeronautics and health sciences. In this context software failures may produce enormous losses, either economical or, in the worst case, in human lives. Software analysis is an area in software engineering concerned with the application o…
▽ More
Nowadays, software artifacts are ubiquitous in our lives being an essential part of home appliances, cars, cell phones, and even in more critical activities like aeronautics and health sciences. In this context software failures may produce enormous losses, either economical or, in the worst case, in human lives. Software analysis is an area in software engineering concerned with the application of diverse techniques in order to prove the absence of errors in software pieces. In many cases different analysis techniques are applied by following specific methodological combinations that ensure better results. These interactions between tools are usually carried out at the user level and it is not supported by the tools. In this work we present HeteroGenius, a framework conceived to develop tools that allow users to perform hybrid analysis of heterogeneous software specifications.
HeteroGenius was designed prioritising the possibility of adding new specification languages and analysis tools and enabling a synergic relation of the techniques under a graphical interface satisfying several well-known usability enhancement criteria. As a case-study we implemented the functionality of Dynamite on top of HeteroGenius.
△ Less
Submitted 5 January, 2014;
originally announced January 2014.
