Applying Generalized Non Deducibility on Compositions (GNDC) Approach in Dependability

S. Gnesi, G. Lenzini, F. Martinelli

Research output: Contribution to journalArticleAcademicpeer-review

2 Downloads (Pure)

Abstract

This paper presents a framework where dependable systems can be uniformly modeled and dependable properties analyzed within the Generalized Non Deducibility on Compositions (GNDC), a scheme that has been profitably used in definition and analysis of security properties. Precisely, our framework requires a systems to be modelled using a formal calculus, here the CCS process algebra, where both the failing behaviour of the system and the related fault-recovering procedures are also explicitly described. An environment able to inject any fault in the system is then defined as a separated component. The parallel composition between the system and the environment represents our scenario of analysis, where some fault tolerance property (e.g. fail stop, safe and silent) are studied as instances of GNDC properties. By using different instances of \gndc we are able to argue about the availability of effective methodologies of analysis, and on the possibility of applying compositional techniques.
Original languageEnglish
Pages (from-to)111-126
Number of pages16
JournalElectronic notes in theoretical computer science
Volume99
DOIs
Publication statusPublished - Aug 2004
Externally publishedYes
EventMEFISTO Project 2003 : Formal Methods for Security and Time - Pisa, Italy
Duration: 3 Nov 20035 Nov 2003

Fingerprint

Dependability
Chemical analysis
Fault tolerance
Fault
Algebra
Parallel Composition
Availability
Process Algebra
Fault Tolerance
Calculus
Scenarios
Methodology
Framework

Keywords

  • Dependability
  • Fault tolerance
  • Security
  • Non interference
  • Formal verification

Cite this

@article{999b3883965b4befad88a429934dd3fe,
title = "Applying Generalized Non Deducibility on Compositions (GNDC) Approach in Dependability",
abstract = "This paper presents a framework where dependable systems can be uniformly modeled and dependable properties analyzed within the Generalized Non Deducibility on Compositions (GNDC), a scheme that has been profitably used in definition and analysis of security properties. Precisely, our framework requires a systems to be modelled using a formal calculus, here the CCS process algebra, where both the failing behaviour of the system and the related fault-recovering procedures are also explicitly described. An environment able to inject any fault in the system is then defined as a separated component. The parallel composition between the system and the environment represents our scenario of analysis, where some fault tolerance property (e.g. fail stop, safe and silent) are studied as instances of GNDC properties. By using different instances of \gndc we are able to argue about the availability of effective methodologies of analysis, and on the possibility of applying compositional techniques.",
keywords = "Dependability, Fault tolerance, Security, Non interference, Formal verification",
author = "S. Gnesi and G. Lenzini and F. Martinelli",
year = "2004",
month = "8",
doi = "10.1016/j.entcs.2004.02.005",
language = "English",
volume = "99",
pages = "111--126",
journal = "Electronic notes in theoretical computer science",
issn = "1571-0661",
publisher = "Elsevier",

}

Applying Generalized Non Deducibility on Compositions (GNDC) Approach in Dependability. / Gnesi, S.; Lenzini, G.; Martinelli, F.

In: Electronic notes in theoretical computer science, Vol. 99, 08.2004, p. 111-126.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Applying Generalized Non Deducibility on Compositions (GNDC) Approach in Dependability

AU - Gnesi, S.

AU - Lenzini, G.

AU - Martinelli, F.

PY - 2004/8

Y1 - 2004/8

N2 - This paper presents a framework where dependable systems can be uniformly modeled and dependable properties analyzed within the Generalized Non Deducibility on Compositions (GNDC), a scheme that has been profitably used in definition and analysis of security properties. Precisely, our framework requires a systems to be modelled using a formal calculus, here the CCS process algebra, where both the failing behaviour of the system and the related fault-recovering procedures are also explicitly described. An environment able to inject any fault in the system is then defined as a separated component. The parallel composition between the system and the environment represents our scenario of analysis, where some fault tolerance property (e.g. fail stop, safe and silent) are studied as instances of GNDC properties. By using different instances of \gndc we are able to argue about the availability of effective methodologies of analysis, and on the possibility of applying compositional techniques.

AB - This paper presents a framework where dependable systems can be uniformly modeled and dependable properties analyzed within the Generalized Non Deducibility on Compositions (GNDC), a scheme that has been profitably used in definition and analysis of security properties. Precisely, our framework requires a systems to be modelled using a formal calculus, here the CCS process algebra, where both the failing behaviour of the system and the related fault-recovering procedures are also explicitly described. An environment able to inject any fault in the system is then defined as a separated component. The parallel composition between the system and the environment represents our scenario of analysis, where some fault tolerance property (e.g. fail stop, safe and silent) are studied as instances of GNDC properties. By using different instances of \gndc we are able to argue about the availability of effective methodologies of analysis, and on the possibility of applying compositional techniques.

KW - Dependability

KW - Fault tolerance

KW - Security

KW - Non interference

KW - Formal verification

U2 - 10.1016/j.entcs.2004.02.005

DO - 10.1016/j.entcs.2004.02.005

M3 - Article

VL - 99

SP - 111

EP - 126

JO - Electronic notes in theoretical computer science

JF - Electronic notes in theoretical computer science

SN - 1571-0661

ER -