Abstract State Machines, Alloy, B, VDM, and Z

Name: Abstract State Machines, Alloy, B, VDM, and Z | Third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

Third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings

John Derrick John Fitzgerald Stefania Gnesi Sarfraz Khurshid Michael Leuschel Steve Reeves Elvinia Riccobene(Herausgeber*in)

Springer (Verlag)

Erschienen am 26. Juni 2012

XV, 378 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-30885-7 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Title
Organization
Table of Contents
Invited Talks
Contribution to a Rigorous Analysis of Web Application Frameworks
Introduction
Concrete Goals and Results So Far
Modeling Browser Components
Browsing Context
Renderer
Event Loop
A High-Level WebServer Model
Functional Request-Reply Web Server View
Refinement for File Transfer Execution
Refinement for Common Gateway Module Execution
Refinement for Scripting Module Execution
The Challenge of Accurate Analysis
References
Integrated Operational Semantics: Small-Step, Big-Step and Multi-step
Introduction
Expressions
Commands
Local State
Control Structures
Concurrency
Big-Step Operational Semantics
Multi-step Operational Semantics
Aliasing
Conclusions and Related Work
References
ASM Papers
Test Generation for Sequential Nets of Abstract State Machines
Introduction
Background
Test Generation for ASMs by Model Checking
Sequential Nets of Abstract State Machines
Description of the Web Application Case Study
Definition of Sequential Net of ASMs
Product Machine
Test Generation for Sequential Nets of ASMs
Generating the Test Suites for Every Machine
Building the Test Sequence Graph
Combining the Tests by Visiting the Test Sequence Graph
Coverage
Limits of the Approach
Initial Experiment
Model-Based Testing of Web-Based Applications
Related Work
Future Work and Conclusion
References
ASM and Controller Synthesis
Introduction
The Controller Synthesis Problem
Undecidability of Controller Synthesis
Computable Controller Synthesis
An Example: Eating with Chopsticks
Food and Chopsticks
Chopsticks and Hand
Continuous Controller Synthesis
Continuous ASM
Continuous Controller Synthesis
Continuous Grasping
Decomposing Continuous Grasping
Conclusion
References
Continuous ASM, and a Pacemaker Sensing Fragment
Introduction
Heart Pacemakers, the Pacemaker Challenge, and Sensing
ASM, Discrete and Continuous
Continuous ASM Models
Continuous ASM Refinement and Retrenchment
Pacemaker Sensing
Sensing Models
The Reference Model
Heartrate-Aware ASM Sensing
On EgmA and EgmCVH
Conclusion
References
An ASM Model of Concurrency in a Web Browser
Introduction
Notation
Transport Layer
Channels and Buffers
HTTP Request/Response
Stream Layer
HTML Streams
Script Streams
Image Streams
Conclusions
References
Alloy Papers
Modeling the Supervisory Control Theory with Alloy
Introduction
Typical Control Problems within the Framework of SCT
State-Based Formulation of Properties
Controllability Property
Normality Property
N-Inference Observability Property
Observational Equivalence Property (Observer)
Implementation of Iterative Specification Refinement Processes
Conclusion
References
Preventing Arithmetic Overflows in Alloy
Introduction
Prototypical Overflow Anomalies
Motivating Example
Approach
User-Level Semantics
Implementation-Level Semantics
Correspondence between the Two Semantics
The Law of the Excluded Middle
Implementation in Circuits
Evaluation
Related Work
References
Extending Alloy with Partial Instances
Introduction
Using Alloy with Partial Instances
Test-Driven Development
Regression Testing of Alloy Models
Modelling by Example
Combined Modelling and Meta-modelling
Language Extension
Semantics
Experiments
Micro Benchmark
Staged Evaluation
Alternatives Considered
Static Analysis
Syntactic Alternatives for the Partial Instance Block
Conclusion
References
Toward a More Complete Alloy
Introduction
Overview of Results
A Sample Application
Related Work
Background: Order-Sorted Predicate Logic and Term Models
Skolemization
A Finite Model Theorem for Order-Sorted Logic
Algorithms
Future Work
References
Temporal Logic Model Checking in Alloy
Introduction
Background
Temporal Logic Model Checking
Alloy
Translating CTLFC to FO(TC)
Model Checking in Alloy
Model Checking Classes of Transition Systems
Experimental Validation
Related Work
Conclusion
References
Active Attacking Multicast Key Management Protocol Using Alloy
Introduction
Overview of the Improved Tanaka-Sato Protocol
Alloy Model of the Active Intruder
Basic Components of the Active Intruder
Main Operations of the Active Intruder
Analysis of the Model
Counterexample of Assertion InsiderCanSend
Counterexample of Assertion InsiderCanRead
Counterexample of Assertion OutsiderCantSend
Counterexample of Assertion OutsiderCantRead
Result
Conclusion
References
B Papers
Formalizing Hybrid Systems with Event-B
Introduction
Approaches
The Approach of Action System to Hybrid Systems
The Proposed Approach with Event-B
Examples
The Saw [2]
Nuclear Plant Cooling [3]
Controlling Trains [4]
Aircraft Collision Avoidance [4] [5]
Conclusion
References
SMT Solvers for Rodin
Introduction
Translating Event-B to SMT
The $\lambda$-Based Approach
The ppTrans Approach
A Small Event-B Example
Solving SMT Formulas
Unquantified Formulas
Instantiation Techniques
Unsat Core Extraction
Experimental Results
Conclusion
References
Refinement Plans for Informed Formal Design
Introduction
Background
Event-B Refinement by Example
Reasoned Modelling Critics
HRemo
Refinement Plans
The Accumulator Refinement Plan
Accumulator Refinement Plan Critics
Combining Modelling Patterns with HRemo
Implementation and Results
Related and Future Work
Conclusions
References
Refinement by Interface Instantiation
Introduction
Event-B
Instantiation
Case Study: Modelling of a Cruise Control System
The Full Model: Refinement, Decomposition and Instantiation
Decomposition: Introducing Interfaces
Mixing Instantiation and Refinement
Repeated Instantiation
Correctness
Conclusion
References
Discharging Proof Obligations from Atelier B Using Multiple Automated Provers
Introduction
Background
The B Environment
The Why3 System
A Translator from B to Why3
Modeling B Set Operators as Why3 Theories
The Translation Process
Soundness of the Translation
Experiments
Comparison with Related Work
Conclusion and Perspectives
References
VDM Papers
A Semantic Analysis of Logics That Cope with Partial Terms
Introduction
The Basis of the Semantics
Classical Logic: Making All Terms Denote
Classical Logic: Variant Relational Operators
Non-classical Logic: LPF
Discussion
A Comparison of the Approaches Considered
Further Approaches
Conclusions
References
Combining VDM with Executable Code
Introduction
The Vienna Development Method
Combining VDM Interpretation with External Code
The External Call Interface
The Remote Control Interface
Case Study
Related Work
Conclusion and Future Work
References
Z Papers
Extending the Test Template Frameworkto Deal with Axiomatic Descriptions, Quantifiers and Set Comprehensions
Introduction
Some Extensions to the Test Template Framework
Axiomatic Descriptions
Quantified Formulas
Set Comprehensions and Lambda Expressions
A Taxonomy of Axiomatic Descriptions
Given Type Constants (C)
Synonyms (S)
Equivalences (E)
Inductive Definitions (ID)
All Other Axiomatic Descriptions (O)
Testing Tactics for Quantifications
Weak Existential Quantifier (WEQ)
Strong Existential Quantifier (SEQ)
Universal Quantifications
Testing Tactics for Set Comprehensions
Concluding Remarks
References
A Tool Chain for the Automatic Generation of Circus Specifications of Simulink Diagrams
Introduction
Background
Translating Simulink Diagrams into Circus Specifications
Z Producer, Generics Converter, and PP2CZT
Type Extractor and Merge
ClawCircus
\LATEX, and the Circus Parser and Type Checker
Enabled and Action Subsystems
Z Definitions
Circus Model
Conclusions and Further Work
References
Verification of Hardware Interaction Properties of Software
Introduction
Document Outline
Disassembly
Behaviour Model Structure
System State Specification
Sequential Instruction Templates
Branch Instruction Templates
Analysis Process
Branch Identification
Formal Instantiation
Simplification
Program Encapsulation
An Example Verification
Conclusion
References
ASM Short Papers
Using the Arbitrator Pattern for Dynamic Process-Instance Extension in a Work-Flow Management System
Basic Problem
The Arbitrator Pattern
The Arbitrator Pattern in S-BPM - The Resulting Specification
Final Thoughts
References
A Unified Processor Model for Compiler Verification and Simulation Using ASM
Introduction
Correctness of Instruction Selection
Fast Cycle-Accurate Simulation
Preliminary Results and Conclusion
References
Modeling Synchronization/Communication Patterns in Vision-Based Robot Control Applications Using ASMs
Introduction
Application Domain and Background Concepts
ASM Models of Tasks Synchronization/Communication
Future Directions
References
A Reliability Prediction Method for Abstract State Machines
Introduction
Modeling the Reliability of ASM Specifications
Conclusions and Future Work
References
A Simplified Parallel ASM Thesis
Parallel ASMs in the Light of the DB-ASM Thesis
A Modified Set of Postulates
An Expected Equivalence Result
References
Refactoring Abstract State Machine Models
Introduction
Pattern-Based Approach
Extract Rule Pattern
Parameterize Rule Pattern
Concluding Remarks
References
B Short Papers
Continuous Behaviour in Event-B: A Sketch
Introduction
Extending Event-B with Continuous Behaviour
Discussion, POs
Formal Verification of PLC Programs Using the B Method
Introduction
The Method
Towards the PLC Model
Generation of the B Model
Discussions and Future Work
References
A Practical Event-B Refinement Method Based on a UML-Driven Development Process
Introduction
From ICONIX to Event-B
Related Work
Discussions and Ongoing Work
References
Learn and Test for Event-B - A Rodin Plugin
Introduction
Tool Overview
The Tool Applied to an Example
References
Event-B Code Generation: Type Extension with Theories
Introduction
An Array Theory
An Event-B Model
Adding Translation Rules
Conclusion
References
Formal Proofs for the NYCT Line 7 (Flushing) Modernization Project
Introduction
Goals and Expected Benefits
Expected Benefits
Methodology
Methodology for Natural Language "Proofs"
Results So Far
Conclusion
References
A Pattern for Modelling Fault Tolerant Systems in Event-B
Introduction
A Development Pattern
Basic Model
Time
Structure.
Simplicity.
Fault Handling
Conclusions
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken