Logical vs. behavioural specifications

J 2020

Logical vs. behavioural specifications

BENEŠ, Nikola, Uli FAHRENBERG, Jan KŘETÍNSKÝ, Axel LEGAY, Louis-Marie TRAONOUEZ et. al.

Základní údaje

Originální název

Logical vs. behavioural specifications

Autoři

BENEŠ, Nikola (203 Česká republika, domácí), Uli FAHRENBERG, Jan KŘETÍNSKÝ (203 Česká republika), Axel LEGAY a Louis-Marie TRAONOUEZ

Vydání

Information and computation, San Diego, Academic Press Inc Elsevier Science, 2020, 0890-5401

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

není předmětem státního či obchodního tajemství

Odkazy

URL

Impakt faktor

Impact factor: 0.704

Kód RIV

RIV/00216224:14330/20:00117715

Organizační jednotka

Fakulta informatiky

DOI

http://dx.doi.org/10.1016/j.ic.2019.104487

UT WoS

000519527800006

Klíčová slova anglicky

Component-based design; Refinement; Logic; Modal transition system; Specification

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 14. 5. 2021 05:46, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

There are two fundamentally different approaches for specifying and verifying properties of systems. The logical approach makes use of specifications given as formulae of temporal or modal logics and relies on efficient model checking algorithms; the behavioural approach exploits various equivalence or refinement checking methods, provided the specifications are given in the same formalism as implementations. In this paper we provide translations between the logical formalism of nu-calculus and the behavioural formalism of disjunctive modal transition systems. The translations preserve structural properties of the input specification and allow us to perform logical operations on the behavioural specifications as well as behavioural compositions on logical formulae. The unification of both approaches provides additional methods for component-based stepwise design.

Citovat

BENEŠ, Nikola, Uli FAHRENBERG, Jan KŘETÍNSKÝ, Axel LEGAY a Louis-Marie TRAONOUEZ. Logical vs. behavioural specifications. Information and computation. San Diego: Academic Press Inc Elsevier Science, 2020, roč. 271, č. 104487, s. 1-24. ISSN 0890-5401. Dostupné z: https://dx.doi.org/10.1016/j.ic.2019.104487.

@article{1726536,
   author = {Beneš, Nikola and Fahrenberg, Uli and Křetínský, Jan and Legay, Axel and Traonouez, LouisandMarie},
   article_location = {San Diego},
   article_number = {104487},
   doi = {http://dx.doi.org/10.1016/j.ic.2019.104487},
   keywords = {Component-based design; Refinement; Logic; Modal transition system; Specification},
   language = {eng},
   issn = {0890-5401},
   journal = {Information and computation},
   title = {Logical vs. behavioural specifications},
   url = {http://dx.doi.org/10.1016/j.ic.2019.104487},
   volume = {271},
   year = {2020}
}

TY  - JOUR
ID  - 1726536
AU  - Beneš, Nikola - Fahrenberg, Uli - Křetínský, Jan - Legay, Axel - Traonouez, Louis-Marie
PY  - 2020
TI  - Logical vs. behavioural specifications
JF  - Information and computation
VL  - 271
IS  - 104487
SP  - 1-24
EP  - 1-24
PB  - Academic Press Inc Elsevier Science
SN  - 08905401
KW  - Component-based design
KW  - Refinement
KW  - Logic
KW  - Modal transition system
KW  - Specification
UR  - http://dx.doi.org/10.1016/j.ic.2019.104487
N2  - There are two fundamentally different approaches for specifying and verifying properties of systems. The logical approach makes use of specifications given as formulae of temporal or modal logics and relies on efficient model checking algorithms; the behavioural approach exploits various equivalence or refinement checking methods, provided the specifications are given in the same formalism as implementations. In this paper we provide translations between the logical formalism of nu-calculus and the behavioural formalism of disjunctive modal transition systems. The translations preserve structural properties of the input specification and allow us to perform logical operations on the behavioural specifications as well as behavioural compositions on logical formulae. The unification of both approaches provides additional methods for component-based stepwise design.
ER  -

BENEŠ, Nikola, Uli FAHRENBERG, Jan KŘETÍNSKÝ, Axel LEGAY a Louis-Marie TRAONOUEZ. Logical vs. behavioural specifications. \textit{Information and computation}. San Diego: Academic Press Inc Elsevier Science, 2020, roč.~271, č.~104487, s.~1-24. ISSN~0890-5401. Dostupné z: https://dx.doi.org/10.1016/j.ic.2019.104487.

Podrobný výpis o publikaci