Preservation and reflection in specification

Antónia Lopes; José Luiz Fiadeiro

doi:10.1007/BFb0000484

Preservation and reflection in specification

Antónia Lopes
, José Luiz Fiadeiro

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

7 Citations (Scopus)

Abstract

We extend the traditional notion of specification based on theories and interpretations between theories to model situations, typical of open, reactive systems, in which properties exhibited locally by an object no longer hold when that object is interconnected as a component of a larger system. The proposed notion of specification is based on the observation, due to Winskel, that while some assertions are preserved across morphisms of labelled transition systems, other are reflected. The distinction between these two classes of assertions leads us to the definition of two categories of specifications, one that supports horizontal structuring and another that supports vertical structuring, for which compositionality is proved.

Original language	English
Title of host publication	AMAST 1997
Subtitle of host publication	Algebraic Methodology and Software Technology
Editors	M. Johnson
Place of Publication	Berlin
Publisher	Springer Verlag
Pages	380-394
Number of pages	15
ISBN (Electronic)	9783540696612
ISBN (Print)	9783540638889
DOIs	https://doi.org/10.1007/BFb0000484
Publication status	Published - 1997
Event	AMAST '97: Algebraic Methodology and Software Technology.: 6th International Conference - Sydney, Australia Duration: 12 Dec 1997 → 17 Dec 1997

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	1349

Conference

Conference	AMAST '97: Algebraic Methodology and Software Technology.
Country/Territory	Australia
City	Sydney
Period	12/12/97 → 17/12/97

Keywords

Temporal Logic
Label Transition System
State Proposition
Synchronisation Point
Local Logic

Access to Document

10.1007/BFb0000484

Cite this

@inproceedings{54e3734357ec41aead12986f773be23f,

title = "Preservation and reflection in specification",

abstract = "We extend the traditional notion of specification based on theories and interpretations between theories to model situations, typical of open, reactive systems, in which properties exhibited locally by an object no longer hold when that object is interconnected as a component of a larger system. The proposed notion of specification is based on the observation, due to Winskel, that while some assertions are preserved across morphisms of labelled transition systems, other are reflected. The distinction between these two classes of assertions leads us to the definition of two categories of specifications, one that supports horizontal structuring and another that supports vertical structuring, for which compositionality is proved.",

keywords = "Temporal Logic, Label Transition System, State Proposition, Synchronisation Point, Local Logic",

author = "Ant{\'o}nia Lopes and Fiadeiro, \{Jos{\'e} Luiz\}",

year = "1997",

doi = "10.1007/BFb0000484",

language = "English",

isbn = "9783540638889",

series = " Lecture Notes in Computer Science",

publisher = "Springer Verlag",

pages = "380--394",

editor = "M. Johnson",

booktitle = "AMAST 1997",

address = "Germany",

note = "AMAST '97: Algebraic Methodology and Software Technology. : 6th International Conference ; Conference date: 12-12-1997 Through 17-12-1997",

}

TY - GEN

T1 - Preservation and reflection in specification

AU - Lopes, Antónia

AU - Fiadeiro, José Luiz

PY - 1997

Y1 - 1997

N2 - We extend the traditional notion of specification based on theories and interpretations between theories to model situations, typical of open, reactive systems, in which properties exhibited locally by an object no longer hold when that object is interconnected as a component of a larger system. The proposed notion of specification is based on the observation, due to Winskel, that while some assertions are preserved across morphisms of labelled transition systems, other are reflected. The distinction between these two classes of assertions leads us to the definition of two categories of specifications, one that supports horizontal structuring and another that supports vertical structuring, for which compositionality is proved.

AB - We extend the traditional notion of specification based on theories and interpretations between theories to model situations, typical of open, reactive systems, in which properties exhibited locally by an object no longer hold when that object is interconnected as a component of a larger system. The proposed notion of specification is based on the observation, due to Winskel, that while some assertions are preserved across morphisms of labelled transition systems, other are reflected. The distinction between these two classes of assertions leads us to the definition of two categories of specifications, one that supports horizontal structuring and another that supports vertical structuring, for which compositionality is proved.

KW - Temporal Logic

KW - Label Transition System

KW - State Proposition

KW - Synchronisation Point

KW - Local Logic

U2 - 10.1007/BFb0000484

DO - 10.1007/BFb0000484

M3 - Conference contribution

SN - 9783540638889

T3 - Lecture Notes in Computer Science

SP - 380

EP - 394

BT - AMAST 1997

A2 - Johnson, M.

PB - Springer Verlag

CY - Berlin

T2 - AMAST '97: Algebraic Methodology and Software Technology.

Y2 - 12 December 1997 through 17 December 1997

ER -

Preservation and reflection in specification

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this