By the same authors

Stateful-Failure Reactive Designs in Isabelle/UTP

Research output: Working paper

Standard

Stateful-Failure Reactive Designs in Isabelle/UTP. / Foster, Simon David; Baxter, James Edward; Cavalcanti, Ana Lucia Caneca; Woodcock, JAMES Charles Paul.

2018.

Research output: Working paper

Harvard

Foster, SD, Baxter, JE, Cavalcanti, ALC & Woodcock, JAMESCP 2018 'Stateful-Failure Reactive Designs in Isabelle/UTP'.

APA

Foster, S. D., Baxter, J. E., Cavalcanti, A. L. C., & Woodcock, JAMES. C. P. (2018). Stateful-Failure Reactive Designs in Isabelle/UTP.

Vancouver

Foster SD, Baxter JE, Cavalcanti ALC, Woodcock JAMESCP. Stateful-Failure Reactive Designs in Isabelle/UTP. 2018 Apr 17.

Author

Foster, Simon David ; Baxter, James Edward ; Cavalcanti, Ana Lucia Caneca ; Woodcock, JAMES Charles Paul. / Stateful-Failure Reactive Designs in Isabelle/UTP. 2018.

Bibtex - Download

@techreport{cb1b9f382b9b4b0bb0cfd0f02f0306b7,
title = "Stateful-Failure Reactive Designs in Isabelle/UTP",
abstract = "Stateful-Failure Reactive Designs specialise reactive design contracts with failures traces,as present in languages like CSP and Circus. A failure trace consists of a sequence of events and a refusal set. It intuitively represents a quiescent observation, where certain events have previously occurred, and others are currently being accepted. Following the UTP book, we add an observational variable to represent refusal sets, and healthiness conditions that ensure their well-formedness. Using these, we also specialise our theory of reactive relations with operators to characterise both completed and quiescent interactions, and an accompanying equational theory. We use these to define the core operators — including assignment, event occurrence, and external choice — and specialise our proof strategy to support these. We also demonstrate a link with the CSP failures-divergences semantic model.",
author = "Foster, {Simon David} and Baxter, {James Edward} and Cavalcanti, {Ana Lucia Caneca} and Woodcock, {JAMES Charles Paul}",
year = "2018",
month = apr,
day = "17",
language = "English",
type = "WorkingPaper",

}

RIS (suitable for import to EndNote) - Download

TY - UNPB

T1 - Stateful-Failure Reactive Designs in Isabelle/UTP

AU - Foster, Simon David

AU - Baxter, James Edward

AU - Cavalcanti, Ana Lucia Caneca

AU - Woodcock, JAMES Charles Paul

PY - 2018/4/17

Y1 - 2018/4/17

N2 - Stateful-Failure Reactive Designs specialise reactive design contracts with failures traces,as present in languages like CSP and Circus. A failure trace consists of a sequence of events and a refusal set. It intuitively represents a quiescent observation, where certain events have previously occurred, and others are currently being accepted. Following the UTP book, we add an observational variable to represent refusal sets, and healthiness conditions that ensure their well-formedness. Using these, we also specialise our theory of reactive relations with operators to characterise both completed and quiescent interactions, and an accompanying equational theory. We use these to define the core operators — including assignment, event occurrence, and external choice — and specialise our proof strategy to support these. We also demonstrate a link with the CSP failures-divergences semantic model.

AB - Stateful-Failure Reactive Designs specialise reactive design contracts with failures traces,as present in languages like CSP and Circus. A failure trace consists of a sequence of events and a refusal set. It intuitively represents a quiescent observation, where certain events have previously occurred, and others are currently being accepted. Following the UTP book, we add an observational variable to represent refusal sets, and healthiness conditions that ensure their well-formedness. Using these, we also specialise our theory of reactive relations with operators to characterise both completed and quiescent interactions, and an accompanying equational theory. We use these to define the core operators — including assignment, event occurrence, and external choice — and specialise our proof strategy to support these. We also demonstrate a link with the CSP failures-divergences semantic model.

M3 - Working paper

BT - Stateful-Failure Reactive Designs in Isabelle/UTP

ER -