Formal Aspects of Component Software
7th International Workshop, FACS 2010, Guimarães, Portugal, October 14-16, 2010, Revised Selected Papers
Published on 19. January 2012
X, 305 pages
978-3-642-27269-1 (ISBN)
Description
This book constitutes revised selected papers of the 7th International Workshop on Formal Aspects of Component Software, FACS 2010, held in Guimarães, Portugal, in October 2010.
The 13 full papers and 4 short papers presented together with 1 panel discussion and 2 invited talks were carefully reviewed and selected from 37 submissions. The workshop seeks to develop a better understanding on how formal methods can or should be used for component-based software development to succeed.
More details
Other editions
Additional editions
Luis Soares Barbosa | Markus Lumpe
Formal Aspects of Component Software
7th International Workshop, FACS 2010, Guimarães, Portugal, October 14-16, 2010, Revised Selected Papers
Book
03/2012
Springer
€53.49
Shipment within 7-9 days
Content
- Title Page
- Preface
- Organization
- Table of Contents
- Quantitative Analysis of Software: Challenges and Recent Advances
- Introduction
- Challenge: Environment Modeling
- Automatic Model Inference: The GameTime Approach
- Looking Ahead
- References
- Analysis of Service Oriented Software Systems with the Conversation Calculus
- Introduction
- Aspects of Services
- Distribution
- Communication, Contexts, and Context Sensitiveness
- Loose Coupling
- Other Aspects
- The Conversation Calculus
- Communication
- Service Oriented Idioms
- Exception Handling
- Syntax and Semantics of the Calculus
- Representing Service-Oriented Idioms
- A Sequence of Examples
- Memory Cell
- Dictionary
- Service Provider Factory
- Exceptions
- Programming a Finance Portal
- Analysis Techniques
- Further Reading and Closing Remarks
- References
- QoS Contract-Aware Reconfiguration of Component Architectures Using E-Graphs
- Introduction
- Motivation and Scope
- Running Example
- E-Graph Modeling of QoS Contracts-Based System Reconfiguration
- Extended Graphs: Base Definitions
- System Reflection
- QoS Contracts
- Component-Based Architecture Reconfiguration Modeling
- QoS Contracts-Based Reconfiguration Properties
- Component-Based Structural Compliance
- Termination and Confluence of the System Reconfiguration
- Stabilization and Exception in the Reconfiguration Process
- Related Work
- Conclusions
- References
- Monitoring Method Call Sequences Using Annotations
- Introduction
- Monitoring Component Based Systems
- Method Sequence Call Specification
- Annotations with Method Sequence Calls
- Sequenced Object Annotations.
- Sequenced Method Annotation.
- The JMSeq Framework
- JMSeq Architecture
- Program Execution Trace Model and Processing.
- Sequential Execution Annotation Repository.
- Execution Verification.
- Related Work
- Conclusion and Future Work
- References
- An Introduction to Pervasive Interface Automata
- Introduction
- Case Study
- Pervasive Interface Automata
- Composition
- Composition
- Composition Examples
- Services
- Logic for Services
- Typical Services
- Components, Environments and Services
- Service Example
- Replacement
- Replacement Example
- Comparison with Interface Automata and Session Types
- Conclusion and Future Work
- References
- A Separation Logic for OO Programs
- Introduction
- An OO Storage Model
- An OO Separation Logic
- Assertions Language
- Semantics
- Properties and Inference Rules
- Discussion
- A Simple OO Language and Its Inference Rules
- A Case Study
- Related Work and Conclusion
- References
- Model Checking Adaptive Multilevel Service Compositions
- Introduction
- The Calculus
- Non-interference
- Modal Formulae for Non-interference
- A Modal Formula for Compliance
- An Adaptive Algorithm
- Conclusion
- References
- Distributed Adaption of Dining Philosophers
- Introduction
- Dining Philosophers As-Is: Deadlock-Prone
- Dining Philosophers To-Be: No Deadlock, No Starvation
- Migration Coordination Set-Up among Helpers
- Migration Coordination Distributed among Helpers
- Discussion and Concluding Remarks
- References
- Component Service Promotion: Contracts, Mechanisms and Safety
- Introduction
- Hierarchical Composition and Service Promotion
- Simple Model and Example
- Promotion Correctness
- Changing Signatures and Predicates
- Small Classification of Service Promotion
- Provided Service Promotion
- Required Service Promotion
- N-ary Service Promotion
- Verification Methodology of Promotion Correction
- An Example in Kmelia
- Explicit Promotion Operators
- Formal Analysis of Service Promotion Correctness
- Experimental Results
- Encapsulation and Observability Rules
- Observability of Predicates
- Variable Abstraction and Promotion
- Invariant Promotion
- Consequences on the Promotion Process
- Related Work
- Conclusion
- References
- Systems-Theoretic View of Component-Based Software Development
- Introduction
- A Running Example: Composition and Control of BPEL Processes
- The Implementation and Control Parts - Introduction to the Supervisory Control Theory
- The Interface Part - The Hierarchical Control Variant
- Composition of Components
- Horizontal Aggregation without Additional Control
- Vertical Aggregation without Additional Control
- Superposition of Control
- Conclusion
- References
- Aspect Weaving in UML Activity Diagrams: A Semantic and Algorithmic Framework
- Introduction
- Syntax
- Activity Diagram Syntax
- Aspect Syntax
- Matching and Weaving Semantics
- Matching Semantics
- Weaving Semantics
- Completeness and Correctness of the Weaving
- Design and Implementation
- Aspect Specialization
- Matching
- Weaving
- Case Study: Adding Authorization to SIP-Communicator
- Related Work
- Conclusion and Future Work
- References
- Using Temporal Logic for Dynamic Reconfigurations of Components
- Introduction
- Motivating Example
- Architectural (Re-)Configuration Model
- Component-Based Architectures
- Dynamicity of Component Architectures
- Temporal Logic for Dynamic Reconfigurations
- Syntax of the Logic
- Semantics of FTPL
- Application to the HTTP Server Example
- On the Expressiveness of FTPL
- Application to the Fractal Component Model
- Overview of Fractal, FPath and FScript
- From the FTPL Model to Fractal
- Dynamic Verification
- Conclusion
- References
- Modular Termination Analysis of Java Bytecodeand Its Application to phoneME Core Libraries
- Introduction
- Non-modular Termination Analysis in costa
- From the Bytecode to the Rule-Based Representation
- Context-Sensitive (Pre-)Analyses to Improve Accuracy
- Size Analysis of Java Bytecode
- Inferring Termination
- Abstract Interpretation Fundamentals
- Extending costa to Modular Termination Analysis
- Modular Bottom-Up Analysis
- Application of Modular Analysis to phoneME Libraries
- Some Further Improvements to costa
- An Example of Modular Analysis of phoneME Libraries
- Contracts for Method Overriding
- Experiments
- Discussion
- References
- Decomposition of Constraint Automata
- Introduction
- Reo: A Coordination Language
- Constraint Automata: Compositional Semantics of Reo
- Product of Constraint Automata with State Memory
- Complete Constraint Automata
- Inverse of Complete Constraint Automata
- Product of Two Complete Constraint Automata
- Decomposition Example
- Related Work
- Conclusion and Future Work
- References
- Graph Representation of Sessions and Pipelines for Structured Service Programming
- Introduction
- The Calculus CaSPiS
- Operational Semantics in Terms of Reduction
- Algebra of Hierarchical Graphs
- Graph Grammar
- Interpretation of Graph Terms by Hypergraphs
- Graph Transformation Rules
- Graph Representation of CaSPiS
- Processes as Designs
- Tagged Graphs of Processes
- Graph Transformation Rules for Congruence
- Graph Transformation Rules for Reduction
- An Example
- Conclusion
- References
- Will the Real Service Oriented Computing Please Stand Up?
- Introduction
- The Buzz
- Software Engineering
- Service Oriented Computing
- Challenges of SOC
- Vote
- Performance Verification in Complex Enterprise-Level Component Systems
- Introduction
- Output- and Input-Compatibility for TIOA and Their Verification
- Services in Component Behaviour
- Conclusion and Future Work
- References
- Runtime Programming through Model-Preserving, Scalable Runtime Patches
- Introduction
- Runtime Programming through Runtime Patches
- Model Preservation
- Scalability
- Ongoing Work
- References
- Steps on the Road to Component Evolvability
- References
- Towards Linear Algebras of Components
- Introduction
- Linear Algebras of Machines
- Typed Matrices for Blockwise Abstraction
- Postlude
- References
- Author Index
