//]]>

Abstract State Machines, Alloy, B and Z (Record no. 12853)

000 -LEADER
fixed length control field 05679nam a22005415i 4500
003 - CONTROL NUMBER IDENTIFIER
control field OSt
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20140310144047.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 100305s2010 gw | s |||| 0|eng d
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 9783642118111
978-3-642-11811-1
050 #4 - LIBRARY OF CONGRESS CALL NUMBER
Classification number QA8.9-QA10.3
082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER
Classification number 005.131
Edition number 23
264 #1 -
-- Berlin, Heidelberg :
-- Springer Berlin Heidelberg,
-- 2010.
912 ## -
-- ZDB-2-SCS
-- ZDB-2-LNC
100 1# - MAIN ENTRY--PERSONAL NAME
Personal name Frappier, Marc.
Relator term editor.
245 10 - IMMEDIATE SOURCE OF ACQUISITION NOTE
Title Abstract State Machines, Alloy, B and Z
Medium [electronic resource] :
Remainder of title Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings /
Statement of responsibility, etc edited by Marc Frappier, Uwe Glässer, Sarfraz Khurshid, Régine Laleau, Steve Reeves.
300 ## - PHYSICAL DESCRIPTION
Extent XIV, 416p. 95 illus.
Other physical details online resource.
440 1# - SERIES STATEMENT/ADDED ENTRY--TITLE
Title Lecture Notes in Computer Science,
International Standard Serial Number 0302-9743 ;
Volume number/sequential designation 5977
505 0# - FORMATTED CONTENTS NOTE
Formatted contents note Invited Talks -- A Structure for Dependability Arguments -- Formal Probabilistic Analysis: A Higher-Order Logic Based Approach -- ASM Papers -- Synchronous Message Passing and Semaphores: An Equivalence Proof -- AsmL-Based Concurrency Semantic Variations for Timed Use Case Maps -- Bârun: A Scripting Language for CoreASM -- AsmetaSMV: A Way to Link High-Level ASM Models to Low-Level NuSMV Specifications -- An Executable Semantics of the SystemC UML Profile -- Alloy Papers -- Specifying Self-configurable Component-Based Systems with FracToy -- Trace Specifications in Alloy -- An Imperative Extension to Alloy -- Towards Formalizing Network Architectural Descriptions -- Lightweight Modeling of Java Virtual Machine Security Constraints -- Alloy+HotCore: A Fast Approximation to Unsat Core -- B Papers -- Supporting Reuse in Event B Development: Modularisation Approach -- Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance -- Applying the B Method for the Rigorous Development of Smart Card Applications -- Automatic Verification for a Class of Proof Obligations with SMT-Solvers -- A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking -- Development of a Synchronous Subset of AADL -- Matelas: A Predicate Calculus Common Formal Definition for Social Networking -- Structured Event-B Models and Proofs -- Refinement-Animation for Event-B — Towards a Method of Validation -- Reactivising Classical B -- Event-B Decomposition for Parallel Programs -- Z Papers -- Communication Systems in ClawZ -- Formalising and Validating RBAC-to-XACML Translation Using Lightweight Formal Methods -- Towards Formally Templated Relational Database Representations in Z -- Translating Z to Alloy -- ABZ Short Papers (Abstracts) -- B-ASM: Specification of ASM à la B -- A Case for Using Data-Flow Analysis to Optimize Incremental Scope-Bounded Checking -- On the Modelling and Analysis of Amazon Web Services Access Policies -- Architecture as an Independent Variable for Aspect-Oriented Application Descriptions -- ParAlloy: Towards a Framework for Efficient Parallel Analysis of Alloy Models -- Introducing Specification-Based Data Structure Repair Using Alloy -- Secrecy UML Method for Model Transformations -- Improving Traceability between KAOS Requirements Models and B Specifications -- Code Synthesis for Timed Automata: A Comparison Using Case Study -- Towards Validation of Requirements Models -- A Proof Based Approach for Formal Verification of Transactional BPEL Web Services -- On an Extensible Rule-Based Prover for Event-B -- B Model Abstraction Combining Syntactic and Semantic Methods -- A Basis for Feature-Oriented Modelling in Event-B -- Using Event-B to Verify the Kmelia Components and Their Assemblies -- Starting B Specifications from Use Cases -- Integrating SMT-Solvers in Z and B Tools -- Formal Analysis in Model Management: Exploiting the Power of CZT.
520 ## - SUMMARY, ETC.
Summary, etc This book constitutes the proceedings of the Second International Conference on Abstract State Machines, B and Z, which took place in Orford, QC, Canada, in February 2010. The 26 full papers presented were carefully reviewed and selected from 60 submissions. The book also contains two invited talks and abstracts of 18 short papers which address work in progress, industrial experience reports and tool descriptions. The papers cover recent advances in four equally rigorous methods for software and hardware development: abstract state machines (ASM), Alloy, B and Z. They share a common conceptual framework, centered around the notions of state and operation, and promote mathematical precision in the modeling, verification and construction of highly dependable systems.
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer science.
Topical term or geographic name as entry element Computer software.
Topical term or geographic name as entry element Logic design.
Topical term or geographic name as entry element Computational complexity.
Topical term or geographic name as entry element Computer Science.
Topical term or geographic name as entry element Mathematical Logic and Formal Languages.
Topical term or geographic name as entry element Logics and Meanings of Programs.
Topical term or geographic name as entry element Algorithm Analysis and Problem Complexity.
Topical term or geographic name as entry element Computation by Abstract Devices.
Topical term or geographic name as entry element Mathematics of Computing.
Topical term or geographic name as entry element Discrete Mathematics in Computer Science.
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Glässer, Uwe.
Relator term editor.
Personal name Khurshid, Sarfraz.
Relator term editor.
Personal name Laleau, Régine.
Relator term editor.
Personal name Reeves, Steve.
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 9783642118104
856 40 - ELECTRONIC LOCATION AND ACCESS
Uniform Resource Identifier http://dx.doi.org/10.1007/978-3-642-11811-1
942 ## - ADDED ENTRY ELEMENTS (KOHA)
Source of classification or shelving scheme
Item type E-Book
Copies
Price effective from Permanent location Date last seen Not for loan Date acquired Source of classification or shelving scheme Koha item type Damaged status Lost status Withdrawn status Current location Full call number
2014-03-27AUM Main Library2014-03-27 2014-03-27 E-Book   AUM Main Library005.131
Languages: 
English |
العربية