2015, Contributo in atti di convegno, ENG
Ter Beek M. H.; Legay A.; Lluch Lafuente A.; Vandin A.
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.
2014, Contributo in atti di convegno, ENG
Ter Beek M. H.; Gnesi S.; Mazzanti F.
Formal modelling and verification of variability concepts in product families has been the subject of extensive study in the literature on Software Product Lines. In recent years, we have laid the basis for the use of modal specifications and branching-time temporal logics for the specification and analysis of behavioural variability in product family definitions. A critical point in this formalization is the lack of a possibility to model an adequate representation of the data that may need to be described when considering real systems. To this aim, we now extend the modelling and verification environment that we have developed for specifications interpreted over Modal Transition Systems, by adding the possibility to include data in the specifications. In concert with this, we also extend the variability-specific modal logic and the associated special-purpose model checker VMC. As a result, it offers the possibility to efficiently verify formulas over possibly infinite-state systems by using the on-the-fly bounded model-checking algorithms implemented in the model checker. We illustrate our approach by means of a simple yet intuitive example: a bike-sharing system.
2008, Contributo in volume, ENG
Bucchiarone A.; Gnesi S.; Bruni R.; Lafuente A. L.; Hirsch D.
We illustrate two ways to address the specification, modelling and analysis of dynamic software architectures using: i) ordinary typed graph transformation techniques implemented in Alloy; ii) a process algebraic presentation of graph transformation implemented in Maude. The two approaches are compared by showing how different aspects can be tackled, including representation issues, modelling phases, property specification and analysis.
2008, Articolo in rivista, ENG
Bucchiarone A.; Gnesi S.; Bruni R.; Lafuente A. L.; Hirsch D.
We illustrate two ways to address the specification, modelling and analysis of dynamic software architectures using: i) ordinary typed graph transformation techniques implemented in Alloy; ii) a process algebraic presentation of graph transformation implemented inMaude. The two approaches are compared by showing how different aspects can be tackled, including representation issues, modelling phases, property specification and analysis.
2007, Contributo in atti di convegno, ENG
Palmeri M. C.; De Nicola R.; Massink M.
The definition of behavioural preorders over process terms as the maximal (pre-)congruences induced by basic observables has proven to be a useful technique to define various preorders and equivalences in the non-probabilistic setting. In this paper, we consider probabilistic observables to define an observational semantics for a probabilistic pro- cess calculus. The resulting pre-congruence is proven to coincide with a probabilistic may preorder, which, in turn, corresponds to a natural probabilistic extension of the may testing preorder of De Nicola and Hennessy.
2005, Presentazione, ENG
De Nicola R.; Katoen J.; Latella D.; Massink M.
Deploying applications within a Grid infrastructure is an important aspect that has not yet be fully addressed. This is particular true when it is offered to the programmers some high-level abstractions. Supporting such high-level abstractions, like objects or components, requires the deployment of several middleware systems that correspond to the implementation of such high-level of abstractions. The deployment problems is thus not anymore related to the application itself but encompass a more general level of concern about how to describe which middleware systems are required for a given application, how resources are discovered and selected according to the application requirement, how the deployment process is planned and enacted and finally how the application is executed. This paper addresses this deployment issue by illustraing how it has been handled within two projects (ASSIST and GridCCM). From this experience, a common deployment model is presented as the result of the integration of the experience gained by researchers involved in these two projects.
1995, Manuale tecnico/Guida tecnica, ENG
Latella D.; Massink M.
In this paper we present an algebra of processes with input and output. The key point is the conceptual distinction between input and output actions.We give an operational semantics and a notion of testing where the experimenter is not allowed to restrict the output possibilities of the process under test, as it instead could be the case if the standard synchronization-based approach of process algebra would be used. We also give two denotational models, one based on la kind of acceptance trees and the other based on sets of functions and we prove them fully abstract with respect to the testing equivalence induced by the new notion of experimenter. The model based on sets of functions provides a simple and powerful way for combining the process algebra approach with the functional one. In process algebras notions for dealing with non--determinism and progress properties of processes deadlock, etc. has been studied deeply. In thefunctional approach clean proof styles - like the transformational one -- and proof techniques - like induction principles for minimal as well as maximal fixpoints - have been proved successful. The combination of these approaches gives an interesting framework for the specification and verification A of concurrent systems.
1991, Contributo in atti di convegno, ENG
Camilleri A.; Inverardi P.; Nesi M.
Most existing verification tools for process algebras allow the correctness of specifications to be checked in a fully automatic fashion. These systems have the obvious advantage of being easy to use, but unfortunately they also have some drawbacks. In particular, they do not always succeed in completing the verification analysis, due to the problem of state explosion, and they do not provide any insight into the meaning of the intended specifications. In this paper we consider an alternative approach in which both interactive and automatic techniques are combined in the hope that the advantages of automation are retained, and that some of its disadvantages are overcome. To achieve our goal, we use the interactive theorem prover hol as a framework for supporting the theory of observational congruence of ccs, and provide a set of automatic proof tools, based on the algebraic axiomatization of the language, which can be used interactively. To illustrate how interaction and automation can be intermixed, we describe two verification strategies which exhibit different degrees of user interaction.
1991, Contributo in atti di convegno, ENG
Inverardi P.; Nesi M.
This paper concerns a verification system for process algebras formalisms based entirely on equational reasoning. One aspect of the kind of reasoning we want to do, the so-called automatic reasoning, that is, the possibility of equipping the axiomatic presentations of various behavioural equivalences with equivalent rewriting relations is analyzed. The problems and the adopted solutions to deal with observational congruence are discussed.