-
Chapter
Towards a Proof Method for Paradigm
The paper describes two perspectives on a verification approach for Paradigm, a coordination modeling language specifying an architecture in terms of components and their collaborations. One perspective concen...
-
Article
Open AccessReconciling real and stochastic time: the need for probabilistic refinement
We conservatively extend an ACP-style discrete-time process theory with discrete stochastic delays. The semantics of the timed delays relies on time additivity and time determinism, which are properties that e...
-
Chapter and Conference Paper
Distributed Adaption of Dining Philosophers
Adaptation of a component-based system can be achieved in the coordination modelling language Paradigm through the special component McPal. McPal regulates the propagation of new behaviour and guides the chang...
-
Chapter and Conference Paper
Towards Dynamic Adaptation of Probabilistic Systems
Dynamic system adaptation is modeled in the coordination language Paradigm as coordination of collaborating components. A special component McPal allows for addition of new behavior, of new constraints and of ...
-
Chapter
In Silico Modelling and Analysis of Ribosome Kinetics and aa-tRNA Competition
We present a formal analysis of ribosome kinetics using probabilistic model checking and the tool Prism. We compute different parameters of the model, like probabilities of translation errors and average inser...
-
Chapter and Conference Paper
Stochastic Analysis of Amino Acid Substitution in Protein Synthesis
We present a formal analysis of amino acid replacement during mRNA translation. Building on an abstract stochastic model of arrival of tRNAs and their processing at the ribosome, we compute probabilities of th...
-
Chapter and Conference Paper
An Operation-Based Metric for CPA Resistance
Differential power analysis (DPA) is a strong attack upon cryptographic devices such as smartcards. Correlation power analysis (CPA) is a specific form of DPA where the Hamming-weight and the correlation coeff...
-
Chapter and Conference Paper
Compositionality for Markov Reward Chains with Fast Transitions
A parallel composition is defined for Markov reward chains with fast transitions and for discontinuous Markov reward chains. In this setting, compositionality with respect to the relevant aggregation preorders...
-
Chapter and Conference Paper
Formalising Receipt-Freeness
Receipt-freeness is the property of voting protocols that a voter cannot create a receipt which proves how she voted. Since Benaloh and Tuinstra introduced this property, there has been a large amount of work ...
-
Chapter and Conference Paper
A Formalization of Anonymity and Onion Routing
The use of formal methods to verify security protocols with respect to secrecy and authentication has become standard practice. In contrast, the formalization of other security goals, such as privacy, has rece...
-
Chapter and Conference Paper
Axiomatizing GSOS with Termination
We discuss a combination of GSOS-type structural operational semantics with explicit termination, that we call the tagh-format (tagh being short for termination and GSOS hybrid).The tagh-format distinguishes betw...
-
Chapter and Conference Paper
Bisimulation for probabilistic transition systems: A coalgebraic approach
The notion of bisimulation as proposed by Larsen and Skou for discrete probabilistic transition systems is shown to coincide with a coalgebraic definition in the sense of Aczel and Mendier in terms of a set fu...
-
Chapter and Conference Paper
Transition system specifications in stalk format with bisimulation as a congruence
A many-sorted variant, called stalk format, of the single sorted tyft-format for transition system specifications, introduced by Groote and Vaandrager, is proposed. The stalk format is shown to be a convenient...
-
Article
Rendez-vous with metric semantics
A comparative semantic study is made of an element of the family of concurrent object-oriented programming languages. Particular attention is paid to two notions: (i) dynamically evolving process structures, i...
-
Chapter and Conference Paper
Asynchronous rendez-vous in distributed logic programming
In this paper the semantics of the communication mechanism of the distributed logic programming language DLP is studied. DLP combines logic programming with object oriented features and parallelism. For an abs...
-
Chapter and Conference Paper
Rendez-Vous with Metric Semantics
A comparative semantic study is made of an element of the family of concurrent object-oriented programming languages. Particular attention is paid to two notions: (i) dynamically evolving process structures, i...
-
Chapter and Conference Paper
Rendez-vous with metric semantics
A comparative semantic study is made of an element of the family of concurrent object-oriented programming languages. Particular attention is paid to two notions: (i) dynamically evolving process structures, i...
-
Chapter and Conference Paper
CCS for OO and LP
We illustrate the design of comparative continuation semantics for object-oriented and logic programming languages by three case studies dealing with process creation, backtracking and rendez-vous. Operational...
-
Chapter and Conference Paper
Retractions in comparing prolog semantics (extended abstract)
We present an operational model O and a continuation based denotational model D for a uniform variant of Prolog, including the cut operator. The two semantical definitions make use of higher order transformations...
-
Article
Step semantics for “true” concurrency with recursion
We present a variety of denotational linear time semantics for a language with recursion and “true” concurrency in a form of synchronous co-operation, which in the literature is known as step semantics. We sho...
