Scipediacontent: Scipediacontent moved page Draft Content 645192136 to Encrenaz Braunstein 2006a

2021-02-03T17:07:00Z

Scipediacontent moved page Draft Content 645192136 to Encrenaz Braunstein 2006a

Scipediacontent: Created page with " == Abstract == International audience; This work studies the relations between pipeline architectures and their specification expressed in CTL. We propose a method to build..."

2021-02-03T17:06:57Z

Created page with " == Abstract == International audience; This work studies the relations between pipeline architectures and their specification expressed in CTL. We propose a method to build..."

New page

== Abstract ==

International audience; This work studies the relations between pipeline architectures and their specification expressed in CTL. We propose a method to build pipeline structures incrementally from a simple one (already verified) to a more complex one. Moreover, we show how each increment can be integrated in a CTL specification. We define increments to model treatment delay and treatment abortion of a pipeline flow, and we formalize the composition of the different increments. In order to represent the increments added to an architecture, we derive a set of CTL formulae transformations. Finally we model a control flow of a protocol converter by composition of these increments. We show how CTL properties of the complex architecture are built by applying automatic transformations on the set of CTL properties of the simplest architecture.

== Original document ==

The different versions of the original document can be found in:

* [https://hal.archives-ouvertes.fr/hal-01338249 https://hal.archives-ouvertes.fr/hal-01338249]

* [http://xplorestaging.ieee.org/ielx5/10855/34196/01630757.pdf?arnumber=1630757 http://xplorestaging.ieee.org/ielx5/10855/34196/01630757.pdf?arnumber=1630757],
: [http://dx.doi.org/10.1109/rsp.2006.19 http://dx.doi.org/10.1109/rsp.2006.19]

* [https://dblp.uni-trier.de/db/conf/rsp/rsp2006.html#BraunsteinE06 https://dblp.uni-trier.de/db/conf/rsp/rsp2006.html#BraunsteinE06],
: [http://yadda.icm.edu.pl/yadda/element/bwmeta1.element.ieee-000001630757 http://yadda.icm.edu.pl/yadda/element/bwmeta1.element.ieee-000001630757],
: [https://ieeexplore.ieee.org/document/1630757 https://ieeexplore.ieee.org/document/1630757],
: [http://ieeexplore.ieee.org/document/1630757 http://ieeexplore.ieee.org/document/1630757],
: [https://doi.org/10.1109/RSP.2006.19 https://doi.org/10.1109/RSP.2006.19],
: [http://doi.org/10.1109/RSP.2006.19 http://doi.org/10.1109/RSP.2006.19],
: [https://hal.archives-ouvertes.fr/hal-01338249 https://hal.archives-ouvertes.fr/hal-01338249],
: [http://www-asim.lip6.fr/~ema/pub/braunstein_encrenaz_rsp06.pdf http://www-asim.lip6.fr/~ema/pub/braunstein_encrenaz_rsp06.pdf],
: [https://academic.microsoft.com/#/detail/2138453630 https://academic.microsoft.com/#/detail/2138453630]

← Older revision	Revision as of 17:07, 3 February 2021
(No difference)

Encrenaz Braunstein 2006a - Revision history

Scipediacontent: Scipediacontent moved page Draft Content 645192136 to Encrenaz Braunstein 2006a

Scipediacontent: Created page with " == Abstract == International audience; This work studies the relations between pipeline architectures and their specification expressed in CTL. We propose a method to build..."