Abstract State Machines, Alloy, B and Z Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Frappier, Marc (Επιμελητής έκδοσης), Glässer, Uwe (Επιμελητής έκδοσης), Khurshid, Sarfraz (Επιμελητής έκδοσης), Laleau, Régine (Επιμελητής έκδοσης), Reeves, Steve (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2010.
• Σειρά: Lecture Notes in Computer Science, 5977
• Θέματα: Computer science.; Computers.; Algorithms.; Computer logic.; Mathematical logic.; Computer science > Mathematics.; Computer Science.; Theory of Computation.; Mathematical Logic and Formal Languages.; Logics and Meanings of Programs.; Algorithm Analysis and Problem Complexity.; Computation by Abstract Devices.; Mathematics of Computing.

Πίνακας περιεχομένων:

• 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.