Formal Methods for Components and Objects: Third International Symposium, FMCO 2004, Leiden, The Netherlands, November 2-5, 200

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 more emphasis on specification, modelling and validation techniques supporting the concepts of reusability and modifiability, and their implementation in new extensions of existing programming languages. This book presents revised tutorial lectures given by invited speakers at the Third International Symposium on Formal Methods for Components and Objects, FMCO 2004, held in Leiden, The Netherlands, in November 2004. The 14 revised lectures by leading researchers present a comprehensive account of the potential of formal methods applied to large and complex software systems such as component-based systems and object systems. The book provides an unique combination of ideas on software engineering and formal methods that reflect the expanding body of knowledge on modern software systems. Table of Contents Cover Formal Methods for Components and Objects, Third International Symposium, FMCO 2004, Leiden, The Netherlands, November 2 - 5, 2004, Revised Lectures ISBN-10 3540291318 ISBN-13 9783540291312 Preface Organization The Mobi-J Project The Omega Project Sponsoring Institutions Table of Contents A Theory of Predicate-Complete Test Coverage and Generation 1 Introduction 2 A Characterization of Predicate-Complete Test Coverage 3 Formalizing Abstraction 3.1 Concrete Transition Systems 3.2 Abstract Transition Systems 3.3 Predicate Abstraction 3.4 Predicate Abstraction of Programs 3.5 Example 4 Defining the Upper and Lower Bounds 4.1 Upper Bound Computation 4.2 Lower Bound Computation L 5 Example 6 Test Generation 6.1 Path Generation 6.3 Observe Test Runs 6.4 Abstraction Re.nement 7 Discussion 8 Related Work 8.1 Control-Flow Coverage Criteria 8.2 Symbolic Execution and Test Generation 8.3 Three-Valued Model Checking 9 Conclusion Acknowledgements References A Perspective on Component Refnement 1 Introduction 2 Coalgebraic Models for Software Components 2.1 Coalgebras 2.2 Components 2.3 A Component Calculus 3 Behavioural Refinemet 3.1 Component's Behaviour and Bisimulation 3.2 Refinement 4 Data Refinement 4.1 State Refinement 4.2 Shape Refinement 5 Conclusions and Further Work Acknowledgements References A Fully Abstract Semantics for UML Components 1 Introduction 1.1 Contribution of This Paper 1.2 Related Work 2 UML Classes, State-Machines and Components 2.1 Abstract State-Machines 2.2 Components 2.3 Operational Semantics 3 Testing Semantics 4 Trace Semantics 4.1 Trace Definbility 5 Trace Abstractions 6 Full Abstraction 7 Conclusion and Future Work References From (Meta) Objects to Aspects: A Java and AspectJ Point of View 1 Lessons from Object-Oriented Languages 1.1 Limitations (CONS) 1.2 Contributions (PRO) 2 The Java Class Model and Its Associated MOP 2.1 Exposing the Java Class Model 2.2 Using the Java MOP 2.3 Some Drawbacks of the Java MOP 3 AGuidedTourofAspectJ 3.1 The Join Point and Advice Models 3.2 Behavioral Crosscutting 3.3 Structural Crosscutting 4 Conclusion and Open Questions Acknowledgments References A Annex MoMo:AModalLogic for Reasoning About Mobility 1 Introduction 2 µKlaim 2.1 µKlaim Syntax 2.2 Operational Semantics 3 MoMo: A Modal Logic for Mobility 3.1 Kernel Fragment 3.2 State Properties 3.3 Temporal Properties 3.5 Mobility Properties 3.6 Syntax and Semantics of MoMo 4 ProofSystem 4.1 Sequents and Proofs 4.2 Names Handling 4.3 Proof Rules 5 Proving Properties of Mobile Systems 6 Conclusions and Future Works References Probabilistic Linda-Based Coordination Languages 1 Introduction 2 Linda 2.1 Adding Probabilities/Quantities 2.2 Data Driven Approach 2.3 Schedule Driven Approach 3 Distributed Tuple Spaces: KLAIM 3.1 A Core KLAIM Calculus 3.2 Probabilistic KLAIM 3.3 Stochastic KLAIM 4 Analysis 4.1 Probabilistic Abstract Interpretation 4.2 Analysis - Discrete Case 4.3 Analysis - Continuous Case 5 Conclusions References Games with Secure Equilibria, 1 Introduction 2 De.nitions 3 2-Player Non-zero-sum Games on Graphs 3.1 Unique Maximal Secure Equilibria 3.2 Algorithmic Characterization 4 .-Regular Objectives 5 n-Player Games 6 Conclusion References Priced Timed Automata: Algorithms and Applications 1 Introduction and Motivation 2 Priced Timed Automata 3 Optimal Scheduling 4 Modeling 4.1 Job Shop Scheduling 4.2 Task Graph Scheduling 4.3 Vehicle Routing with Time Windows 4.4 Aircraft Landing 4.5 PTA Versus MILP 4.6 Industrial Case Study: Steel Production 4.7 Industrial Case Study: Lacquer Production 5 Other Optimization Problems References rCOS: Refinement of Component and Object Systems 1 Introduction 2 Semantic Basis 2.1 Programs as Designs 2.2 Refinement of Designs 3 Object Systems 3.1 Syntax 3.2 Semantics 3.3 Evaluation of Expressions 4 Object-Oriented Refinement 4.1 Refinement of Object Systems 4.2 Structure Refinement 4.3 Laws of Structural Refinement 5 Component Systems 5.1 Introduction 5.2 Interfaces 5.3 Contracts 5.4 Component 5.5 Semantics Components 5.6 Refinement and Composition of Components 6 Conclusion 6.1 Related Work 6.2 Future Work Acknowledgments References Program Generation and Components 1 Introduction 2 Program Generation 2.1 What Is It? 2.2 What Is for? 3 Names and Software Components 4 A Core Calculus with Names: MMLN 4.2 Simpli cation 4.3 Computation 4.4 Type Safety 5 Programming Examples 6 RelatingMMLN to MetaML 6.1 MetaML2 6.2 Translation of MetaML2 into MMLN 7 RelatingMMLN to CMS 7.1 CMS 7.2 MLN 7.3 Translation of CMS into MLN 8 Conclusions and Related Work References Assertion-Based Encapsulation, Object Invariants and Simulations 1 Introduction 2 How Shared Objects and Reentrant Callbacks Violate Encapsulation 3 Reentrance and Object Invariants 4 Sharing and Object Invariants 5 Additional Aspects of the inv /own Discipline 6 Pointer Con nement and Simulation 7 Beyond Single-Object Invariants 8 Challenges for Future Work References A Dynamic Binding Strategy for Multiple Inheritance and Asynchronously Communicating Objects 1 Introduction 2 Inheritance: Reuse of Behavior and Reuse of Code 2.1 Multiple Inheritance 2.2 Naming Policies for Conflic Resolution 2.3 Virtual Binding 3 A Language for Asynchronously Communicating Objects 4 Multiple Inheritance 4.1 Qualifie Names 4.2 Virtual Binding 5 Example: Combining Authorization Policies 6 An Operational Semantics of Inheritance and Virtual Binding 6.1 System Confgurations 6.2 Concurrent Transitions 6.3 Method Calls 6.4 Virtual and Static Binding of Method Calls 6.5 Guarded Statements 6.6 Object Creation and Attribute Instantiation 7 Related Work 8 Conclusion References Observability, Connectivity, and Replay in a Sequential Calculus of Classes 1 Introduction 2 Observability and Classes 2.1 Cross-Border Instantiation and Connectivity 2.2 Di.erent Observers and Order of Events 2.3 Classes as Generators of Objects, Replay, and Determinism 3 A Single-Threaded Calculus with Classes 3.1 Operational Semantics 4 Trace Semantics and Ordering on Traces 4.1 Balance Conditions 4.2 Equivalences 5 Full Abstraction 5.1 Notion of Observation 5.2 Legal Traces 5.3 Soundness and Completeness 6 Conclusion References Timing Analysis and Timing Predictability Extended Abstract 1 Execution-Time Variability 1.1 Timing Analysis 2 CostofUncertainty 3 On the Multiplicative Nature of Uncertainty in Layered Systems 4 Towards a Rational Basis for Design Acknowledgements References Author Index