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. |
Další formáty:
BibTeX
LaTeX
RIS
@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.
|