Formal Methods for Embedded Distributed Systems: How to Master the Complexity

ISBN-13: 9781441954596 / Angielski / Miękka / 2010 / 263 str.

Fabrice Kordon; Michel Lemoine

Opis

The development of any Software (Industrial) Intensive System, e.g. critical embedded software, requires both different notations, and a strong devel- ment process. Different notations are mandatory because different aspects of the Software System have to be tackled. A strong development process is mandatory as well because without a strong organization we cannot warrantee the system will meet its requirements. Unfortunately, much more is needed The different notations that can be used must all possess at least one property: formality. The development process must also have important properties: a exha- tive coverage of the development phases, and a set of well integrated support tools. In Computer Science it is now widely accepted that only formal notations can guarantee a perfect de?ned meaning. This becomes a more and more important issue since software systems tend to be distributed in large systems (for instance in safe public transportation systems), and in small ones (for instance numerous processors in luxury cars). Distribution increases the complexity of embedded software while safety criteria get harder to be met. On the other hand, during the past decade Software Engineering techniques have been improved a lot, and are now currently used to conduct systematic and rigorous development of large software systems. UML has become the de facto standard notation for documenting Software Engineering projects. UML is supported by many CASE tools that offer graphical means for the UML notation.

Spis treści

Preface Contributing Authors Introduction; F. Kordon, M. Lemoine 1. The 'Traditional' development approach 2. What is covered in this book 3. Organization of chapters Part I: The BART Case Study 1: The BART Case Study; V. Winter, F. Kordon, M. Lemoine 1. Introduction 2. Objective 3. General Background on the BART Train System 4. Informal Specification for the AATC System 5. Inputs and Outputs to the Control Algorithm 6. Physical Performance of the Train in Response to Commands 7. Worst Case Stopping Profile 8. Considerations with Acceleration and Speed Commands 9. Quantitative Quality and Safety Metrics to be Demonstrated 10. Vital Station Computer (VSC) Issues 11. Miscellaneous Questions and Answers Part II: Building and Validating Conceptual Aspects 2: Formal Specification and Refinement of a Safe Train Control Function; V. Winter, D. Kapur, G. Fuehrer 1. Introduction 2. Technical approach and method 3. Inputs taken from the BART case study 4. Applying the approach to the case study 5. Results raised by this technique 6. Conclusion 7. Appendixes 3: From UML to Z; M. Lemoine, G. Gaudière 1. Introduction 2. Technical approach and method 3. Our approach in details 4. Inputs taken from the BART case study 5. Applying the approach to the case study 6. Results raised by this technique 7. Conclusion 4: Environmental Modeling with UML; Adriaan de Groot, Jozef Hooman 1. Introduction 2. Technical approach and method 3. Applying our approach to the case study 4. Designing a Controller 5. Results raised by this technique 6. Conclusion Part III: Building and Validating Operational Aspects 5: Checking BART Test Scenarios with UML’s Object Constraint Language; M. Gogolla, P. Ziemann 1. Introduction 2. Technical approach and method 3. Inputs taken from the BARTcase study 4. Applying the approach to the case study 5. Results raised by this technique 6. Conclusion 6: Modeling and verifying behavioral aspects; F. Bréant, J. -M. Couvreur, F. Gilliers, F. Kordon, I. Mounier, E. Paviot-Adet, D. Poitrenaud, D. Regep, G. Sutre 1. Introduction 2. Technical approach and method 3. Inputs taken from the DART case study 4. Applying the approach to the case study 5. State space computation using DDD 6. Conclusion Part IV: Methodological Aspects 7: AutoFocus - Mastering the Complexity; B. Schätz 1. Introduction 2. Technical Approach and Method 3. Inputs taken from the BART case study 4. Applying the approach to the case study 5. Results raised by this technique 6. Conclusion 8: Conclusions; F. Kordon, M. Lemoine 1. Are Formal Methods an appropriate answer to the Design of Distributed Systems? 2. A process for the Design of Safety Critical Distributed Systems