Specification and refinement of mobile systems in MTLA and mobile UML
Identifieur interne :
000461 ( PascalFrancis/Corpus );
précédent :
000460;
suivant :
000462
Specification and refinement of mobile systems in MTLA and mobile UML
Auteurs : Alexander Knapp ;
Stephan Merz ;
Martin Wirsing ;
Julia ZappeSource :
-
Theoretical computer science [ 0304-3975 ] ; 2006.
RBID : Pascal:06-0160706
Descripteurs français
- Pascal (Inist)
- Spécification formelle,
Logique temporelle,
Vérification formelle,
Code,
Sémantique,
Informatique théorique,
Affinement,
Système formel,
Système mobile,
Logique spatiale,
Développement système,
UML.
English descriptors
- KwdEn :
- Code,
Computer theory,
Formal specification,
Formal verification,
Mobile system,
Refinement,
Semantics,
Spatial logic,
System development,
Temporal logic,
UML.
Abstract
We define the spatio-temporal logic MTLA as an extension of Lamport's Temporal Logic of Actions TLA for the specification, verification, and formal development of systems that rely on mobile code. The formalism is validated by an encoding of models written in the mobile UML notation. We identify refinement principles for mobile systems and justify refinements of mobile UML state machines with the help of the MTLA semantics.
Notice en format standard (ISO 2709)
Pour connaître la documentation sur le format Inist Standard.
| pA |
| A01 | 01 | 1 | | @0 0304-3975 |
|---|
| A02 | 01 | | | @0 TCSCDI |
|---|
| A03 | | 1 | | @0 Theor. comput. sci. |
|---|
| A05 | | | | @2 351 |
|---|
| A06 | | | | @2 2 |
|---|
| A08 | 01 | 1 | ENG | @1 Specification and refinement of mobile systems in MTLA and mobile UML |
|---|
| A09 | 01 | 1 | ENG | @1 Algebraic methodology and software technology |
|---|
| A11 | 01 | 1 | | @1 KNAPP (Alexander) |
|---|
| A11 | 02 | 1 | | @1 MERZ (Stephan) |
|---|
| A11 | 03 | 1 | | @1 WIRSING (Martin) |
|---|
| A11 | 04 | 1 | | @1 ZAPPE (Julia) |
|---|
| A12 | 01 | 1 | | @1 MAHARAJ (Savi) @9 ed. |
|---|
| A12 | 02 | 1 | | @1 SHANKLAND (Carron) @9 ed. |
|---|
| A12 | 03 | 1 | | @1 RATTRAY (Charles) @9 ed. |
|---|
| A14 | 01 | | | @1 Institut für Informatik, Ludwig-Maximilians-Universität @2 Munich @3 DEU @Z 1 aut. @Z 3 aut. @Z 4 aut. |
|---|
| A14 | 02 | | | @1 INRIA Lorraine & LORIA @2 Nancy @3 FRA @Z 2 aut. @Z 4 aut. |
|---|
| A15 | 01 | | | @1 Department of Computing Science and Mathematics, University of Stirling @2 Stirling, FK9 4LA @3 GBR @Z 1 aut. @Z 2 aut. @Z 3 aut. |
|---|
| A20 | | | | @1 184-202 |
|---|
| A21 | | | | @1 2006 |
|---|
| A23 | 01 | | | @0 ENG |
|---|
| A43 | 01 | | | @1 INIST @2 17243 @5 354000133193310040 |
|---|
| A44 | | | | @0 0000 @1 © 2006 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 28 ref. |
|---|
| A47 | 01 | 1 | | @0 06-0160706 |
|---|
| A60 | | | | @1 P @2 C |
|---|
| A61 | | | | @0 A |
|---|
| A64 | 01 | 1 | | @0 Theoretical computer science |
|---|
| A66 | 01 | | | @0 NLD |
|---|
| C01 | 01 | | ENG | @0 We define the spatio-temporal logic MTLA as an extension of Lamport's Temporal Logic of Actions TLA for the specification, verification, and formal development of systems that rely on mobile code. The formalism is validated by an encoding of models written in the mobile UML notation. We identify refinement principles for mobile systems and justify refinements of mobile UML state machines with the help of the MTLA semantics. |
|---|
| C02 | 01 | X | | @0 001A02A01B |
|---|
| C02 | 02 | X | | @0 001D02B09 |
|---|
| C02 | 03 | X | | @0 001D02A05 |
|---|
| C02 | 04 | X | | @0 001D02A02 |
|---|
| C03 | 01 | X | FRE | @0 Spécification formelle @5 17 |
|---|
| C03 | 01 | X | ENG | @0 Formal specification @5 17 |
|---|
| C03 | 01 | X | SPA | @0 Especificación formal @5 17 |
|---|
| C03 | 02 | X | FRE | @0 Logique temporelle @5 18 |
|---|
| C03 | 02 | X | ENG | @0 Temporal logic @5 18 |
|---|
| C03 | 02 | X | SPA | @0 Lógica temporal @5 18 |
|---|
| C03 | 03 | 3 | FRE | @0 Vérification formelle @5 19 |
|---|
| C03 | 03 | 3 | ENG | @0 Formal verification @5 19 |
|---|
| C03 | 04 | X | FRE | @0 Code @5 20 |
|---|
| C03 | 04 | X | ENG | @0 Code @5 20 |
|---|
| C03 | 04 | X | SPA | @0 Código @5 20 |
|---|
| C03 | 05 | X | FRE | @0 Sémantique @5 21 |
|---|
| C03 | 05 | X | ENG | @0 Semantics @5 21 |
|---|
| C03 | 05 | X | SPA | @0 Semántica @5 21 |
|---|
| C03 | 06 | X | FRE | @0 Informatique théorique @5 22 |
|---|
| C03 | 06 | X | ENG | @0 Computer theory @5 22 |
|---|
| C03 | 06 | X | SPA | @0 Informática teórica @5 22 |
|---|
| C03 | 07 | X | FRE | @0 Affinement @5 23 |
|---|
| C03 | 07 | X | ENG | @0 Refinement @5 23 |
|---|
| C03 | 07 | X | SPA | @0 Afinamiento @5 23 |
|---|
| C03 | 08 | X | FRE | @0 Système formel @4 INC @5 72 |
|---|
| C03 | 09 | X | FRE | @0 Système mobile @4 CD @5 96 |
|---|
| C03 | 09 | X | ENG | @0 Mobile system @4 CD @5 96 |
|---|
| C03 | 10 | X | FRE | @0 Logique spatiale @4 CD @5 97 |
|---|
| C03 | 10 | X | ENG | @0 Spatial logic @4 CD @5 97 |
|---|
| C03 | 11 | X | FRE | @0 Développement système @4 CD @5 98 |
|---|
| C03 | 11 | X | ENG | @0 System development @4 CD @5 98 |
|---|
| C03 | 12 | X | FRE | @0 UML @4 CD @5 99 |
|---|
| C03 | 12 | X | ENG | @0 UML @4 CD @5 99 |
|---|
| N21 | | | | @1 100 |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | ENG | @1 International Conference on Algebraic Methodology and Software Technology @2 10 @3 Stirling GBR @4 2004-07-12 |
|---|
|
|---|
Format Inist (serveur)
| NO : | PASCAL 06-0160706 INIST |
|---|
| ET : | Specification and refinement of mobile systems in MTLA and mobile UML |
|---|
| AU : | KNAPP (Alexander); MERZ (Stephan); WIRSING (Martin); ZAPPE (Julia); MAHARAJ (Savi); SHANKLAND (Carron); RATTRAY (Charles) |
|---|
| AF : | Institut für Informatik, Ludwig-Maximilians-Universität/Munic h/Allemagne (1 aut., 3 aut., 4 aut.); INRIA Lorraine & LORIA/Nancy/France (2 aut., 4 aut.); Department of Computing Science and Mathematics, University of Stirling/Stirling, FK9 4LA/Royaume-Uni (1 aut., 2 aut., 3 aut.) |
|---|
| DT : | Publication en série; Congrès; Niveau analytique |
|---|
| SO : | Theoretical computer science; ISSN 0304-3975; Coden TCSCDI; Pays-Bas; Da. 2006; Vol. 351; No. 2; Pp. 184-202; Bibl. 28 ref. |
|---|
| LA : | Anglais |
|---|
| EA : | We define the spatio-temporal logic MTLA as an extension of Lamport's Temporal Logic of Actions TLA for the specification, verification, and formal development of systems that rely on mobile code. The formalism is validated by an encoding of models written in the mobile UML notation. We identify refinement principles for mobile systems and justify refinements of mobile UML state machines with the help of the MTLA semantics. |
|---|
| CC : | 001A02A01B; 001D02B09; 001D02A05; 001D02A02 |
|---|
| FD : | Spécification formelle; Logique temporelle; Vérification formelle; Code; Sémantique; Informatique théorique; Affinement; Système formel; Système mobile; Logique spatiale; Développement système; UML |
|---|
| ED : | Formal specification; Temporal logic; Formal verification; Code; Semantics; Computer theory; Refinement; Mobile system; Spatial logic; System development; UML |
|---|
| SD : | Especificación formal; Lógica temporal; Código; Semántica; Informática teórica; Afinamiento |
|---|
| LO : | INIST-17243.354000133193310040 |
|---|
| ID : | 06-0160706 |
|---|
Links to Exploration step
Pascal:06-0160706
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Specification and refinement of mobile systems in MTLA and mobile UML</title>
<author><name sortKey="Knapp, Alexander" sort="Knapp, Alexander" uniqKey="Knapp A" first="Alexander" last="Knapp">Alexander Knapp</name>
<affiliation><inist:fA14 i1="01"><s1>Institut für Informatik, Ludwig-Maximilians-Universität</s1>
<s2>Munich</s2>
<s3>DEU</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14><author><name sortKey="Merz, Stephan" sort="Merz, Stephan" uniqKey="Merz S" first="Stephan" last="Merz">Stephan Merz</name>
<affiliation><inist:fA14 i1="02"><s1>INRIA Lorraine & LORIA</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14><author><name sortKey="Wirsing, Martin" sort="Wirsing, Martin" uniqKey="Wirsing M" first="Martin" last="Wirsing">Martin Wirsing</name>
<affiliation><inist:fA14 i1="01"><s1>Institut für Informatik, Ludwig-Maximilians-Universität</s1>
<s2>Munich</s2>
<s3>DEU</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14><author><name sortKey="Zappe, Julia" sort="Zappe, Julia" uniqKey="Zappe J" first="Julia" last="Zappe">Julia Zappe</name>
<affiliation><inist:fA14 i1="01"><s1>Institut für Informatik, Ludwig-Maximilians-Universität</s1>
<s2>Munich</s2>
<s3>DEU</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14><affiliation><inist:fA14 i1="02"><s1>INRIA Lorraine & LORIA</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14><publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">06-0160706</idno>
<date when="2006">2006</date>
<idno type="stanalyst">PASCAL 06-0160706 INIST</idno>
<idno type="RBID">Pascal:06-0160706</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000461</idno>
</publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Specification and refinement of mobile systems in MTLA and mobile UML</title>
<author><name sortKey="Knapp, Alexander" sort="Knapp, Alexander" uniqKey="Knapp A" first="Alexander" last="Knapp">Alexander Knapp</name>
<affiliation><inist:fA14 i1="01"><s1>Institut für Informatik, Ludwig-Maximilians-Universität</s1>
<s2>Munich</s2>
<s3>DEU</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14><author><name sortKey="Merz, Stephan" sort="Merz, Stephan" uniqKey="Merz S" first="Stephan" last="Merz">Stephan Merz</name>
<affiliation><inist:fA14 i1="02"><s1>INRIA Lorraine & LORIA</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14><author><name sortKey="Wirsing, Martin" sort="Wirsing, Martin" uniqKey="Wirsing M" first="Martin" last="Wirsing">Martin Wirsing</name>
<affiliation><inist:fA14 i1="01"><s1>Institut für Informatik, Ludwig-Maximilians-Universität</s1>
<s2>Munich</s2>
<s3>DEU</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14><author><name sortKey="Zappe, Julia" sort="Zappe, Julia" uniqKey="Zappe J" first="Julia" last="Zappe">Julia Zappe</name>
<affiliation><inist:fA14 i1="01"><s1>Institut für Informatik, Ludwig-Maximilians-Universität</s1>
<s2>Munich</s2>
<s3>DEU</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14><affiliation><inist:fA14 i1="02"><s1>INRIA Lorraine & LORIA</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
<sZ>4 aut.</sZ>
</inist:fA14><series><title level="j" type="main">Theoretical computer science</title>
<title level="j" type="abbreviated">Theor. comput. sci.</title>
<idno type="ISSN">0304-3975</idno>
<imprint><date when="2006">2006</date>
</imprint><seriesStmt><title level="j" type="main">Theoretical computer science</title>
<title level="j" type="abbreviated">Theor. comput. sci.</title>
<idno type="ISSN">0304-3975</idno>
</seriesStmt><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Code</term>
<term>Computer theory</term>
<term>Formal specification</term>
<term>Formal verification</term>
<term>Mobile system</term>
<term>Refinement</term>
<term>Semantics</term>
<term>Spatial logic</term>
<term>System development</term>
<term>Temporal logic</term>
<term>UML</term>
</keywords><keywords scheme="Pascal" xml:lang="fr"><term>Spécification formelle</term>
<term>Logique temporelle</term>
<term>Vérification formelle</term>
<term>Code</term>
<term>Sémantique</term>
<term>Informatique théorique</term>
<term>Affinement</term>
<term>Système formel</term>
<term>Système mobile</term>
<term>Logique spatiale</term>
<term>Développement système</term>
<term>UML</term>
</keywords><front><div type="abstract" xml:lang="en">We define the spatio-temporal logic MTLA as an extension of Lamport's Temporal Logic of Actions TLA for the specification, verification, and formal development of systems that rely on mobile code. The formalism is validated by an encoding of models written in the mobile UML notation. We identify refinement principles for mobile systems and justify refinements of mobile UML state machines with the help of the MTLA semantics.</div>
</front><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0304-3975</s0>
</fA01><fA02 i1="01"><s0>TCSCDI</s0>
</fA02><fA03 i2="1"><s0>Theor. comput. sci.</s0>
</fA03><fA05><s2>351</s2>
</fA05><fA08 i1="01" i2="1" l="ENG"><s1>Specification and refinement of mobile systems in MTLA and mobile UML</s1>
</fA08><fA09 i1="01" i2="1" l="ENG"><s1>Algebraic methodology and software technology</s1>
</fA09><fA11 i1="01" i2="1"><s1>KNAPP (Alexander)</s1>
</fA11><fA11 i1="02" i2="1"><s1>MERZ (Stephan)</s1>
</fA11><fA11 i1="03" i2="1"><s1>WIRSING (Martin)</s1>
</fA11><fA11 i1="04" i2="1"><s1>ZAPPE (Julia)</s1>
</fA11><fA12 i1="01" i2="1"><s1>MAHARAJ (Savi)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="02" i2="1"><s1>SHANKLAND (Carron)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="03" i2="1"><s1>RATTRAY (Charles)</s1>
<s9>ed.</s9>
</fA12><fA14 i1="01"><s1>Institut für Informatik, Ludwig-Maximilians-Universität</s1>
<s2>Munich</s2>
<s3>DEU</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
<sZ>4 aut.</sZ>
</fA14><fA14 i1="02"><s1>INRIA Lorraine & LORIA</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
<sZ>4 aut.</sZ>
</fA14><fA15 i1="01"><s1>Department of Computing Science and Mathematics, University of Stirling</s1>
<s2>Stirling, FK9 4LA</s2>
<s3>GBR</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</fA15><fA20><s1>184-202</s1>
</fA20><fA21><s1>2006</s1>
</fA21><fA23 i1="01"><s0>ENG</s0>
</fA23><fA43 i1="01"><s1>INIST</s1>
<s2>17243</s2>
<s5>354000133193310040</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 2006 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>28 ref.</s0>
</fA45><fA47 i1="01" i2="1"><s0>06-0160706</s0>
</fA47><fA60><s1>P</s1>
<s2>C</s2>
</fA60><fA64 i1="01" i2="1"><s0>Theoretical computer science</s0>
</fA64><fA66 i1="01"><s0>NLD</s0>
</fA66><fC01 i1="01" l="ENG"><s0>We define the spatio-temporal logic MTLA as an extension of Lamport's Temporal Logic of Actions TLA for the specification, verification, and formal development of systems that rely on mobile code. The formalism is validated by an encoding of models written in the mobile UML notation. We identify refinement principles for mobile systems and justify refinements of mobile UML state machines with the help of the MTLA semantics.</s0>
</fC01><fC02 i1="01" i2="X"><s0>001A02A01B</s0>
</fC02><fC02 i1="02" i2="X"><s0>001D02B09</s0>
</fC02><fC02 i1="03" i2="X"><s0>001D02A05</s0>
</fC02><fC02 i1="04" i2="X"><s0>001D02A02</s0>
</fC02><fC03 i1="01" i2="X" l="FRE"><s0>Spécification formelle</s0>
<s5>17</s5>
</fC03><fC03 i1="01" i2="X" l="ENG"><s0>Formal specification</s0>
<s5>17</s5>
</fC03><fC03 i1="01" i2="X" l="SPA"><s0>Especificación formal</s0>
<s5>17</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Logique temporelle</s0>
<s5>18</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Temporal logic</s0>
<s5>18</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Lógica temporal</s0>
<s5>18</s5>
</fC03><fC03 i1="03" i2="3" l="FRE"><s0>Vérification formelle</s0>
<s5>19</s5>
</fC03><fC03 i1="03" i2="3" l="ENG"><s0>Formal verification</s0>
<s5>19</s5>
</fC03><fC03 i1="04" i2="X" l="FRE"><s0>Code</s0>
<s5>20</s5>
</fC03><fC03 i1="04" i2="X" l="ENG"><s0>Code</s0>
<s5>20</s5>
</fC03><fC03 i1="04" i2="X" l="SPA"><s0>Código</s0>
<s5>20</s5>
</fC03><fC03 i1="05" i2="X" l="FRE"><s0>Sémantique</s0>
<s5>21</s5>
</fC03><fC03 i1="05" i2="X" l="ENG"><s0>Semantics</s0>
<s5>21</s5>
</fC03><fC03 i1="05" i2="X" l="SPA"><s0>Semántica</s0>
<s5>21</s5>
</fC03><fC03 i1="06" i2="X" l="FRE"><s0>Informatique théorique</s0>
<s5>22</s5>
</fC03><fC03 i1="06" i2="X" l="ENG"><s0>Computer theory</s0>
<s5>22</s5>
</fC03><fC03 i1="06" i2="X" l="SPA"><s0>Informática teórica</s0>
<s5>22</s5>
</fC03><fC03 i1="07" i2="X" l="FRE"><s0>Affinement</s0>
<s5>23</s5>
</fC03><fC03 i1="07" i2="X" l="ENG"><s0>Refinement</s0>
<s5>23</s5>
</fC03><fC03 i1="07" i2="X" l="SPA"><s0>Afinamiento</s0>
<s5>23</s5>
</fC03><fC03 i1="08" i2="X" l="FRE"><s0>Système formel</s0>
<s4>INC</s4>
<s5>72</s5>
</fC03><fC03 i1="09" i2="X" l="FRE"><s0>Système mobile</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fC03 i1="09" i2="X" l="ENG"><s0>Mobile system</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fC03 i1="10" i2="X" l="FRE"><s0>Logique spatiale</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03><fC03 i1="10" i2="X" l="ENG"><s0>Spatial logic</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03><fC03 i1="11" i2="X" l="FRE"><s0>Développement système</s0>
<s4>CD</s4>
<s5>98</s5>
</fC03><fC03 i1="11" i2="X" l="ENG"><s0>System development</s0>
<s4>CD</s4>
<s5>98</s5>
</fC03><fC03 i1="12" i2="X" l="FRE"><s0>UML</s0>
<s4>CD</s4>
<s5>99</s5>
</fC03><fC03 i1="12" i2="X" l="ENG"><s0>UML</s0>
<s4>CD</s4>
<s5>99</s5>
</fC03><fN21><s1>100</s1>
</fN21><pR><fA30 i1="01" i2="1" l="ENG"><s1>International Conference on Algebraic Methodology and Software Technology</s1>
<s2>10</s2>
<s3>Stirling GBR</s3>
<s4>2004-07-12</s4>
</fA30><server><NO>PASCAL 06-0160706 INIST</NO>
<ET>Specification and refinement of mobile systems in MTLA and mobile UML</ET>
<AU>KNAPP (Alexander); MERZ (Stephan); WIRSING (Martin); ZAPPE (Julia); MAHARAJ (Savi); SHANKLAND (Carron); RATTRAY (Charles)</AU>
<AF>Institut für Informatik, Ludwig-Maximilians-Universität/Munic h/Allemagne (1 aut., 3 aut., 4 aut.); INRIA Lorraine & LORIA/Nancy/France (2 aut., 4 aut.); Department of Computing Science and Mathematics, University of Stirling/Stirling, FK9 4LA/Royaume-Uni (1 aut., 2 aut., 3 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Theoretical computer science; ISSN 0304-3975; Coden TCSCDI; Pays-Bas; Da. 2006; Vol. 351; No. 2; Pp. 184-202; Bibl. 28 ref.</SO>
<LA>Anglais</LA>
<EA>We define the spatio-temporal logic MTLA as an extension of Lamport's Temporal Logic of Actions TLA for the specification, verification, and formal development of systems that rely on mobile code. The formalism is validated by an encoding of models written in the mobile UML notation. We identify refinement principles for mobile systems and justify refinements of mobile UML state machines with the help of the MTLA semantics.</EA>
<CC>001A02A01B; 001D02B09; 001D02A05; 001D02A02</CC>
<FD>Spécification formelle; Logique temporelle; Vérification formelle; Code; Sémantique; Informatique théorique; Affinement; Système formel; Système mobile; Logique spatiale; Développement système; UML</FD>
<ED>Formal specification; Temporal logic; Formal verification; Code; Semantics; Computer theory; Refinement; Mobile system; Spatial logic; System development; UML</ED>
<SD>Especificación formal; Lógica temporal; Código; Semántica; Informática teórica; Afinamiento</SD>
<LO>INIST-17243.354000133193310040</LO>
<ID>06-0160706</ID>
</server>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000461 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000461 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= PascalFrancis
|étape= Corpus
|type= RBID
|clé= Pascal:06-0160706
|texte= Specification and refinement of mobile systems in MTLA and mobile UML
}}
| This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022 |  |
