205 research outputs found
Assume-Guarantee Testing of Evolving Software Product Line Architectures
No full textDespite some work on testing software product lines, maintaining the quality of products when a software product line evolves is still an open problem. In this paper, we propose a novel assume-guarantee testing approach as a solution to the following research question: how can we verify the correct functioning of products of an software product line when core components evolve? The underlying idea is to retest only some of the products that conform to the software product line architecture and to infer, using assume-guarantee reasoning, the correctness of the other products. Assume-guarantee reasoning moreover permits the retesting of only those components that are affected by the changes. © 2012 Springer-Verlag
The Legacy of Stefania Gnesi: From Software Engineering to Formal Methods and Tools, and Back
No full textStefania Gnesi was born in Livorno in 1954. She studied Computer Science at the University of Pisa, where she graduated summa cum laude in 1978. During her studies at ISI, which was the University of Pisa’s Institute for Computer Science, a young discipline at that time, Stefania became interested in the continuing challenge associated with the production of software, namely to demonstrate that the developed software is actually doing what is expected to do, a challenge made harder in many cases by the fact that the expectations themselves are not precisely expressed. This has kept her busy ever since. To face this challenge her very first steps in research, towards the end of her university studies, of purely theoretical nature, proved very valuable. In a publication in the Journal of the ACM [63] (not bad for a first journal paper!), resulting from her thesis under the supervision of Prof. Ugo Montanari, it is shown that finding the solution of a dynamic programming problem in the form of polyadic functional equations is equivalent to searching a minimal cost path in an and/or graph with monotone cost functions. An important computational application of this result is that the solution of a system of functional equations can always be reduced to the problem of searching a minimal cost solution tree in an and/or graph
Validating reconfigurations of Reo circuits in an e-banking scenario
No full textWe formalize dynamic reconfiguration of Reo circuits (which can be thought of as multi-party communication infrastructures built from primitive channels) through graph transformation, and apply it to a scenario from the Finance domain: a critical infrastructure controlling the business process of an e-banking system. In this scenario, reconfiguration is triggered as soon as the communication buffers reach specific predefined thresholds of congestion. These constraints are implemented inside the Reo model by associating suitable predicates to channels, thus extending previous results on the use of graph transformation for the reconfiguration of Reo's graphical structures
Dynamic Software Architecture Development: Towards an Automated Process
No full textWe propose a software engineering process to aid the development of Dynamic Software Architectures (DSAs). This process is based on the sequential application of a number of formal methods and tools, and it can support software architects throughout the design, analysis and code generation of software systems. To illustrate the process, we apply it to an industrial case study from the Service-Oriented Computing (SOC) domain
Detecting Policy Conflicts by Model Checking UML State Machines
No full textPolicies are convenient means to modify system behaviour at run-time.
Nowadays, policies are created in great numbers by different actors, ranging from
system administrators to lay-users. However, this situation may lead naturally to
inconsistencies, a problem that has been recognized and termed policy conflict.
The adoption of a widely-used notation, with good tool support, to express the
policies, can not only support the detection, but also help all the involved actors
in understanding and resolving the conflicts. In this respect, a natural candidate
is UML due to its current wide use in the industrial practice. In this paper we
show how to model check policies expressed in UML to verify whether they are
free of conflicts: we define a correspondence between APPEL policies and UML
state machines and use UMC as a model checker. We validate the approach with
examples taken from the literature
Analysing Robot Movement Using the Sensoria Methods
No full textIn this paper, we give a recount of the application of Sensoria approaches, languages, and tools to the modeling of movement of the robot that has taken the lead role in Sensoria demonstrations at the exhibitions ICT 2008 in Lyon and FET 2009 in Prague. The demos were centred around a robot-bowling game that actively involved the visitors in programming a robot that plays bowling, using some of the techniques developed in Sensoria in order to predict the outcomes of the game according to their design choices. Specifically, the Sensoria techniques have been used for the analysis of functional and non-functional properties of the system, both in the ex-post analysis of the robot movement during the demo and in the ex-ante analysis of the possible robot configurations during the design of the robot and of the demo itself. This paper presents how the techniques have been applied and to what extent the results of the application match the real robot behavior. The Sensoria modeling and analysis techniques used are the UML4SOA graphical modeling language, the Performance Evaluation Process Algebra PEPA, the UMC model checker and the Markovian process algebra MarCaSPiS
Quantitative Analysis of Probabilistic Models of SoftwareProduct Lines with Statistical Model Checking
No full textWe investigate the suitability of statistical model checking techniques for analysing quantitative prop-erties of software product line models with probabilistic aspects. For this purpose, we enrich thefeature-oriented language FLANwith action rates, which specify the likelihood of exhibiting par-ticular behaviour or of installing features at a specific moment or in a specific order. The enrichedlanguage (called PFLAN) allows us to specify models of software product lines with probabilis-tic configurations and behaviour, e.g. by considering a PFLANsemantics based on discrete-timeMarkov chains. The Maude implementation of PFLANis combined with the distributed statisticalmodel checker MultiVeStA to perform quantitative analyses of a simple product line case study. Thepresented analyses include the likelihood of certain behaviour of interest (e.g. product malfunction-ing) and the expected average cost of product
Variability meets Security: Quantitative security modeling and analysis of highly customizable attack scenarios
No full textWe present a framework for quantitative security modeling and analysis of highly customizable attack scenarios, which resulted as a spin-off from our research in software product line engineering. The graphical security models are based on attributed attack-defense diagrams to capture the structure and properties of vulnerabilities, defenses and countermeasures-with notable similarities to feature diagrams-and on probabilistic models of attack behavior, capable of capturing resource constraints and attack effectiveness. In this paper, we provide an overview of the framework that is described in full technical detail in twin papers, which present the formal syntax and semantics of the domain-specific language and showcase the associated tool with advanced IDE support for performing analyses based on statistical model checking. The properties of interest range from average cost and success probability of attacks to the effectiveness of defenses and countermeasures. Here we illustrate the capabilities of the DSL and the tool by applying them to an example scenario from the security domain. This shows how techniques from variability modeling can be applied to security. We conclude with a vision and roadmap for future research
Towards Reinforcement Learning-based Aggregate Computing
No full textRecent trends in pervasive computing promote the vision of Collective Adaptive Systems (CASs): large-scale collections of relatively simple agents that act and coordinate with no central orchestrator to support distributed applications. Engineering global behaviour out of local activity and interaction, however, is a difficult task, typically addressed by try-and-error approaches in simulation environments. In the context of Aggregate Computing (AC), a prominent functional programming approach for CASs based on field-based coordination, this difficulty is reflected in the design of versatile algorithms preserving efficiency in a variety of environments. To deal with this complexity, in this work we propose to apply Machine Learning techniques to automatically devise local actions to improve over manually-defined AC algorithms specifications. Most specifically, we adopt a Reinforcement Learning-based approach to let a collective learn local policies to improve over the standard gradient algorithm—a cornerstone brick of several higher-level self-organisation algorithms. Our evaluation shows that the learned policies can speed up the self-stabilisation of the gradient to external perturbations
- …
