17 Result(s)
within
Gian-Luigi Ferrari
Mathematical Logic and Formal Languages
-
Chapter
Automata-Based Behavioural Contracts with Action Correlation
The rigorous design of Service-Oriented Computing (SOC) applications has been identified as one of the primary research challenges for the next 10 years. Many foundational theories for SOC have been defined, ...
-
Chapter
Last Mile’s Resources
We extend an existing two-phase static analysis for an adaptive programming language to also deal with dynamic resources. The focus of our analysis is on predicting how these are used, in spite of the differen...
-
Chapter and Conference Paper
Playing with Our CAT and Communication-Centric Applications
We describe CAT, a toolkit supporting the analysis of communication-centric applications, i.e., applications consisting of ensembles of interacting services. Services are modelled in CAT as contract automata and ...
-
Chapter and Conference Paper
A Two-Phase Static Analysis for Reliable Adaptation
Adaptive systems are designed to modify their behaviour in response to changes of their operational environment. We adopt a language-based approach to the development of such systems, with particular attention...
-
Chapter and Conference Paper
Automata for Analysing Service Contracts
A novel approach to the formal description of service contracts is presented in terms of automata. We focus on the basic property of guaranteeing that in the multi-party composition of principals each individu...
-
Chapter and Conference Paper
Towards Nominal Context-Free Model-Checking
Two kinds of automata are introduced, for recognising regular and context-free nominal languages. We compare their expressive power with that of analogous proposals in the literature. Some properties of our la...
-
Chapter and Conference Paper
Nominal Automata for Resource Usage Control
Two classes of nominal automata, namely Usage Automata (UAs) and Variable Finite Automata (VFAs) are considered to express resource control policies over program execution traces expressed by a nominal calculus (
-
Chapter
Ugo Montanari and Software Verification
The great honour of introducing the Chapter on Software Verification for the Festschrift dedicated to Ugo Montanari brings to mind a very personal memory. I was a young Ph.D. student and I was discussing somethin...
-
Chapter
Event-Based Service Coordination
In this paper we tackle the problem of designing and implementing a framework for programming service coordination policies. In particular, we illustrate the design and the prototype implementation of Java Sig...
-
Chapter
History Dependent Automata for Service Compatibility
We use History Dependent Automata (HD-Automata) as a syntax-indepentend formalism to check compatibility of services at binding time in Service-Oriented Computing.
-
Chapter and Conference Paper
Types and Effects for Resource Usage Analysis
An extension of the λ-calculus is proposed, to study resource usage analysis and verification. Resources can be dynamically created, and passed / returned by functions; their usages have side effects, represented...
-
Chapter and Conference Paper
History-Based Access Control with Local Policies
An extension of the λ-calculus is proposed, to study history-based access control. It allows for security policies with a possibly nested, local scope. We define a type and effect system that, given a program, ex...
-
Chapter and Conference Paper
Checking Risky Events Is Enough for Local Policies
An extension of the λ-calculus is proposed to study history-based access control. It allows for parametrized security policies with a possibly nested, local scope. To govern the rich interplay between local polic...
-
Chapter and Conference Paper
Model Checking for Nominal Calculi
Nominal calculi have been shown very effective to formally model a variety of computational phenomena. The models of nominal calculi have often infinite states, thus making model checking a difficult task. In ...
-
Chapter and Conference Paper
Security-Aware Program Transformations
Stack inspection is a basic mechanism for implementing language based security. Stack inspection is time consuming and may prevent from code optimization. A static analysis is presented that safely approximate...
-
Chapter and Conference Paper
On causality observed incrementally, finally
One of the main problems of the partial ordering approach to the description of computations of concurrent and distributed systems is that there is no operation of sequential composition for partial orders whi...
-
Chapter and Conference Paper
Transition systems with algebraic structure as models of computations
This paper is a tutorial introduction to a general methodology, consisting of categorical constructions, for the definition of new algebraic semantics for transition-based formalisms. The methodology individua...
