Logical vs. behavioural specifications

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F20%3A00117715" target="_blank" >RIV/00216224:14330/20:00117715 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1016/j.ic.2019.104487" target="_blank" >http://dx.doi.org/10.1016/j.ic.2019.104487</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1016/j.ic.2019.104487" target="_blank" >10.1016/j.ic.2019.104487</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Logical vs. behavioural specifications

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Logical vs. behavioural specifications

Popis výsledku anglicky

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.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2020

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Information and computation

ISSN

0890-5401

e-ISSN

—

Svazek periodika

271

Číslo periodika v rámci svazku

104487

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

24

Strana od-do

1-24

Kód UT WoS článku

000519527800006

EID výsledku v databázi Scopus

2-s2.0-85075905322