From Flow Logic to static type systems for coordination languages

Rocco De Nicola; Daniele Gorla; Rene Rydhof Hansen; Flemming Nielson; Hanne Riis Nielson; Christian W. Probst; Rosario Pugliese

doi:10.1016/j.scico.2009.07.009

From Flow Logic to static type systems for coordination languages

Rocco De Nicola, Daniele Gorla, Rene Rydhof Hansen, Flemming Nielson, Hanne Riis Nielson, Christian W. Probst, Rosario Pugliese

Research output: Contribution to journal › Conference article › Research › peer-review

Abstract

Coordination languages are often used to describe open-ended systems. This makes it challenging to develop tools for guaranteeing the security of the coordinated systems and the correctness of their interaction. Successful approaches to this problem have been based on type systems with dynamic checks; therefore, the correctness properties cannot be statically enforced. By contrast, static analysis approaches based on Flow Logic usually guarantee properties statically. In this paper, we show how the insights from the Flow Logic approach can be used to construct a type system for statically ensuring secure access to tuple spaces and safe process migration for an extension of the language KLAIM. (C) 2009 Elsevier B.V. All rights reserved.

Original language	English
Journal	Science of Computer Programming
Volume	75
Issue number	6
Pages (from-to)	376-397
ISSN	0167-6423
DOIs	https://doi.org/10.1016/j.scico.2009.07.009
Publication status	Published - 2010
Event	10th International Conference Coordination Models and Languages - Oslo, Norway Duration: 4 Jun 2008 → 6 Jun 2008 Conference number: 10 http://www.informatik.uni-trier.de/~ley/db/conf/coordination/coordination2008.html

Conference

Conference	10th International Conference Coordination Models and Languages
Number	10
Country/Territory	Norway
City	Oslo
Period	04/06/2008 → 06/06/2008
Internet address	http://www.informatik.uni-trier.de/~ley/db/conf/coordination/coordination2008.html

Access to Document

10.1016/j.scico.2009.07.009

OpenUrl availability

Full text

Cite this

@inproceedings{7c5b5b4734e84f9793033328c8c9f91f,

title = "From Flow Logic to static type systems for coordination languages",

abstract = "Coordination languages are often used to describe open-ended systems. This makes it challenging to develop tools for guaranteeing the security of the coordinated systems and the correctness of their interaction. Successful approaches to this problem have been based on type systems with dynamic checks; therefore, the correctness properties cannot be statically enforced. By contrast, static analysis approaches based on Flow Logic usually guarantee properties statically. In this paper, we show how the insights from the Flow Logic approach can be used to construct a type system for statically ensuring secure access to tuple spaces and safe process migration for an extension of the language KLAIM. (C) 2009 Elsevier B.V. All rights reserved.",

author = "\{De Nicola\}, Rocco and Daniele Gorla and Hansen, \{Rene Rydhof\} and Flemming Nielson and Nielson, \{Hanne Riis\} and Probst, \{Christian W.\} and Rosario Pugliese",

year = "2010",

doi = "10.1016/j.scico.2009.07.009",

language = "English",

volume = "75",

pages = "376--397",

journal = "Science of Computer Programming",

issn = "0167-6423",

publisher = "Elsevier",

number = "6",

note = "10th International Conference Coordination Models and Languages, COORDINATION 2008 ; Conference date: 04-06-2008 Through 06-06-2008",

url = "http://www.informatik.uni-trier.de/\textasciitilde{}ley/db/conf/coordination/coordination2008.html",

}

TY - GEN

T1 - From Flow Logic to static type systems for coordination languages

AU - De Nicola, Rocco

AU - Gorla, Daniele

AU - Hansen, Rene Rydhof

AU - Nielson, Flemming

AU - Nielson, Hanne Riis

AU - Probst, Christian W.

AU - Pugliese, Rosario

N1 - Conference code: 10

PY - 2010

Y1 - 2010

N2 - Coordination languages are often used to describe open-ended systems. This makes it challenging to develop tools for guaranteeing the security of the coordinated systems and the correctness of their interaction. Successful approaches to this problem have been based on type systems with dynamic checks; therefore, the correctness properties cannot be statically enforced. By contrast, static analysis approaches based on Flow Logic usually guarantee properties statically. In this paper, we show how the insights from the Flow Logic approach can be used to construct a type system for statically ensuring secure access to tuple spaces and safe process migration for an extension of the language KLAIM. (C) 2009 Elsevier B.V. All rights reserved.

AB - Coordination languages are often used to describe open-ended systems. This makes it challenging to develop tools for guaranteeing the security of the coordinated systems and the correctness of their interaction. Successful approaches to this problem have been based on type systems with dynamic checks; therefore, the correctness properties cannot be statically enforced. By contrast, static analysis approaches based on Flow Logic usually guarantee properties statically. In this paper, we show how the insights from the Flow Logic approach can be used to construct a type system for statically ensuring secure access to tuple spaces and safe process migration for an extension of the language KLAIM. (C) 2009 Elsevier B.V. All rights reserved.

U2 - 10.1016/j.scico.2009.07.009

DO - 10.1016/j.scico.2009.07.009

M3 - Conference article

SN - 0167-6423

VL - 75

SP - 376

EP - 397

JO - Science of Computer Programming

JF - Science of Computer Programming

IS - 6

T2 - 10th International Conference Coordination Models and Languages

Y2 - 4 June 2008 through 6 June 2008

ER -

From Flow Logic to static type systems for coordination languages

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this