(UM)
-
Specification and verification of a parametric handover procedure using TLAKapus, TatjanaIn mobile systems, some nodes link dynamically through different channels at different times. The $▫pi▫$-calculus is a popular process algebra for specification and verification of systems with ... dynamic linking and synchronous, rendezvous message passing communication of component processes. Dynamic linking can be elegantly specified in it by sending channels to be used for further communication as messages. However, in order to be able to use the $▫pi▫$-calculus, one has to learn its process-algebraic concepts and laws. On the other hand, specification and verification in the Temporal Logic of Actions (TLA) is almost entirely based on ordinary mathematics (i.e., first-order predicate logic, set theory, etc.). Therefore, this paper proposes a TLA approach to the specification and verification of systems with synchronous communication and dynamic linking similar to the $▫pi▫$-calculus one. It is presented with help of a TLA specification and verification of a parametric mobile network handover procedure which has previously been specified with the ▫$pi$▫-calculus. In fact, TLA + is used as the specification language, thus achieving completely formal specifications.Vir: Journal of circuits, systems, and computers. - ISSN 0218-1266 (Vol. 15, no. 6, Dec. 2006, str. 881-906)Vrsta gradiva - članek, sestavni delLeto - 2006Jezik - angleškiCOBISS.SI-ID - 11418902
![loading ... loading ...](themes/default/img/ajax-loading.gif)
vir: Journal of circuits, systems, and computers. - ISSN 0218-1266 (Vol. 15, no. 6, Dec. 2006, str. 881-906)
![loading ... loading ...](themes/default/img/ajax-loading.gif)
![loading ... loading ...](themes/default/img/ajax-loading.gif)
![loading ... loading ...](themes/default/img/ajax-loading.gif)
Vnos na polico
Trajna povezava
- URL:
Faktor vpliva
Dostop do baze podatkov JCR je dovoljen samo uporabnikom iz Slovenije. Vaš trenutni IP-naslov ni na seznamu dovoljenih za dostop, zato je potrebna avtentikacija z ustreznim računom AAI.
Leto | Faktor vpliva | Izdaja | Kategorija | Razvrstitev | ||||
---|---|---|---|---|---|---|---|---|
JCR | SNIP | JCR | SNIP | JCR | SNIP | JCR | SNIP |
Baze podatkov, v katerih je revija indeksirana
Ime baze podatkov | Področje | Leto |
---|
Povezave do osebnih bibliografij avtorjev | Povezave do podatkov o raziskovalcih v sistemu SICRIS |
---|---|
Kapus, Tatjana | 00873 |
Vir: Osebne bibliografije
in: SICRIS
Izberite prevzemno mesto:
Prevzem gradiva po pošti
Naslov za dostavo:
Med podatki člana manjka naslov.
Storitev za pridobivanje naslova trenutno ni dostopna, prosimo, poskusite še enkrat.
S klikom na gumb "V redu" boste potrdili zgoraj izbrano prevzemno mesto in dokončali postopek rezervacije.
S klikom na gumb "V redu" boste potrdili zgoraj izbrano prevzemno mesto in naslov za dostavo ter dokončali postopek rezervacije.
S klikom na gumb "V redu" boste potrdili zgoraj izbrani naslov za dostavo in dokončali postopek rezervacije.
Obvestilo
Trenutno je storitev za avtomatsko prijavo in rezervacijo nedostopna. Gradivo lahko rezervirate sami na portalu Biblos ali ponovno poskusite tukaj kasneje.
Gesla v Splošnem geslovniku COBISS
Izbira mesta prevzema
Gradivo iz matične enote je brezplačno. Če je gradivo na mesto prevzema dostavljeno iz drugih enot, lahko knjižnica to storitev zaračuna.
Mesto prevzema | Status gradiva | Rezervacija |
---|
Rezervacija v teku
Prosimo, počakajte trenutek.
Rezervacija je uspela.
Rezervacija ni uspela.
Rezervacija...
Članska izkaznica:
Mesto prevzema: