Fundamentals of Software Engineering: Third IPM International Conference, FSEN 2009, Kish Island, Iran, April 15-17, 2009, Revised Selected Papers (Lecture ... / Programming and Software Engineering)

This book constitutes the thoroughly refereed post-conference proceedings of the Third International Conference on Fundamentals of Software Engineering, FSEN 2009, held in Kish Island, Iran, in April 2009. The 22 revised full papers and 5 revised short papers presented together with 3 invited lectures were carefully reviewed and selected from 88 submissions. The topics include models of programs and systems, software specification, validation and verification, software architectures and their description languages, object and multi-agent systems, coordination and feature interaction, integration of formal and informal methods, integration of different formal methods, component-based development, service-oriented development, model checking and theorem proving, software and hardware verification and CASE tools and tool integration. 3642116221......Page 1 Lecture Notes in Computer Science 5961......Page 2 Fundamentals of Software Engineering......Page 3 Preface......Page 5 Table of Contents......Page 10 Introduction......Page 13 Process Theory......Page 15 Regular Processes......Page 20 Pushdown and Context-Free Processes......Page 25 Computable Processes......Page 39 References......Page 44 Introduction......Page 46 Syntax and Semantics......Page 47 Reachability......Page 49 Regions......Page 52 Behavioural Refinement Relations......Page 53 Language Inclusion and Equivalence......Page 56 Zones and Difference-Bound Matrices......Page 58 Weighted Timed Automata......Page 61 Optimal Reachability......Page 62 Multi-weighted Timed Automata......Page 63 Optimal Infinite Runs......Page 64 Timed Games......Page 67 References......Page 69 Introduction......Page 74 Natural Path to CB-MDD......Page 75 Theoretical and Tool Support to Successful CB-MDD......Page 76 Theoretical Foundation of rCOS......Page 79 Component Implementation and Component Refinement......Page 80 Contracts......Page 81 Publications......Page 82 Composition......Page 84 Tool Support to Requirement Analysis......Page 85 Model Transformation Tool to Support Design......Page 87 Concluding Remarks......Page 89 References......Page 90 Introduction......Page 93 The Calculus......Page 95 A Type System to Ensure Termination in HOpi2......Page 96 An Analysis of the Type System for HOpi2......Page 98 HOPi: Transmitting Higher-Order Functions......Page 102 Controlling Communication and Passivation......Page 104 References......Page 108 Introduction......Page 109 The S-Calculus and Its Operational Semantics......Page 111 Asymmetric Session Types......Page 114 Compliance up to Deadlock......Page 117 Delegation via Higher-Order Sessions......Page 119 Related Work and Conclusion......Page 122 References......Page 123 Introduction......Page 125 Restricted Broadcast Process Theory......Page 126 Computed Network Theory......Page 127 Operational Semantics of CNT......Page 128 Computed Network Bisimulation......Page 130 CNT Axiomatization......Page 131 Conclusion......Page 134 Branching Computed Network Bisimilarity Is an Equivalence......Page 135 Rooted Branching Computed Network Bisimilarity Is a Congruence......Page 138 Introduction......Page 141 Preliminaries......Page 142 Notions and Concepts Related to UCs......Page 143 Unsatisfiable Cores via Parse Trees......Page 144 Basic Form......Page 145 Variants......Page 147 Comparison with Separated Normal Form......Page 148 Unsatisfiable Cores via Bounded Model Checking......Page 149 Unsatisfiable Cores via Tableaux......Page 150 Related Work......Page 152 Conclusion......Page 154 References......Page 155 Introduction......Page 158 Preliminaries......Page 159 Determinism......Page 161 Examples......Page 164 Format......Page 167 Relaxing the Restrictions......Page 168 Predicates......Page 169 Examples......Page 170 Conclusions......Page 171 References......Page 172 Introduction......Page 174 The Randomized Sabotage Game......Page 176 The l-Edge Construction......Page 178 Existential, Universal, and Verification Gadgets......Page 179 The Parametrization Gadget......Page 182 Towards the PSPACE-Hardness for Arbitrary Probabilities......Page 184 On the Distribution and Computation of the Probabilities pk,n......Page 185 Perspectives......Page 187 References......Page 188 Introduction......Page 190 PT-Nets......Page 193 Coverability Tree......Page 195 Coverability Tree and Step Semantics......Page 196 Weak Monotonicity and Component-Based Systems......Page 199 Concluding Remarks......Page 204 References......Page 205 Introduction......Page 206 PCF with Jumps......Page 209 The Logic......Page 210 Axioms and Rules......Page 212 Simplifying Reasoning......Page 219 Conclusion......Page 221 References......Page 222 Introduction......Page 224 Preliminaries......Page 226 The Modular Schedulability Analysis Framework......Page 227 Real-Time Creol......Page 230 The Translation Algorithm......Page 232 Schedulability Analysis of Creol......Page 236 Checking Compatibility......Page 237 Conclusions and Future Work......Page 238 References......Page 239 Introduction......Page 240 The Calculus......Page 242 The Operational Semantics......Page 244 Well-Formedness......Page 247 Observational Semantics......Page 249 Bisimulation Proof Methods......Page 251 Future and Related Work......Page 253 References......Page 254 Introduction......Page 256 The Modelling Language......Page 257 Duration Calculus and Linear Duration Invariants......Page 258 Duration of a Location Vector sj......Page 259 Transformation of the Network of Automata......Page 260 Construction of the Auxiliary Automaton S......Page 261 Case Study......Page 267 Conclusion......Page 268 References......Page 270 Introduction......Page 272 Reo Connectors......Page 274 Büchi Automata of Records......Page 275 Record-Based Linear-Time Temporal Logic......Page 278 Some Useful Encodings......Page 279 Specifying Reo Connectors......Page 280 From Formulas to Automata: Model Checking......Page 281 On-the-Fly Model Checking......Page 282 Conclusion......Page 284 The Algorithm......Page 286 Introduction......Page 288 Basic Notions: Refinement Settings and Expressiveness......Page 289 A Wide Collection of Refinement Settings......Page 292 Comparison......Page 294 Related Work......Page 301 References......Page 302 Introduction......Page 304 LTL Model Checking......Page 306 Reinforcement Learning and Monte Carlo Policy......Page 307 Quantitative Model Checking......Page 308 Applying Reinforcement Learning......Page 309 Providing a Measure of Correctness......Page 311 Experimental Results......Page 312 Related Works......Page 315 Conclusion and Future Works......Page 316 References......Page 317 Proof of Correctness......Page 318 Introduction......Page 320 ToolBus and Tscript......Page 323 The Auction Example......Page 324 From Tscript to mCRL2......Page 325 Analysis of the Auction System......Page 327 Conclusions and Future Work......Page 333 References......Page 334 Introduction......Page 336 Syntax......Page 338 Operational Semantics......Page 340 A Behavioral Interface Specification Language......Page 342 Well-Formedness......Page 343 Observational Blur......Page 344 Scheduling and Asynchronous Testing of Creol Objects......Page 345 Implementing a Specification-Driven Creol Interpreter......Page 347 Conclusion......Page 348 References......Page 350 Introduction......Page 352 Component Model......Page 353 Strategy Refinement......Page 354 Stability......Page 357 Strategy Mapping......Page 362 Application: Distributed Algorithms......Page 363 Conclusion......Page 365 References......Page 366 Introduction......Page 367 Related Work......Page 368 Notation......Page 369 The Java Virtual Machine Model......Page 370 Non-interference......Page 372 Intra-Method Abstract Dependency......Page 373 Relations between Abstract and Concrete Worlds......Page 376 Analysis Correctness......Page 377 Inter-method Analysis......Page 378 Secure Information Flow......Page 380 References......Page 381 Introduction......Page 383 UML State Machines......Page 384 Syntax......Page 385 Operational Semantics......Page 387 Refinement and Simulation......Page 390 Refinement Patterns......Page 391 Conclusions, Related Work, and Future Work......Page 396 References......Page 397 Introduction......Page 399 Separation of Concerns......Page 401 Example......Page 402 Integrated Specification......Page 403 Verification......Page 405 Conclusion......Page 411 References......Page 412 Introduction......Page 414 Roles and Relationships......Page 416 Roles in powerJava......Page 417 Relationship as Attribute with Roles Pattern......Page 418 Relationship Object Pattern......Page 421 Abstract Roles and Relationships......Page 422 References......Page 427 Introduction......Page 428 A Modal Language......Page 430 A Language for M-Interactors......Page 432 Composing Interactors......Page 433 Elementary Connectors......Page 435 New Connectors from Old......Page 436 Configurations of M-Interactors......Page 439 Conclusions and Future Work......Page 440 References......Page 441 Introduction......Page 443 Synchronizing Model and Software Artifacts......Page 444 Data Model, Version Model......Page 445 Relationship Evolution Control......Page 446 Definition and Support of Consistency Constraints......Page 447 Conclusion......Page 449 References......Page 450 Introduction......Page 451 The Deployment and Its Management Description in ``3DxSOADL"......Page 452 Distributed Repository Schema......Page 453 Distributed SOA Structure Schema......Page 455 Dynamic Distributed Deployment Schema......Page 456 Conclusion......Page 457 References......Page 458 Introduction......Page 459 Sequence Charts......Page 460 Policy Sequence Charts......Page 461 Compliance of a Connector with Its Security Policy......Page 463 Conclusion and Future Work......Page 465 References......Page 466 Introduction......Page 467 From FDJ to FSJ: The Translation Algorithm......Page 469 Conclusions and Related Work......Page 473 References......Page 474 Introduction......Page 475 A Semantical Foundation for Modeling Functionality......Page 476 Hierarchical Structuring of Services......Page 479 References......Page 482 Author Index......Page 483 The present volume contains the proceedings of the Third IPM International Conference on Fundamentals of Software Engineering (FSEN), Kish, Iran, April 15–17, 2009. FSEN 2009 was organized by the School of Computer Science at the Institute for Studies in Fundamental Sciences (IPM) in Iran, in cooperation with the ACM SIGSOFT and IFIP WG 2.2. This conference brought together around 100 researchers and practitioners working on di?erent aspects of formal methods in software engineering from 15 di?erentcountries.ThetopicsofinterestinFSENspanoverallaspects offormal methods,especiallythoserelatedtoadvancingtheapplicationofformalmethods in software industry and promoting their integration with practical engineering techniques. The Program Committee of FSEN 2009 consisted of top researchers from 24 di?erent academic institutes in 11 countries. We received a total of 88 submissions from 25 countries out of which the Program Committee selected 22 as regular papers, 5 as short papers, and 7 as poster presentations in the conferenceprogram.Eachsubmissionwasreviewedbyatleastthreeindependent referees, for its quality, originality, contribution, clarity of presentation, and its relevance to the conference topics. This volume contains the revised versions of the regular and short papers presented at FSEN 2009. Three distinguished keynote speakers delivered their lectures at FSEN 2009 on models of computation: automata and processes (Jos Baeten), veri?cation, performanceanalysisandcontrollersynthesisforreal-timesystems(KimLarsen), and theory and tool for component-based model-driven development in rCOS (Zhiming Liu). Our invited speakers also contributed to this volume by s- mitting their keynote papers, which were accepted after they were reviewed by independent referees.