Invariant-based synthesis of fault-tolerant systems

K Lano; David Clark; K Androutsopoulos; P Kan

Invariant-based synthesis of fault-tolerant systems

K Lano, David Clark, K Androutsopoulos, P Kan

Research output: Chapter in Book/Report/Conference proceeding › Conference paper

5 Citations (Scopus)

Abstract

Statecharts are a very widely used formalism for reactive system development, however, there are problems in using them as a fully formal specification notation because of the conflicting variants of statechart semantics which exist. In this paper a modular subset of statechart notation is defined which has a simple semantics, and permits compositional development and verification. Techniques for decomposing specifications in this notation, design strategies for incorporating fault tolerance, and translation to the B formal language, are also described, and illustrated with extracts from a case study of a fault tolerant system.

Original language	English
Title of host publication	Formal Techniques in Real-Time and Fault-Tolerant Systems
Subtitle of host publication	6th International Symposium, FTRTFT 2000 Pune, India, September 20-22, 2000, Proceedings
Place of Publication	Berlin, Germany
Publisher	Springer
Pages	46 - 57
Number of pages	12
Volume	N/A
Edition	N/A
ISBN (Print)	3540410554
Publication status	Published - 2000
Event	FTRTFT 2000: Formal Techniques in Real-Time and Fault-Tolerant Systems - 6th International Symposium Proceedings - Pune, India Duration: 20 Sept 2000 → 22 Sept 2000

Publication series

Name	Lecture notes in computer science
Publisher	Springer
Volume	1926

Conference

Conference	FTRTFT 2000: Formal Techniques in Real-Time and Fault-Tolerant Systems - 6th International Symposium Proceedings
Country/Territory	India
City	Pune
Period	20/09/2000 → 22/09/2000

Cite this

@inbook{2f0068414f3a4192b0bec4b9a1c2b548,

title = "Invariant-based synthesis of fault-tolerant systems",

abstract = "Statecharts are a very widely used formalism for reactive system development, however, there are problems in using them as a fully formal specification notation because of the conflicting variants of statechart semantics which exist. In this paper a modular subset of statechart notation is defined which has a simple semantics, and permits compositional development and verification. Techniques for decomposing specifications in this notation, design strategies for incorporating fault tolerance, and translation to the B formal language, are also described, and illustrated with extracts from a case study of a fault tolerant system.",

author = "K Lano and David Clark and K Androutsopoulos and P Kan",

year = "2000",

language = "English",

isbn = "3540410554",

volume = "N/A",

series = "Lecture notes in computer science",

publisher = "Springer",

pages = "46 -- 57",

booktitle = "Formal Techniques in Real-Time and Fault-Tolerant Systems",

edition = "N/A",

note = "FTRTFT 2000: Formal Techniques in Real-Time and Fault-Tolerant Systems - 6th International Symposium Proceedings ; Conference date: 20-09-2000 Through 22-09-2000",

}

Lano, K , Clark, D, Androutsopoulos, K & Kan, P 2000, Invariant-based synthesis of fault-tolerant systems. in Formal Techniques in Real-Time and Fault-Tolerant Systems: 6th International Symposium, FTRTFT 2000 Pune, India, September 20-22, 2000, Proceedings. N/A edn, vol. N/A, Lecture notes in computer science, vol. 1926, Springer, Berlin, Germany, pp. 46 - 57, FTRTFT 2000: Formal Techniques in Real-Time and Fault-Tolerant Systems - 6th International Symposium Proceedings, Pune, India, 20/09/2000.

Invariant-based synthesis of fault-tolerant systems. / Lano, K ; Clark, David; Androutsopoulos, K et al.
Formal Techniques in Real-Time and Fault-Tolerant Systems: 6th International Symposium, FTRTFT 2000 Pune, India, September 20-22, 2000, Proceedings. Vol. N/A N/A. ed. Berlin, Germany: Springer, 2000. p. 46 - 57 (Lecture notes in computer science; Vol. 1926).

Research output: Chapter in Book/Report/Conference proceeding › Conference paper

TY - CHAP

T1 - Invariant-based synthesis of fault-tolerant systems

AU - Lano, K

AU - Clark, David

AU - Androutsopoulos, K

AU - Kan, P

PY - 2000

Y1 - 2000

N2 - Statecharts are a very widely used formalism for reactive system development, however, there are problems in using them as a fully formal specification notation because of the conflicting variants of statechart semantics which exist. In this paper a modular subset of statechart notation is defined which has a simple semantics, and permits compositional development and verification. Techniques for decomposing specifications in this notation, design strategies for incorporating fault tolerance, and translation to the B formal language, are also described, and illustrated with extracts from a case study of a fault tolerant system.

AB - Statecharts are a very widely used formalism for reactive system development, however, there are problems in using them as a fully formal specification notation because of the conflicting variants of statechart semantics which exist. In this paper a modular subset of statechart notation is defined which has a simple semantics, and permits compositional development and verification. Techniques for decomposing specifications in this notation, design strategies for incorporating fault tolerance, and translation to the B formal language, are also described, and illustrated with extracts from a case study of a fault tolerant system.

M3 - Conference paper

SN - 3540410554

VL - N/A

T3 - Lecture notes in computer science

SP - 46

EP - 57

BT - Formal Techniques in Real-Time and Fault-Tolerant Systems

PB - Springer

CY - Berlin, Germany

T2 - FTRTFT 2000: Formal Techniques in Real-Time and Fault-Tolerant Systems - 6th International Symposium Proceedings

Y2 - 20 September 2000 through 22 September 2000

ER -

Invariant-based synthesis of fault-tolerant systems

Abstract

Publication series

Conference

Fingerprint

Cite this