دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
دسته بندی: کامپیوتر ویرایش: 1 نویسندگان: Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, Willem-Paul de Roever سری: ISBN (شابک) : 3540291318, 9783540291312 ناشر: Springer سال نشر: 2005 تعداد صفحات: 334 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 4 مگابایت
در صورت تبدیل فایل کتاب Formal Methods for Components and Objects: Third International Symposium, FMCO 2004, Leiden, The Netherlands, November 2-5, 2004, Revised Lectures ... / Programming and Software Engineering) به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب روشهای رسمی برای مؤلفه ها و اشیاء: سومین سمپوزیوم بین المللی ، FMCO 2004 ، لیدن ، هلند ، 2-5 نوامبر 2004 ، سخنرانی های تجدید نظر شده ... / برنامه نویسی و مهندسی نرم افزار) نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
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
Front Matter....Pages -
A Theory of Predicate-Complete Test Coverage and Generation....Pages 1-22
A Perspective on Component Refinement....Pages 23-48
A Fully Abstract Semantics for UML Components....Pages 49-69
From (Meta) Objects to Aspects: A Java and AspectJ Point of View....Pages 70-94
MoMo : A Modal Logic for Reasoning About Mobility....Pages 95-119
Probabilistic Linda-Based Coordination Languages....Pages 120-140
Games with Secure Equilibria , ....Pages 141-161
Priced Timed Automata: Algorithms and Applications....Pages 162-182
r COS : Refinement of Component and Object Systems....Pages 183-221
Program Generation and Components....Pages 222-250
Assertion-Based Encapsulation, Object Invariants and Simulations....Pages 251-273
A Dynamic Binding Strategy for Multiple Inheritance and Asynchronously Communicating Objects....Pages 274-295
Observability, Connectivity, and Replay in a Sequential Calculus of Classes....Pages 296-316
Timing Analysis and Timing Predictability....Pages 317-323
Back Matter....Pages -