A modal specification theory for components with data

Sebastian S. Bauer; Kim G. Larsen; Axel Legay; Ulrik Nyman; Andrzej Wasowski

doi:10.1016/j.scico.2013.06.003

A modal specification theory for components with data

Sebastian S. Bauer, Kim G. Larsen, Axel Legay, Ulrik Nyman, Andrzej Wasowski

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › peer review

7 Citationer (Scopus)

806 Downloads (Pure)

Abstract

Modal specification is a well-known formalism used as an abstraction theory for tran-
sition systems. Modal specifications are transition systems equipped with two types
of transitions: must-transitions that are mandatory to any implementation, and may-
transitions that are optional. The duality of transitions allows for developing a unique
approach for both logical and structural compositions, and eases the step-wise refine-
ment process for building implementations. We propose Modal Specifications with
Data (MSDs), the first modal specification theory with explicit representation of data.
Our new theory includes the most commonly seen ingredients of a specification the-
ory; that is parallel composition, conjunction and quotient. As MSDs are by nature
potentially infinite-state systems, we propose symbolic representations based on effec-
tive predicates. Our theory serves as a new abstraction-based formalism for transition
systems with data.

Originalsprog	Engelsk
Tidsskrift	Science of Computer Programming
Vol/bind	83
Sider (fra-til)	106–128
Antal sider	22
ISSN	0167-6423
DOI	https://doi.org/10.1016/j.scico.2013.06.003
Status	Udgivet - 1 apr. 2014
Begivenhed	8th International Workshop, FACS 2011 - Oslo, Norge Varighed: 14 nov. 2011 → 16 nov. 2011 Konferencens nummer: 8th

Konference

Konference	8th International Workshop, FACS 2011
Nummer	8th
Land/Område	Norge
By	Oslo
Periode	14/11/2011 → 16/11/2011

Adgang til dokumentet

10.1016/j.scico.2013.06.003

BauerSCP2013Accepteret manuskript, 542 KB

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

Andre filer og links

Link to publication in Scopus

Citationsformater

@article{93c73daa66b44701ab308e9d967daf89,

title = "A modal specification theory for components with data",

abstract = "Modal specification is a well-known formalism used as an abstraction theory for tran-sition systems. Modal specifications are transition systems equipped with two typesof transitions: must-transitions that are mandatory to any implementation, and may-transitions that are optional. The duality of transitions allows for developing a uniqueapproach for both logical and structural compositions, and eases the step-wise refine-ment process for building implementations. We propose Modal Specifications withData (MSDs), the first modal specification theory with explicit representation of data.Our new theory includes the most commonly seen ingredients of a specification the-ory; that is parallel composition, conjunction and quotient. As MSDs are by naturepotentially infinite-state systems, we propose symbolic representations based on effec-tive predicates. Our theory serves as a new abstraction-based formalism for transitionsystems with data.",

keywords = "Modal Transition Systems, Specifications, Interfaces, Data Abstraction, Modal Specifications with Data",

author = "Bauer, {Sebastian S.} and Larsen, {Kim G.} and Axel Legay and Ulrik Nyman and Andrzej Wasowski",

year = "2014",

month = apr,

day = "1",

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

language = "English",

volume = "83",

pages = "106–128",

journal = "Science of Computer Programming",

issn = "0167-6423",

publisher = "Elsevier",

note = "8th International Workshop, FACS 2011 ; Conference date: 14-11-2011 Through 16-11-2011",

}

TY - JOUR

T1 - A modal specification theory for components with data

AU - Bauer, Sebastian S.

AU - Larsen, Kim G.

AU - Legay, Axel

AU - Nyman, Ulrik

AU - Wasowski, Andrzej

N1 - Conference code: 8th

PY - 2014/4/1

Y1 - 2014/4/1

N2 - Modal specification is a well-known formalism used as an abstraction theory for tran-sition systems. Modal specifications are transition systems equipped with two typesof transitions: must-transitions that are mandatory to any implementation, and may-transitions that are optional. The duality of transitions allows for developing a uniqueapproach for both logical and structural compositions, and eases the step-wise refine-ment process for building implementations. We propose Modal Specifications withData (MSDs), the first modal specification theory with explicit representation of data.Our new theory includes the most commonly seen ingredients of a specification the-ory; that is parallel composition, conjunction and quotient. As MSDs are by naturepotentially infinite-state systems, we propose symbolic representations based on effec-tive predicates. Our theory serves as a new abstraction-based formalism for transitionsystems with data.

AB - Modal specification is a well-known formalism used as an abstraction theory for tran-sition systems. Modal specifications are transition systems equipped with two typesof transitions: must-transitions that are mandatory to any implementation, and may-transitions that are optional. The duality of transitions allows for developing a uniqueapproach for both logical and structural compositions, and eases the step-wise refine-ment process for building implementations. We propose Modal Specifications withData (MSDs), the first modal specification theory with explicit representation of data.Our new theory includes the most commonly seen ingredients of a specification the-ory; that is parallel composition, conjunction and quotient. As MSDs are by naturepotentially infinite-state systems, we propose symbolic representations based on effec-tive predicates. Our theory serves as a new abstraction-based formalism for transitionsystems with data.

KW - Modal Transition Systems, Specifications, Interfaces, Data Abstraction, Modal Specifications with Data

UR - http://www.scopus.com/inward/record.url?scp=84879580186&partnerID=8YFLogxK

U2 - 10.1016/j.scico.2013.06.003

DO - 10.1016/j.scico.2013.06.003

M3 - Journal article

AN - SCOPUS:84894584009

SN - 0167-6423

VL - 83

SP - 106

EP - 128

JO - Science of Computer Programming

JF - Science of Computer Programming

T2 - 8th International Workshop, FACS 2011

Y2 - 14 November 2011 through 16 November 2011

ER -

A modal specification theory for components with data

Abstract

Konference

Adgang til dokumentet

AUB Link

Andre filer og links

Fingeraftryk

Citationsformater