All modern industries rely on large and complex software systems. In order to construct such large systems in a systematic manner, the focus of the development methodologies has switched in the last two decades from functional to structural issues. Formal methods have been applied successfully to the verification of medium-sized programs in protocol and hardware design. However, their application to the development of large systems requires a greater emphasis on specification, modeling, and validation techniques supporting the concepts of reusability and modifiability, and their implementation in new extensions of existing programming languages like Java. This state-of-the-art survey presents the outcome of the 7th Symposium on Formal Methods for Components and Objects, held in Sophia Antipolis, France, in October 2008. The volume contains 14 revised contributions submitted after the symposium by speakers from each of the following European IST projects: the IST-FP7 project COMPAS on compliance-driven models, languages, and architectures for services; the IST-FP6 project CREDO on modelling and analysis of evolutionary structures for distributed services; the IST-FP7 DEPLOY on industrial deployment of advanced system engineering methods for high productivity and dependability; the IST-FP6 project GridComp on grid programming with components; and the IST-FP6 project MOBIUS aiming at developing the technology for establishing trust and security for the next generation of global computers, using the proof carrying code paradigm.
Author(s): Frank S. de Boer, Marcello M. Bonsangue, Eric Madelaine
Edition: 1
Publisher: Springer
Year: 2009
Language: English
Pages: 309
front-matter......Page 1
Introduction......Page 9
Repository, Metadata Repository, and Model Repository......Page 10
Reusable Architectural Decision Models......Page 11
Architectural Decisions......Page 12
Architectural Decision: Select Basic Repository Technology......Page 13
Architectural Decision: Select XML to NXD Mapping......Page 14
Architectural Decision: Select XML to File Mapping......Page 15
Architectural Decision: Select Repository Type......Page 16
Architectural Decision: Select Support for Metamodel......Page 17
Architectural Decision: Select Modeling Levels Stored in the Repository......Page 18
Architectural Decision: Select Metadata Types......Page 19
Architectural Decision: Select Security Metadata Types......Page 21
Architectural Decision: Select Association Model......Page 22
Case Study......Page 23
Related Work......Page 25
Conclusion and Outlook......Page 26
Introduction......Page 29
Business Process Modeling......Page 31
Process Modeling with Eclipse Coordination Tools......Page 32
Formal Behavioral Model for Service Composition: Extended Constrained Automata......Page 35
Verifying Business Process Specification......Page 38
Compliance-Aware Process Modeling by Examples......Page 40
Related Work......Page 45
Conclusions and Future Work......Page 46
Introduction......Page 50
Modelling Distributed Concurrent Objects in Creol......Page 51
Syntax......Page 52
Denotational Semantics......Page 53
CreolRT: Extending Creol with Real-Time Constraints......Page 58
Modelling Biomedical Sensor Nodes in Creol_{RT}......Page 61
Discussion......Page 65
Introduction......Page 69
Overview: The Testing Approach......Page 70
Finding Test Cases with Dynamic Symbolic Execution......Page 71
Conformance Testing Using Recorded Event Traces......Page 72
Creol......Page 73
Representation of a Run......Page 74
The ASK Case Study......Page 75
Test Case Generation......Page 78
Dynamic Symbolic Execution in the Parallel Setting......Page 79
The ASK Case Study Revisited......Page 80
Generating the Test Driver......Page 84
Related Work......Page 87
Conclusions......Page 88
Introduction......Page 90
Constraint Automata......Page 92
Linear-Time Properties......Page 96
Branching and Alternating-Time Properties......Page 100
Bisimulation Equivalence for Constraint Automata......Page 106
Results, Conclusion and Future Work......Page 108
Introduction......Page 110
Concepts Used in This Paper......Page 111
Definition of Context and Context Related Matters......Page 112
The Action System Formalism at a Glimpse......Page 113
Action System at a Glimpse......Page 114
Action Systems for Modelling Context......Page 116
Integrating Contextual Information to an Application......Page 119
Composing Information from Elementary Contexts......Page 121
Processing Context......Page 122
Conclusions......Page 123
References......Page 124
Introduction and Motivation......Page 127
Study of the Existing { c DeCCo} System......Page 129
Description of the Subset of Java Bytecode......Page 131
Stack Layout Analysis......Page 132
Formalisation of Java Bytecode Execution......Page 134
B Description of the RISC Processor......Page 136
Compiling Data Operations by Refinement......Page 138
Compiling Control Flow......Page 140
Related Work: Overview of Alternative Approaches......Page 142
Conclusion......Page 143
Introduction......Page 147
Event-B......Page 148
Machine Consistency......Page 149
Machine Refinement......Page 150
Problem Statement......Page 151
Getting Started with a Fresh Model......Page 152
Moving between Rooms......Page 154
Intermezzo on Transitive Closures......Page 156
Initialisation......Page 157
Granting Door Authorisations......Page 158
Revoking Door Authorisations......Page 161
Towards a Better Model......Page 164
References......Page 165
Introduction......Page 167
An Asynchronous Component Model......Page 168
Component Structure......Page 169
Informal Semantics......Page 171
Comparison with Some Component Models......Page 174
Structure and Notations......Page 177
Local Actions......Page 178
Semantics of the Component Model......Page 179
Tools/Middleware......Page 183
Synchronisation and Stop......Page 184
Conclusions......Page 185
Introduction......Page 188
Fractal and GCM......Page 190
A GCM Reference Implementation: GCM/ProActive......Page 192
Parameterized Networks of Synchronised Automata (pNets)......Page 194
Model Generation for Active Objects......Page 198
Model Generation for Hierarchical Components......Page 199
Hierarchical Components + Management Interfaces = Fractal......Page 200
Model Generation for GCM......Page 201
Vercors Architecture......Page 204
Building Tools Using Eclipse Meta-modelling Framework......Page 205
Graphical Diagrams for Component Architecture......Page 206
Model Generation......Page 207
Model-Checking: Engineering, Pragmatic Complexity......Page 208
Conclusion and Perspectives......Page 209
Introduction......Page 212
Addressing Functional and Non-functional Concerns......Page 213
The Grid Component Model (GCM)......Page 215
Behavioural Skeletons......Page 216
Tools to Support Reasoning about Autonomic Management......Page 218
Sample ``Semi-formal'' Usage of Orc......Page 219
Demonstrating the Validity of Autonomic Management Policy with Semi-formal Reasoning in Orc......Page 222
Modelling Autonomic Management......Page 223
Reasoning about Program Transformation Rule Correctness with Orc......Page 224
Introducing $location$ Metadata......Page 226
Exploiting $location$ Metadata......Page 227
Related Work......Page 229
Conclusions......Page 230
Introduction......Page 234
A Hardware Model and DMA Primitives......Page 236
Stream Processing and Double-Buffering......Page 238
Double Buffering in the Intermediate Language......Page 240
L1 with Multiparty Session Types......Page 241
Further Safety Analysis......Page 244
Basic Ideas......Page 246
Compilation......Page 247
Conclusion......Page 250
Introduction......Page 255
Syntax......Page 257
Semantics......Page 258
Calculus......Page 259
A Dynamic Logic with Abstraction......Page 261
Abstract Domains......Page 262
Update Weakening and Abstraction Rule......Page 263
An Invariant Rule Based on Updates......Page 264
The Proof Search Strategy......Page 265
Joining Proof Branches......Page 267
Example......Page 269
Modeling Information Flow......Page 271
Dependencies in Dynamic Logic......Page 272
Dependency Aware Rules......Page 274
Dependency Aware Abstraction......Page 275
Conclusion and Future Work......Page 277
Basic Semantics......Page 279
Semantics Enriched with Dependency Tracking......Page 280
Lemma 1: Soundness of weakenUpdate......Page 281
Lemma 2: Soundness of invariantUpdate......Page 283
Introduction......Page 286
Class-Level Specifications......Page 289
Method-Level Specifications......Page 291
Code-Level Specifications......Page 292
Representation of BML Specifications......Page 293
Binary Representation of BML......Page 294
Textual Representation of BML......Page 297
{ f JACK}......Page 298
{ f BMLLib}: A Library to Manipulate BML Specifications......Page 299
{ f Umbra}: A BML Editor......Page 300
{ f JML2BML}: A Specification Compiler from JML to BML......Page 301
{ f CCT}: A Tool for Packaging Certificates......Page 302
Conclusions and Further Work......Page 303
back-matter......Page 306
