Formal Aspects of Component Software

Name: Formal Aspects of Component Software | 7th International Workshop, FACS 2010, Guimarães, Portugal, October 14-16, 2010, Revised Selected Papers
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

7th International Workshop, FACS 2010, Guimarães, Portugal, October 14-16, 2010, Revised Selected Papers

Luis Soares Barbosa Markus Lumpe(Herausgeber*in)

Springer (Verlag)

Erschienen am 19. Januar 2012

X, 305 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-27269-1 (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 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

Systemvoraussetzungen

Als PDF speichern Als Link merken