FEEDBACK Smiley face

Theoretical and Practical Aspects of SPIN Model Checking (Record no. 14692)

000 -LEADER
fixed length control field 04724nam a22005775i 4500
001 - CONTROL NUMBER
control field 978-3-540-48234-5
003 - CONTROL NUMBER IDENTIFIER
control field DE-He213
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20170515111506.0
007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION
fixed length control field cr nn 008mamaa
008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION
fixed length control field 121227s1999 gw | s |||| 0|eng d
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 9783540482345
-- 978-3-540-48234-5
024 7# - OTHER STANDARD IDENTIFIER
Standard number or code 10.1007/3-540-48234-2
Source of number or code doi
050 #4 - LIBRARY OF CONGRESS CALL NUMBER
Classification number QA76.75-76.765
072 #7 - SUBJECT CATEGORY CODE
Subject category code UFM
Source bicssc
072 #7 - SUBJECT CATEGORY CODE
Subject category code COM077000
Source bisacsh
082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER
Classification number 004
Edition number 23
245 10 - TITLE STATEMENT
Title Theoretical and Practical Aspects of SPIN Model Checking
Medium [electronic resource] :
Remainder of title 5th and 6th International SPIN Workshops Trento, Italy, July 5, 1999 Toulouse, France, September 21 and 24, 1999 Proceedings /
Statement of responsibility, etc edited by Dennis Dams, Rob Gerth, Stefan Leue, Mieke Massink.
264 #1 -
-- Berlin, Heidelberg :
-- Springer Berlin Heidelberg,
-- 1999.
300 ## - PHYSICAL DESCRIPTION
Extent X, 282 p.
Other physical details online resource.
336 ## -
-- text
-- txt
-- rdacontent
337 ## -
-- computer
-- c
-- rdamedia
338 ## -
-- online resource
-- cr
-- rdacarrier
347 ## -
-- text file
-- PDF
-- rda
490 1# - SERIES STATEMENT
Series statement Lecture Notes in Computer Science,
International Standard Serial Number 0302-9743 ;
Volume number/sequential designation 1680
505 0# - FORMATTED CONTENTS NOTE
Formatted contents note 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.
520 ## - SUMMARY, ETC.
Summary, etc 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 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Mathematics.
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Software engineering.
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Programming languages (Electronic computers).
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer logic.
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer software.
650 14 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Mathematics.
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Mathematical Software.
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Logics and Meanings of Programs.
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Software Engineering.
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Programming Languages, Compilers, Interpreters.
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Dams, Dennis.
Relator term editor.
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Gerth, Rob.
Relator term editor.
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Leue, Stefan.
Relator term editor.
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Massink, Mieke.
Relator term editor.
710 2# - ADDED ENTRY--CORPORATE NAME
Corporate name or jurisdiction name as entry element SpringerLink (Online service)
773 0# - HOST ITEM ENTRY
Title Springer eBooks
776 08 - ADDITIONAL PHYSICAL FORM ENTRY
Display text Printed edition:
International Standard Book Number 9783540664994
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
Uniform title Lecture Notes in Computer Science,
-- 0302-9743 ;
Volume number/sequential designation 1680
856 40 - ELECTRONIC LOCATION AND ACCESS
Uniform Resource Identifier http://dx.doi.org/10.1007/3-540-48234-2
912 ## -
-- ZDB-2-SCS
912 ## -
-- ZDB-2-LNC
912 ## -
-- ZDB-2-BAE
942 ## - ADDED ENTRY ELEMENTS (KOHA)
Source of classification or shelving scheme
Koha item type e-Book

No items available.


© IIIT-Delhi, 2013 | Phone: +91-11-26907510| FAX +91-11-26907405 | E-mail: library@iiitd.ac.in