- Formal Methods in Verification
- Software Reliability and Analysis Research
- Software Testing and Debugging Techniques
- Logic, programming, and type systems
- Model-Driven Software Engineering Techniques
- Petri Nets in System Modeling
- Software Engineering Research
- Software System Performance and Reliability
- Advanced Software Engineering Methodologies
- Computability, Logic, AI Algorithms
- Big Data Technologies and Applications
- Cognitive Computing and Networks
- Distributed systems and fault tolerance
Imperial College London
2016-2020
University of Naples Federico II
2014-2015
We investigate the dependence of software failure reproducibility on environment in which is executed. The existence such ascertained literature, but so far it not fully characterized. In this paper we pinpoint some environmental components that can affect a and show influence through an experimental campaign conducted My SQL Server system. set failures interest drawn from SQL's reports database experiment designed for each these failures. experiments expose disk usage level concurrency...
A challenge that has gathered much attention in recent years is automated synthesis of correct-by-construction software systems from declarative specifications. The specification language typically a subset linear temporal logic called generalized reactivity rank 1, for which there exists an efficient algorithm. Specifications this model the system as interaction between environment and controller, former satisfying set assumptions latter guarantees. In order solution to exist, sufficient...
Defect prediction techniques allow spotting modules (or commits) likely to contain (introduce) a defect by training models with product or process metrics -- thus supporting testing, code integration, and release decisions. When applied processes where software changes rapidly, conventional might fail, as trained are not thought evolve along the software. In this study, we analyze performance of in rapidly evolving Framed high commit frequency context, set up an approach continuously refine...
Defect prediction techniques allow spotting modules (or commits) likely to contain (introduce) a defect by training models with product or process metrics -- thus supporting testing, code integration, and release decisions. When applied processes where software changes rapidly, conventional might fail, as trained are not thought evolve along the software. In this study, we analyze performance of in rapidly evolving Framed high commit frequency context, set up an approach continuously refine...
Abstract When dealing with unrealizable specifications in reactive synthesis, finding the weakest environment assumptions that ensure realizability is often considered a desirable property. However, little effort has been dedicated to defining or evaluating notion of weakness formally. The question whether one assumption weaker than another commonly interpreted by considering implication relationship between two or, equivalently, their language inclusion. This interpretation fails provide...
Reactive synthesis is concerned with finding a correct-by-construction controller from formal specifications, typically expressed in Linear Temporal Logic (LTL). The specifications describe assumptions about an environment and guarantees to be achieved by the operating that environment. If exists, given assumptions, specification said realizable. This paper focuses on minimal set of guarantee realizability context counterstrategy-guided assumption refinement procedures. Specifically, we...
This paper considers the problem of assumptions refinement in context unrealizable specifications for reactive systems. We propose a new counterstrategy-guided synthesis approach GR(1) based on Craig's interpolants. Our interpolation-based method identifies causes unrealizability and computes that directly target cores, without need user input. Thereby, we discuss how this property reduces maximum number steps needed to converge realizability compared with other techniques. describe...
In spite of the theoretical and algorithmic developments for system synthesis in recent years, little effort has been dedicated to quantifying quality specifications used synthesis. When dealing with unrealizable specifications, finding weakest environment assumptions that would ensure realizability is typically a desirable property; such context weakness major parameter. The question whether one assumption weaker than another commonly interpreted using implication or, equivalently, language...
Abstract The paper ‘A Weakness Measure for GR(1) Formulae’, by Davide G. Cavezza, Dalal Alrajeh and András György, published in Formal Aspects of Computing, November 2020, explores a new measure assessing the weakness conjunctions quantitatively.