-
Towards reduction of Paradigm coordination models
Authors:
Suzana Andova,
Luuk Groenewegen,
Erik de Vink
Abstract:
The coordination modelling language Paradigm addresses collaboration between components in terms of dynamic constraints. Within a Paradigm model, component dynamics are consistently specified at a detailed and a global level of abstraction. To enable automated verification of Paradigm models, a translation of Paradigm into process algebra has been defined in previous work. In this paper we invest…
▽ More
The coordination modelling language Paradigm addresses collaboration between components in terms of dynamic constraints. Within a Paradigm model, component dynamics are consistently specified at a detailed and a global level of abstraction. To enable automated verification of Paradigm models, a translation of Paradigm into process algebra has been defined in previous work. In this paper we investigate, guided by a client-server example, reduction of Paradigm models based on a notion of global inertness. Representation of Paradigm models as process algebraic specifications helps to establish a property-preserving equivalence relation between the original and the reduced Paradigm model. Experiments indicate that in this way larger Paradigm models can be analyzed.
△ Less
Submitted 9 August, 2011;
originally announced August 2011.
-
Prototyping the Semantics of a DSL using ASF+SDF: Link to Formal Verification of DSL Models
Authors:
Suzana Andova,
Mark van den Brand,
Luc Engelen
Abstract:
A formal definition of the semantics of a domain-specific language (DSL) is a key prerequisite for the verification of the correctness of models specified using such a DSL and of transformations applied to these models. For this reason, we implemented a prototype of the semantics of a DSL for the specification of systems consisting of concurrent, communicating objects. Using this prototype, models…
▽ More
A formal definition of the semantics of a domain-specific language (DSL) is a key prerequisite for the verification of the correctness of models specified using such a DSL and of transformations applied to these models. For this reason, we implemented a prototype of the semantics of a DSL for the specification of systems consisting of concurrent, communicating objects. Using this prototype, models specified in the DSL can be transformed to labeled transition systems (LTS). This approach of transforming models to LTSs allows us to apply existing tools for visualization and verification to models with little or no further effort. The prototype is implemented using the ASF+SDF Meta-Environment, an IDE for the algebraic specification language ASF+SDF, which offers efficient execution of the transformation as well as the ability to read models and produce LTSs without any additional pre or post processing.
△ Less
Submitted 30 June, 2011;
originally announced July 2011.
-
Testing Reactive Probabilistic Processes
Authors:
Sonja Georgievska,
Suzana Andova
Abstract:
We define a testing equivalence in the spirit of De Nicola and Hennessy for reactive probabilistic processes, i.e. for processes where the internal nondeterminism is due to random behaviour. We characterize the testing equivalence in terms of ready-traces. From the characterization it follows that the equivalence is insensitive to the exact moment in time in which an internal probabilistic choice…
▽ More
We define a testing equivalence in the spirit of De Nicola and Hennessy for reactive probabilistic processes, i.e. for processes where the internal nondeterminism is due to random behaviour. We characterize the testing equivalence in terms of ready-traces. From the characterization it follows that the equivalence is insensitive to the exact moment in time in which an internal probabilistic choice occurs, which is inherent from the original testing equivalence of De Nicola and Hennessy. We also show decidability of the testing equivalence for finite systems for which the complete model may not be known.
△ Less
Submitted 25 June, 2010;
originally announced June 2010.
-
Proceedings First Workshop on Quantitative Formal Methods: Theory and Applications
Authors:
Suzana Andova,
Annabelle McIver,
Pedro D'Argenio,
Pieter Cuijpers,
Jasen Markovski,
Caroll Morgan,
Manuel Núñez
Abstract:
This volume contains the papers presented at the 1st workshop on Quantitative Formal Methods: Theory and Applications, which was held in Eindhoven on 3 November 2009 as part of the International Symposium on Formal Methods 2009. This volume contains the final versions of all contributions accepted for presentation at the workshop.
This volume contains the papers presented at the 1st workshop on Quantitative Formal Methods: Theory and Applications, which was held in Eindhoven on 3 November 2009 as part of the International Symposium on Formal Methods 2009. This volume contains the final versions of all contributions accepted for presentation at the workshop.
△ Less
Submitted 10 December, 2009;
originally announced December 2009.
-
Testing Probabilistic Processes: Can Random Choices Be Unobservable?
Authors:
Sonja Georgievska,
Suzana Andova
Abstract:
A central paradigm behind process semantics based on observability and testing is that the exact moment of occurring of an internal nondeterministic choice is unobservable. It is natural, therefore, for this property to hold when the internal choice is quantified with probabilities. However, ever since probabilities have been introduced in process semantics, it has been a challenge to preserve t…
▽ More
A central paradigm behind process semantics based on observability and testing is that the exact moment of occurring of an internal nondeterministic choice is unobservable. It is natural, therefore, for this property to hold when the internal choice is quantified with probabilities. However, ever since probabilities have been introduced in process semantics, it has been a challenge to preserve the unobservability of the random choice, while not violating the other laws of process theory and probability theory. This paper addresses this problem. It proposes two semantics for processes where the internal nondeterminism has been quantified with probabilities. The first one is based on the notion of testing, i.e. interaction between the process and its environment. The second one, the probabilistic ready trace semantics, is based on the notion of observability. Both are shown to coincide. They are also preserved under the standard operators.
△ Less
Submitted 9 July, 2009;
originally announced July 2009.
-
A framework for compositional verification of security protocols
Authors:
Suzana Andova,
Cas Cremers,
Kristian Gjosteen,
Sjouke Mauw,
Stig F. Mjolsnes,
Sasa Radomirovic
Abstract:
Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach.
We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verifi…
▽ More
Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach.
We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verification of large structured security protocols. Our approach is to verify properties of component protocols in a multi-protocol environment, then deduce properties about the composed protocol. To reduce the complexity of multi-protocol verification, we introduce a notion of protocol independence and prove a number of theorems that enable analysis of independent component protocols in isolation.
To illustrate the applicability of our framework to real-world protocols, we study a key establishment sequence in WiMax consisting of three subprotocols. Except for a small amount of trivial reasoning, the analysis is done using automatic tools.
△ Less
Submitted 1 May, 2007; v1 submitted 14 November, 2006;
originally announced November 2006.
