Formal Methods and Software Engineering 8th International Conference on Formal Engineering Methods, ICFEM 2006, Macao, China, November 1-3, 2006. Proceedings /
Συγγραφή απο Οργανισμό/Αρχή: | |
---|---|
Άλλοι συγγραφείς: | , |
Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
Γλώσσα: | English |
Έκδοση: |
Berlin, Heidelberg :
Springer Berlin Heidelberg,
2006.
|
Σειρά: | Lecture Notes in Computer Science,
4260 |
Θέματα: | |
Διαθέσιμο Online: | Full Text via HEAL-Link |
Πίνακας περιεχομένων:
- Keynote Talks
- Program Verification Through Computer Algebra
- JML’s Rich, Inherited Specifications for Behavioral Subtypes
- Three Perspectives in Formal Engineering
- Specification and Verification
- A Method for Formalizing, Analyzing, and Verifying Secure User Interfaces
- Applying Timed Interval Calculus to Simulink Diagrams
- Reducing Model Checking of the Few to the One
- Induction-Guided Falsification
- Verifying ? Models of Industrial Systems with Spin
- Stateful Dynamic Partial-Order Reduction
- Internetware and Web-Based Systems
- User-Defined Atomicity Constraint: A More Flexible Transaction Model for Reliable Service Composition
- Environment Ontology-Based Capability Specification for Web Service Discovery
- Scenario-Based Component Behavior Derivation
- Verification of Computation Orchestration Via Timed Automata
- Towards the Semantics for Web Service Choreography Description Language
- Type Checking Choreography Description Language
- Concurrent, Communicating, Timing and Probabilistic Systems
- Formalising Progress Properties of Non-blocking Programs
- Towards a Fully Generic Theory of Data
- Verifying Statemate Statecharts Using CSP and FDR
- A Reasoning Method for Timed CSP Based on Constraint Solving
- Mapping RT-LOTOS Specifications into Time Petri Nets
- Reasoning Algebraically About Probabilistic Loops
- Object and Component Orientation
- Formal Verification of the Heap Manager of an Operating System Using Separation Logic
- A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs
- Model Checking Dynamic UML Consistency
- Testing and Model Checking
- Conditions for Avoiding Controllability Problems in Distributed Testing
- Generating Test Cases for Constraint Automata by Genetic Symbiosis Algorithm
- Checking the Conformance of Java Classes Against Algebraic Specifications
- Incremental Slicing
- Assume-Guarantee Software Verification Based on Game Semantics
- Optimized Execution of Deterministic Blocks in Java PathFinder
- Tools
- A Tool for a Formal Pattern Modeling Language
- An Open Extensible Tool Environment for Event-B
- Tool for Translating Simulink Models into Input Language of a Model Checker
- Fault-Tolerance and Security
- Verifying Abstract Information Flow Properties in Fault Tolerant Security Devices
- A Language for Modeling Network Availability
- Multi-process Systems Analysis Using Event B: Application to Group Communication Systems
- Specification and Refinement
- Issues in Implementing a Model Checker for Z
- Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking
- Discovering Likely Method Specifications
- Time Aware Modelling and Analysis of Multiclocked VLSI Systems
- SALT—Structured Assertion Language for Temporal Logic.