Serveur d'exploration Fieldbus

Attention, ce site est en cours de développement !
Attention, site généré par des moyens informatiques à partir de corpus bruts.
Les informations ne sont donc pas validées.

Formal specification and validation of a vital communication protocol

Identifieur interne : 000374 ( Main/Exploration ); précédent : 000373; suivant : 000375

Formal specification and validation of a vital communication protocol

Auteurs : A. Cimatti [Italie] ; P. L. Pieraccini [Italie] ; R. Sebastiani [Italie] ; P. Traverso [Italie] ; A. Villafiorita [Italie]

Source :

RBID : ISTEX:1F7A26633BF3F72800F22F0E21FD4CE17D5579E0

Abstract

Abstract: Formal methods have a great potential of application as powerful specification and early debugging methods in the development of industrial systems. In certain application fields, formal methods are even becoming part of standards. However, the application of formal methods in the development of industrial products is by no means trivial. Indeed, formal methods can be costly, slow down the process of development, and require changes on the development cycle, and training. This paper describes a project developed by Ansaldo Segnalamento Ferroviario with the collaboration of IRST. Formal methods have been successfully applied to the development of an industrial communication protocol for distributed, safety critical systems. The project used a formal language to specify the protocol, and model checking techniques to validate the model.


Url:
DOI: 10.1007/3-540-48118-4_34


Affiliations:


Links toward previous steps (curation, corpus...)


Le document en format XML

