Model Checking Software : 8th International SPIN Workshop, Toronto, Canada, May 19-20, 2001 Proceedings / / edited by Matthew Dwyer
| Model Checking Software : 8th International SPIN Workshop, Toronto, Canada, May 19-20, 2001 Proceedings / / edited by Matthew Dwyer |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (X, 318 p.) |
| Disciplina | 005.1/4 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computer logic Software Engineering/Programming and Operating Systems Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Software Engineering |
| ISBN | 3-540-45139-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Keynotes -- From model checking to a temporal proof -- Model checking if your life depends on it: a view from intel’s trenches -- Model checking if your life depends on it: a view from intel’s trenches -- Technical Papers and Tool Reports -- Model-checking in finite state-space systems with fine-grained abstractions using SPIN -- Implementing LTL model checking with net unfoldings -- Directed explicit model checking with HSF-SPIN -- Directed explicit model checking with HSF-SPIN -- Addressing dynamic issues of program model checking -- Addressing dynamic issues of program model checking -- Automatically validating temporal safety properties of interfaces -- Automatically validating temporal safety properties of interfaces -- Verification experiments on the MASCARA protocol -- Verification experiments on the MASCARA protocol -- Using SPIN for feature interaction analysis - a case study -- Using SPIN for feature interaction analysis - a case study -- Behavioural analysis of the enterprise javaBeans™ component architecture -- Behavioural analysis of the enterprise javaBeans™ component architecture -- p2b: A translation utility for linking promela and symbolic model checking (tool paper) -- p2b: A translation utility for linking promela and symbolic model checking (tool paper) -- Transformations for model checking distributed java programs -- Transformations for model checking distributed java programs -- Distributed LTL model-checking in SPIN -- Distributed LTL model-checking in SPIN -- Parallel state space construction for model-checking -- Parallel state space construction for model-checking -- Model checking systems of replicated processes with spin -- Model checking systems of replicated processes with spin -- A SPIN-based model checker for telecommunication protocols -- A SPIN-based model checker for telecommunication protocols -- Modeling and verifying a price model for congestion control in computer networks using promela/spin -- Modeling and verifying a price model for congestion control in computer networks using promela/spin -- Invited Project Summaries -- A model checking project at philips research -- Applications of model checking at honeywell laboratories -- Coarse-granular model checking in practice. |
| Altri titoli varianti | SPIN '01 |
| Record Nr. | UNISA-996465900503316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Model Checking Software : 8th International SPIN Workshop, Toronto, Canada, May 19-20, 2001 Proceedings / / edited by Matthew Dwyer
| Model Checking Software : 8th International SPIN Workshop, Toronto, Canada, May 19-20, 2001 Proceedings / / edited by Matthew Dwyer |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (X, 318 p.) |
| Disciplina | 005.1/4 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computer logic Software Engineering/Programming and Operating Systems Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Software Engineering |
| ISBN | 3-540-45139-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Keynotes -- From model checking to a temporal proof -- Model checking if your life depends on it: a view from intel’s trenches -- Model checking if your life depends on it: a view from intel’s trenches -- Technical Papers and Tool Reports -- Model-checking in finite state-space systems with fine-grained abstractions using SPIN -- Implementing LTL model checking with net unfoldings -- Directed explicit model checking with HSF-SPIN -- Directed explicit model checking with HSF-SPIN -- Addressing dynamic issues of program model checking -- Addressing dynamic issues of program model checking -- Automatically validating temporal safety properties of interfaces -- Automatically validating temporal safety properties of interfaces -- Verification experiments on the MASCARA protocol -- Verification experiments on the MASCARA protocol -- Using SPIN for feature interaction analysis - a case study -- Using SPIN for feature interaction analysis - a case study -- Behavioural analysis of the enterprise javaBeans™ component architecture -- Behavioural analysis of the enterprise javaBeans™ component architecture -- p2b: A translation utility for linking promela and symbolic model checking (tool paper) -- p2b: A translation utility for linking promela and symbolic model checking (tool paper) -- Transformations for model checking distributed java programs -- Transformations for model checking distributed java programs -- Distributed LTL model-checking in SPIN -- Distributed LTL model-checking in SPIN -- Parallel state space construction for model-checking -- Parallel state space construction for model-checking -- Model checking systems of replicated processes with spin -- Model checking systems of replicated processes with spin -- A SPIN-based model checker for telecommunication protocols -- A SPIN-based model checker for telecommunication protocols -- Modeling and verifying a price model for congestion control in computer networks using promela/spin -- Modeling and verifying a price model for congestion control in computer networks using promela/spin -- Invited Project Summaries -- A model checking project at philips research -- Applications of model checking at honeywell laboratories -- Coarse-granular model checking in practice. |
| Altri titoli varianti | SPIN '01 |
| Record Nr. | UNINA-9910143603403321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Lo trovi qui: Univ. Federico II | ||
| ||