Real-time specifications

Alexandre David; Kim Guldstrand Larsen; Axel Legay; Ulrik Mathias Nyman; Louis-Marie Traonouez; Andrzej Wasowski

doi:10.1007/s10009-013-0286-x

Real-time specifications

Alexandre David, Kim Guldstrand Larsen, Axel Legay, Ulrik Mathias Nyman, Louis-Marie Traonouez, Andrzej Wasowski

Publikation: Artikel i tidsskrift og konference artikel i tidsskrift › Tidsskriftartikel › Forskning › peer review

Abstract

A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation, and a set of operators supporting stepwise design. We develop a specification framework for real-time systems using Timed I/O Automata as the specification formalism, with the semantics expressed in terms of Timed I/O Transition Systems. We provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications—all indispensable ingredients of a compositional design methodology. The theory is implemented in the new tool ECDAR. We present symbolic versions of the algorithms used in ECDAR, and demonstrate the use of the tool using a small case study in compositional verification.

Originalsprog	Engelsk
Tidsskrift	International Journal on Software Tools for Technology Transfer
Sider (fra-til)	1-29
Antal sider	29
ISSN	1433-2779
DOI	https://doi.org/10.1007/s10009-013-0286-x
Status	Udgivet - aug. 2013

Emneord

Real-time systems
Stepwise-refinement
Compositional verification
Timed I/O automata

Adgang til dokumentet

10.1007/s10009-013-0286-x

MT-Lab - Modelling of Information Technology
Wasowski, A. (CoI), Godskesen, J. C. (PI), Song, L. (CoI), Traonouez, L.-M. (CoI) & Biondi, F. (CoI)
01/11/2008 → 31/10/2013
Projekter: Projekt › Forskning

Citationsformater

@article{9dbc9f50f9094563ae5442668ffa599b,

title = "Real-time specifications",

abstract = "A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation, and a set of operators supporting stepwise design. We develop a specification framework for real-time systems using Timed I/O Automata as the specification formalism, with the semantics expressed in terms of Timed I/O Transition Systems. We provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications—all indispensable ingredients of a compositional design methodology. The theory is implemented in the new tool ECDAR. We present symbolic versions of the algorithms used in ECDAR, and demonstrate the use of the tool using a small case study in compositional verification.",

keywords = "Real-time systems, Stepwise-refinement, Compositional verification, Timed I/O automata, Real-time systems, Stepwise-refinement, Compositional verification, Timed I/O automata",

author = "Alexandre David and Larsen, {Kim Guldstrand} and Axel Legay and Nyman, {Ulrik Mathias} and Louis-Marie Traonouez and Andrzej Wasowski",

note = "Cannot be verified as published, date: 21.01.2014 haal",

year = "2013",

month = aug,

doi = "10.1007/s10009-013-0286-x",

language = "English",

pages = "1--29",

journal = "International Journal on Software Tools for Technology Transfer",

issn = "1433-2779",

publisher = "Springer",

}

TY - JOUR

T1 - Real-time specifications

AU - David, Alexandre

AU - Larsen, Kim Guldstrand

AU - Legay, Axel

AU - Nyman, Ulrik Mathias

AU - Traonouez, Louis-Marie

AU - Wasowski, Andrzej

N1 - Cannot be verified as published, date: 21.01.2014 haal

PY - 2013/8

Y1 - 2013/8

N2 - A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation, and a set of operators supporting stepwise design. We develop a specification framework for real-time systems using Timed I/O Automata as the specification formalism, with the semantics expressed in terms of Timed I/O Transition Systems. We provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications—all indispensable ingredients of a compositional design methodology. The theory is implemented in the new tool ECDAR. We present symbolic versions of the algorithms used in ECDAR, and demonstrate the use of the tool using a small case study in compositional verification.

AB - A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation, and a set of operators supporting stepwise design. We develop a specification framework for real-time systems using Timed I/O Automata as the specification formalism, with the semantics expressed in terms of Timed I/O Transition Systems. We provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications—all indispensable ingredients of a compositional design methodology. The theory is implemented in the new tool ECDAR. We present symbolic versions of the algorithms used in ECDAR, and demonstrate the use of the tool using a small case study in compositional verification.

KW - Real-time systems

KW - Stepwise-refinement

KW - Compositional verification

KW - Timed I/O automata

KW - Real-time systems

KW - Stepwise-refinement

KW - Compositional verification

KW - Timed I/O automata

U2 - 10.1007/s10009-013-0286-x

DO - 10.1007/s10009-013-0286-x

M3 - Journal article

SN - 1433-2779

SP - 1

EP - 29

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

ER -

Real-time specifications

Abstract

Emneord

Adgang til dokumentet

Fingeraftryk

Projekter

MT-Lab - Modelling of Information Technology

Citationsformater