Theoretical and practical aspects of SPIN model-checking : 5th and 6th International SPIN Workshops, Trento, Italy, July 5, 1999 Toulouse, France, September 21 and 24, 1999 : proceedings
Increasing the designer s con dence that a piece of software or hardwareis c- pliant with its speci cation has become a key objective in the design process for software and hardware systems. Many approaches to reaching this goal have been developed, including rigorous speci cation, formal veri catio...
Enregistré dans:
| Collectivités auteurs: | , |
|---|---|
| Andre forfattere: | , , |
| Format: | Livre numérique |
| Sprog: | Anglais |
| Udgivet: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Serier: | Lecture notes in computer science
1680 |
| Fag: | |
| Online adgang: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Kommentar: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Practical aspects of SPIN model-checking, 6th International Workshop, SPIN'99, held as FM'99 User Group Meeting, Toulouse, France, September 21 and 24, 1999, proceedings, Dennis Dams, Rob Gerth, Stefan Leue ... [et al.], (Eds.), 1999, New York, Springer, 1 vol. (X-276 p.), Lecture notes in computer science, 3-540-66499-8 • Theoretical and Practical Aspects of SPIN Model Checking, Texte imprimé, 9783662211687 |
| LEADER | 05382nam a22004337a 4500 | ||
|---|---|---|---|
| 001 | 971889 | ||
| 008 | 110927q2000 xxe ||| |||| 00| 0 eng d | ||
| 009 | PPN15521473X | ||
| 020 | |a 9783540482345 (PDF) | ||
| 041 | 0 | |a eng | |
| 082 | |a 004 | ||
| 111 | 2 | |a International SPIN Workshop |n (06 |d :1999 |c :Toulouse). | |
| 245 | 1 | 0 | |a Theoretical and practical aspects of SPIN model-checking : |b 5th and 6th International SPIN Workshops, Trento, Italy, July 5, 1999 Toulouse, France, September 21 and 24, 1999 : proceedings |c [edited by] Dennis Dams, Rob Gerth, Stefan Leue... [et al.]. |
| 260 | |a Berlin [etc.] : |b Springer. | ||
| 260 | |a Cham : |b Springer Nature, |c [20..]. | ||
| 490 | 0 | |a Lecture notes in computer science |v 1680 |x 1611-3349 | |
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 505 | 0 | |a I:Selection of Papers Presented at 5thSPIN99 -- Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving -- Runtime Efficient State Compaction in Spin -- Distributed-Memory Model Checking with SPIN -- Partial Order Reduction in Presence of Rendez-vous Communications with Unless Constructs and Weak Fairness -- Divide, Abstract, and Model-Check -- II: Papers Presented at 6thSPIN99 -- Formal Methods Adoption: What s Working, What s Not! -- Model Checking for Managers -- Xspin/Project - Integrated Validation Management for Xspin -- Analyzing Mode Confusion via Model Checking -- Detecting Feature Interactions in the Terrestrial Trunked Radio (TETRA) Network Using Promela and Xspin -- Java PathFinder A Translator from Java to Promela -- VIP: A Visual Interface for Promela -- Events in Property Patterns -- Assume-Guarantee Model Checking of Software: A Comparative Case Study -- A Framework for Automatic Construction of Abstract Promela Models -- Model Checking Operator Procedures -- Applying Model Checking in Java Verification -- The Engineering of a Model Checker: the Gnu i-Protocol Case Study Revisited. -- Embedding a Dialect of SDL in PROMELA -- dSPIN: A Dynamic Extension of SPIN. | |
| 506 | |a Accès en ligne pour les établissements français bénéficiaires des licences nationales | ||
| 506 | |a Accès soumis à abonnement pour tout autre établissement | ||
| 506 | |a Conditions particulières de réutilisation pour les bénéficiaires des licences nationales. https://www.licencesnationales.fr/springer-nature-ebooks-contrat-licence-ln-2017 | ||
| 520 | |a Increasing the designer s con dence that a piece of software or hardwareis c- pliant with its speci cation has become a key objective in the design process for software and hardware systems. Many approaches to reaching this goal have been developed, including rigorous speci cation, formal veri cation, automated validation, and testing. Finite-state model checking, as it is supported by the explicit-state model checkerSPIN,is enjoying a constantly increasingpopularity in automated property validation of concurrent, message based systems. SPIN has been in large parts implemented and is being maintained by Gerard Ho- mann, and is freely available via ftp fromnetlib.bell-labs.comor from URL http://cm.bell-labs.com/cm/cs/what/spin/Man/README.html. The beauty of nite-state model checking lies in the possibility of building \push-button" validation tools. When the state space is nite, the state-space traversal will eventually terminate with a de nite verdict on the property that is being validated. Equally helpful is the fact that in case the property is inv- idated the model checker will return a counterexample, a feature that greatly facilitates fault identi cation. On the downside, the time it takes to obtain a verdict may be very long if the state space is large and the type of properties that can be validated is restricted to a logic of rather limited expressiveness. | ||
| 650 | |a Génie logiciel | ||
| 650 | |a Informatique | ||
| 650 | |a Langages de programmation | ||
| 650 | |a Logiciels |x Développement | ||
| 650 | |a Actes de congrès | ||
| 700 | 1 | |a Dams, Dennis Rene, |d 1966- |4 pbd | |
| 700 | 1 | |a Gerth, Robert. |4 pbd | |
| 700 | 1 | |a Leue, Stefan, |d 1962-...., |c auteur en informatique. |4 pbd | |
| 711 | 2 | |a International SPIN Workshop |n (05 |d :1999 |c :Trento). |4 aut | |
| 776 | 0 | |0 04654738X |t Practical aspects of SPIN model-checking |o 6th International Workshop, SPIN'99, held as FM'99 User Group Meeting, Toulouse, France, September 21 and 24, 1999 |o proceedings |f Dennis Dams, Rob Gerth, Stefan Leue ... [et al.], (Eds.) |d 1999 |c New York |n Springer |p 1 vol. (X-276 p.) |s Lecture notes in computer science |z 3-540-66499-8 | |
| 776 | 0 | |t Theoretical and Practical Aspects of SPIN Model Checking |b Texte imprimé |z 9783662211687 | |
| 856 | 4 | |q PDF |u https://doi.org/10.1007/3-540-48234-2 |z Accès sur la plateforme de l'éditeur | |
| 856 | 4 | |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-06JPZC03-9 |z Accès sur la plateforme Istex | |
| 856 | 4 | |5 452349901:750602481 |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/3-540-48234-2 |z Accès Université d'Orléans | |
| 856 | 4 | |5 180339901:753962829 |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/3-540-48234-2 |z Accès INSA CVL | |
| 997 | |0 971889 |1 Livre numérique |a Ressource numérique |b INSA |b ENSA |c 0/Bibliothèque numérique/ |c 1/Bibliothèque numérique/Autre ressource numérique/ | ||