Formal method for timed tests sequences generation
Identifieur interne : 000805 ( PascalFrancis/Checkpoint ); précédent : 000804; suivant : 000806Formal method for timed tests sequences generation
Auteurs : Franaoise Simonot-Lion [France] ; Laurent Kaiser [France] ; Ricardo Santos Marques [France]Source :
- Journal européen des systèmes automatisés [ 1269-6935 ] ; 2002.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
This paper deals with the temporal interoperability of components in a real time application and presents a method in order to verify it. The temporal interoperability expresses the capability of a component to cooperate and exchange information with its environment while respecting specked timing properties. The principal aim of this paper is to propose a construction method of an adaptative tester. The tester generation process is based on the TIOSM formalism. The logical behaviour of this tester is statically defined (sequence of events, identification of the different clocks). The evaluation of the transition firing times is done on line by the tester itself during the test process. For this, a set of linear inequalities is generated and attached to each state of the tester and a solver is integrated to it.
Affiliations:
Links toward previous steps (curation, corpus...)
Links to Exploration step
Pascal:03-0116368Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Formal method for timed tests sequences generation</title><author><name sortKey="Simonot Lion, Franaoise" sort="Simonot Lion, Franaoise" uniqKey="Simonot Lion F" first="Franaoise" last="Simonot-Lion">Franaoise Simonot-Lion</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA, UMR 7503 Campus Scientifique BP 239</s1><s2>54506 Vandoeuvre les Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ><sZ>3 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation></author><author><name sortKey="Kaiser, Laurent" sort="Kaiser, Laurent" uniqKey="Kaiser L" first="Laurent" last="Kaiser">Laurent Kaiser</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA, UMR 7503 Campus Scientifique BP 239</s1><s2>54506 Vandoeuvre les Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ><sZ>3 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation></author><author><name sortKey="Santos Marques, Ricardo" sort="Santos Marques, Ricardo" uniqKey="Santos Marques R" first="Ricardo" last="Santos Marques">Ricardo Santos Marques</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA, UMR 7503 Campus Scientifique BP 239</s1><s2>54506 Vandoeuvre les Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ><sZ>3 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">03-0116368</idno><date when="2002">2002</date><idno type="stanalyst">PASCAL 03-0116368 CRAN</idno><idno type="RBID">Pascal:03-0116368</idno><idno type="wicri:Area/PascalFrancis/Corpus">000825</idno><idno type="wicri:Area/PascalFrancis/Curation">000218</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000805</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000805</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Formal method for timed tests sequences generation</title><author><name sortKey="Simonot Lion, Franaoise" sort="Simonot Lion, Franaoise" uniqKey="Simonot Lion F" first="Franaoise" last="Simonot-Lion">Franaoise Simonot-Lion</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA, UMR 7503 Campus Scientifique BP 239</s1><s2>54506 Vandoeuvre les Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ><sZ>3 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation></author><author><name sortKey="Kaiser, Laurent" sort="Kaiser, Laurent" uniqKey="Kaiser L" first="Laurent" last="Kaiser">Laurent Kaiser</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA, UMR 7503 Campus Scientifique BP 239</s1><s2>54506 Vandoeuvre les Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ><sZ>3 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation></author><author><name sortKey="Santos Marques, Ricardo" sort="Santos Marques, Ricardo" uniqKey="Santos Marques R" first="Ricardo" last="Santos Marques">Ricardo Santos Marques</name><affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA, UMR 7503 Campus Scientifique BP 239</s1><s2>54506 Vandoeuvre les Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ><sZ>3 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation></author></analytic><series><title level="j" type="main">Journal européen des systèmes automatisés</title><title level="j" type="abbreviated">J. eur. syst. autom.</title><idno type="ISSN">1269-6935</idno><imprint><date when="2002">2002</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Journal européen des systèmes automatisés</title><title level="j" type="abbreviated">J. eur. syst. autom.</title><idno type="ISSN">1269-6935</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Information exchange</term><term>Real time</term><term>Test method</term><term>Timing</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Temps réel</term><term>Echange information</term><term>Timing</term><term>Méthode essai</term><term>vérification à la volée</term><term>test de conformité</term><term>automates temporisés</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">This paper deals with the temporal interoperability of components in a real time application and presents a method in order to verify it. The temporal interoperability expresses the capability of a component to cooperate and exchange information with its environment while respecting specked timing properties. The principal aim of this paper is to propose a construction method of an adaptative tester. The tester generation process is based on the TIOSM formalism. The logical behaviour of this tester is statically defined (sequence of events, identification of the different clocks). The evaluation of the transition firing times is done on line by the tester itself during the test process. For this, a set of linear inequalities is generated and attached to each state of the tester and a solver is integrated to it.</div></front></TEI><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>1269-6935</s0></fA01><fA03 i2="1"><s0>J. eur. syst. autom.</s0></fA03><fA05><s2>36</s2></fA05><fA06><s2>7</s2></fA06><fA08 i1="01" i2="1" l="ENG"><s1>Formal method for timed tests sequences generation</s1></fA08><fA09 i1="01" i2="1" l="ENG"><s1>Modelling of Reactive Systems</s1></fA09><fA11 i1="01" i2="1"><s1>SIMONOT-LION (Franaoise)</s1></fA11><fA11 i1="02" i2="1"><s1>KAISER (Laurent)</s1></fA11><fA11 i1="03" i2="1"><s1>SANTOS MARQUES (Ricardo)</s1></fA11><fA12 i1="01" i2="1"><s1>JUANOLE (Guy)</s1><s9>ed.</s9></fA12><fA12 i1="02" i2="1"><s1>VALETTE (Robert)</s1><s9>ed.</s9></fA12><fA12 i1="03" i2="1"><s1>VERNADAT (François)</s1><s9>ed.</s9></fA12><fA14 i1="01"><s1>LORIA, UMR 7503 Campus Scientifique BP 239</s1><s2>54506 Vandoeuvre les Nancy</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ><sZ>3 aut.</sZ></fA14><fA15 i1="01"><s1>LAAS-CNRS</s1><s2>Toulouse</s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ><sZ>3 aut.</sZ></fA15><fA15 i1="02"><s1>Université Paul Sabatier</s1><s2>Toulouse</s2><s3>FRA</s3><sZ>1 aut.</sZ></fA15><fA15 i1="03"><s1>INSA</s1><s2>Toulouse</s2><s3>FRA</s3><sZ>3 aut.</sZ></fA15><fA20><s1>1001-1013</s1></fA20><fA21><s1>2002</s1></fA21><fA23 i1="01"><s0>ENG</s0></fA23><fA24 i1="01"><s0>fre</s0></fA24><fA43 i1="01"><s1>INIST</s1><s2>26104</s2></fA43><fA44><s0>A300</s0></fA44><fA45><s0>12 ref.</s0></fA45><fA47 i1="01" i2="1"><s0>03-0116368</s0></fA47><fA60><s1>P</s1><s2>C</s2></fA60><fA61><s0>A</s0></fA61><fA64 i1="01" i2="1"><s0>Journal européen des systèmes automatisés</s0></fA64><fA66 i1="01"><s0>FRA</s0></fA66><fC01 i1="01" l="ENG"><s0>This paper deals with the temporal interoperability of components in a real time application and presents a method in order to verify it. The temporal interoperability expresses the capability of a component to cooperate and exchange information with its environment while respecting specked timing properties. The principal aim of this paper is to propose a construction method of an adaptative tester. The tester generation process is based on the TIOSM formalism. The logical behaviour of this tester is statically defined (sequence of events, identification of the different clocks). The evaluation of the transition firing times is done on line by the tester itself during the test process. For this, a set of linear inequalities is generated and attached to each state of the tester and a solver is integrated to it.</s0></fC01><fC02 i1="01" i2="X"><s0>001D02D10</s0></fC02><fC02 i1="02" i2="X"><s0>001D02D13</s0></fC02><fC03 i1="01" i2="X" l="FRE"><s0>Temps réel</s0><s5>01</s5></fC03><fC03 i1="01" i2="X" l="ENG"><s0>Real time</s0><s5>01</s5></fC03><fC03 i1="01" i2="X" l="SPA"><s0>Tiempo real</s0><s5>01</s5></fC03><fC03 i1="02" i2="X" l="FRE"><s0>Echange information</s0><s5>11</s5></fC03><fC03 i1="02" i2="X" l="ENG"><s0>Information exchange</s0><s5>11</s5></fC03><fC03 i1="02" i2="X" l="SPA"><s0>Intercambio información</s0><s5>11</s5></fC03><fC03 i1="03" i2="X" l="FRE"><s0>Timing</s0><s5>12</s5></fC03><fC03 i1="03" i2="X" l="ENG"><s0>Timing</s0><s5>12</s5></fC03><fC03 i1="03" i2="X" l="SPA"><s0>Timing</s0><s5>12</s5></fC03><fC03 i1="04" i2="X" l="FRE"><s0>Méthode essai</s0><s5>15</s5></fC03><fC03 i1="04" i2="X" l="ENG"><s0>Test method</s0><s5>15</s5></fC03><fC03 i1="04" i2="X" l="SPA"><s0>Método ensayo</s0><s5>15</s5></fC03><fC03 i1="05" i2="X" l="FRE"><s0>vérification à la volée</s0><s4>INC</s4><s5>82</s5></fC03><fC03 i1="06" i2="X" l="FRE"><s0>test de conformité</s0><s4>INC</s4><s5>83</s5></fC03><fC03 i1="07" i2="X" l="FRE"><s0>automates temporisés</s0><s4>INC</s4><s5>84</s5></fC03><fN21><s1>069</s1></fN21><fN82><s1>PSI</s1></fN82></pA><pR><fA30 i1="01" i2="1" l="ENG"><s1>MSR'2001: Reactive Systems Modeling. Conference</s1><s2>3</s2><s3>Toulouse FRA</s3><s4>2001-10</s4></fA30></pR></standard></inist><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Vandœuvre-lès-Nancy</li></settlement></list><tree><country name="France"><region name="Grand Est"><name sortKey="Simonot Lion, Franaoise" sort="Simonot Lion, Franaoise" uniqKey="Simonot Lion F" first="Franaoise" last="Simonot-Lion">Franaoise Simonot-Lion</name></region><name sortKey="Kaiser, Laurent" sort="Kaiser, Laurent" uniqKey="Kaiser L" first="Laurent" last="Kaiser">Laurent Kaiser</name><name sortKey="Santos Marques, Ricardo" sort="Santos Marques, Ricardo" uniqKey="Santos Marques R" first="Ricardo" last="Santos Marques">Ricardo Santos Marques</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000805 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Checkpoint/biblio.hfd -nk 000805 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= PascalFrancis
|étape= Checkpoint
|type= RBID
|clé= Pascal:03-0116368
|texte= Formal method for timed tests sequences generation
}}
| This area was generated with Dilib version V0.6.33. |  |