<record>
<TEI wicri:istexFullTextTei="biblStruct">
<teiHeader>
<fileDesc>
<titleStmt>
<title xml:lang="en">Formal specification and validation of a vital communication protocol</title>
<author>
<name sortKey="Cimatti, A" sort="Cimatti, A" uniqKey="Cimatti A" first="A." last="Cimatti">A. Cimatti</name>
</author>
<author>
<name sortKey="Pieraccini, P L" sort="Pieraccini, P L" uniqKey="Pieraccini P" first="P. L." last="Pieraccini">P. L. Pieraccini</name>
</author>
<author>
<name sortKey="Sebastiani, R" sort="Sebastiani, R" uniqKey="Sebastiani R" first="R." last="Sebastiani">R. Sebastiani</name>
</author>
<author>
<name sortKey="Traverso, P" sort="Traverso, P" uniqKey="Traverso P" first="P." last="Traverso">P. Traverso</name>
</author>
<author>
<name sortKey="Villafiorita, A" sort="Villafiorita, A" uniqKey="Villafiorita A" first="A." last="Villafiorita">A. Villafiorita</name>
</author>
</titleStmt>
<publicationStmt>
<idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:1F7A26633BF3F72800F22F0E21FD4CE17D5579E0</idno>
<date when="1999" year="1999">1999</date>
<idno type="doi">10.1007/3-540-48118-4_34</idno>
<idno type="url">https://api.istex.fr/document/1F7A26633BF3F72800F22F0E21FD4CE17D5579E0/fulltext/pdf</idno>
<idno type="wicri:Area/Main/Corpus">000106</idno>
<idno type="wicri:explorRef" wicri:stream="Main" wicri:step="Corpus" wicri:corpus="ISTEX">000106</idno>
<idno type="wicri:Area/Main/Curation">000106</idno>
<idno type="wicri:Area/Main/Exploration">000374</idno>
<idno type="wicri:explorRef" wicri:stream="Main" wicri:step="Exploration">000374</idno>
</publicationStmt>
<sourceDesc>
<biblStruct>
<analytic>
<title level="a" type="main" xml:lang="en">Formal specification and validation of a vital communication protocol</title>
<author>
<name sortKey="Cimatti, A" sort="Cimatti, A" uniqKey="Cimatti A" first="A." last="Cimatti">A. Cimatti</name>
<affiliation wicri:level="1">
<country xml:lang="fr">Italie</country>
<wicri:regionArea>ITC-IRST, Via Sommarive 18, 38055, Trento, Povo</wicri:regionArea>
<wicri:noRegion>Povo</wicri:noRegion>
</affiliation>
<affiliation wicri:level="1">
<country wicri:rule="url">Italie</country>
</affiliation>
</author>
<author>
<name sortKey="Pieraccini, P L" sort="Pieraccini, P L" uniqKey="Pieraccini P" first="P. L." last="Pieraccini">P. L. Pieraccini</name>
<affiliation wicri:level="1">
<country xml:lang="fr">Italie</country>
<wicri:regionArea>Ansaldo Segnalamento Ferroviario, Via dei Pescatori 35, Genova</wicri:regionArea>
<wicri:noRegion>Genova</wicri:noRegion>
</affiliation>
<affiliation wicri:level="1">
<country wicri:rule="url">Italie</country>
</affiliation>
</author>
<author>
<name sortKey="Sebastiani, R" sort="Sebastiani, R" uniqKey="Sebastiani R" first="R." last="Sebastiani">R. Sebastiani</name>
<affiliation wicri:level="1">
<country xml:lang="fr">Italie</country>
<wicri:regionArea>ITC-IRST, Via Sommarive 18, 38055, Trento, Povo</wicri:regionArea>
<wicri:noRegion>Povo</wicri:noRegion>
</affiliation>
<affiliation wicri:level="1">
<country wicri:rule="url">Italie</country>
</affiliation>
</author>
<author>
<name sortKey="Traverso, P" sort="Traverso, P" uniqKey="Traverso P" first="P." last="Traverso">P. Traverso</name>
<affiliation wicri:level="1">
<country xml:lang="fr">Italie</country>
<wicri:regionArea>ITC-IRST, Via Sommarive 18, 38055, Trento, Povo</wicri:regionArea>
<wicri:noRegion>Povo</wicri:noRegion>
</affiliation>
<affiliation wicri:level="1">
<country wicri:rule="url">Italie</country>
</affiliation>
</author>
<author>
<name sortKey="Villafiorita, A" sort="Villafiorita, A" uniqKey="Villafiorita A" first="A." last="Villafiorita">A. Villafiorita</name>
<affiliation wicri:level="1">
<country xml:lang="fr">Italie</country>
<wicri:regionArea>ITC-IRST, Via Sommarive 18, 38055, Trento, Povo</wicri:regionArea>
<wicri:noRegion>Povo</wicri:noRegion>
</affiliation>
<affiliation wicri:level="1">
<country wicri:rule="url">Italie</country>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series>
<title level="s">Lecture Notes in Computer Science</title>
<imprint>
<date>1999</date>
</imprint>
<idno type="ISSN">0302-9743</idno>
<idno type="ISSN">0302-9743</idno>
</series>
<idno type="istex">1F7A26633BF3F72800F22F0E21FD4CE17D5579E0</idno>
<idno type="DOI">10.1007/3-540-48118-4_34</idno>
<idno type="ChapterID">Chap34</idno>
<idno type="ChapterID">34</idno>
</biblStruct>
</sourceDesc>
<seriesStmt>
<idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc>
<textClass></textClass>
<langUsage>
<language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front>
<div type="abstract" xml:lang="en">Abstract: Formal methods have a great potential of application as powerful specification and early debugging methods in the development of industrial systems. In certain application fields, formal methods are even becoming part of standards. However, the application of formal methods in the development of industrial products is by no means trivial. Indeed, formal methods can be costly, slow down the process of development, and require changes on the development cycle, and training. This paper describes a project developed by Ansaldo Segnalamento Ferroviario with the collaboration of IRST. Formal methods have been successfully applied to the development of an industrial communication protocol for distributed, safety critical systems. The project used a formal language to specify the protocol, and model checking techniques to validate the model.</div>
</front>
</TEI>
<affiliations>
<list>
<country>
<li>Italie</li>
</country>
</list>
<tree>
<country name="Italie">
<noRegion>
<name sortKey="Cimatti, A" sort="Cimatti, A" uniqKey="Cimatti A" first="A." last="Cimatti">A. Cimatti</name>
</noRegion>
<name sortKey="Cimatti, A" sort="Cimatti, A" uniqKey="Cimatti A" first="A." last="Cimatti">A. Cimatti</name>
<name sortKey="Pieraccini, P L" sort="Pieraccini, P L" uniqKey="Pieraccini P" first="P. L." last="Pieraccini">P. L. Pieraccini</name>
<name sortKey="Pieraccini, P L" sort="Pieraccini, P L" uniqKey="Pieraccini P" first="P. L." last="Pieraccini">P. L. Pieraccini</name>
<name sortKey="Sebastiani, R" sort="Sebastiani, R" uniqKey="Sebastiani R" first="R." last="Sebastiani">R. Sebastiani</name>
<name sortKey="Sebastiani, R" sort="Sebastiani, R" uniqKey="Sebastiani R" first="R." last="Sebastiani">R. Sebastiani</name>
<name sortKey="Traverso, P" sort="Traverso, P" uniqKey="Traverso P" first="P." last="Traverso">P. Traverso</name>
<name sortKey="Traverso, P" sort="Traverso, P" uniqKey="Traverso P" first="P." last="Traverso">P. Traverso</name>
<name sortKey="Villafiorita, A" sort="Villafiorita, A" uniqKey="Villafiorita A" first="A." last="Villafiorita">A. Villafiorita</name>
<name sortKey="Villafiorita, A" sort="Villafiorita, A" uniqKey="Villafiorita A" first="A." last="Villafiorita">A. Villafiorita</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Informatique/corpus/FieldbusV1/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000374 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Informatique
   |area=    FieldbusV1
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     ISTEX:1F7A26633BF3F72800F22F0E21FD4CE17D5579E0
   |texte=   Formal specification and validation of a vital communication protocol
}}

Wicri

This area was generated with Dilib version V0.6.29.
Data generation: Thu May 25 22:29:54 2017. Site generation: Wed Jul 19 17:31:17 2017