Formal Methods for Embedded Distributed Systems

PrefaceContributing AuthorsIntroduction; F. Kordon, M. Lemoine1. The 'Traditional' development approach2. What is covered in this book3. Organization of chaptersPart I: The BART Case Study1: The BART Case Study; V. Winter, F. Kordon, M. Lemoine1. Introduction2. Objective3. General Background on the BART Train System4. Informal Specification for the AATC System5. Inputs and Outputs to the Control Algorithm6. Physical Performance of the Train in Response to Commands7. Worst Case Stopping Profile8. Considerations with Acceleration and Speed Commands9. Quantitative Quality and Safety Metrics to be Demonstrated10. Vital Station Computer (VSC) Issues11. Miscellaneous Questions and AnswersPart II: Building and Validating Conceptual Aspects2: Formal Specification and Refinement of a Safe Train Control Function; V. Winter, D. Kapur, G. Fuehrer1. Introduction2. Technical approach and method3. Inputs taken from the BART case study4. Applying the approach to the case study5. Results raised by this technique6. Conclusion7. Appendixes3: From UML to Z; M. Lemoine, G. Gaudière1. Introduction2. Technical approach and method3. Our approach in details4. Inputs taken from the BART case study5. Applying the approach to the case study6. Results raised by this technique7. Conclusion4: Environmental Modeling with UML; Adriaan de Groot, Jozef Hooman1. Introduction2. Technical approach and method3. Applying our approach to the case study4. Designing a Controller5. Results raised by this technique6. ConclusionPart III: Building and Validating Operational Aspects5: Checking BART Test Scenarios with UML's Object Constraint Language; M. Gogolla, P. Ziemann1. Introduction2. Technical approach and method3. Inputs taken from the BARTcase study4. Applying the approach to the case study5. Results raised by this technique6. Conclusion6: 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. Sutre1.