Formal Methods for Embedded Distributed Systems How to master the co
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
- PDF / 2,225,070 Bytes
- 275 Pages / 432 x 684 pts Page_size
- 4 Downloads / 167 Views
Formal Methods for Embedded Distributed Systems How to master the complexity Edited by
Fabrice Kordon Université P. & M. Curie, France and
Michel Lemoine ONERA Centre de Toulouse, France
KLUWER ACADEMIC PUBLISHERS NEW YORK, BOSTON, DORDRECHT, LONDON, MOSCOW
eBook ISBN: Print ISBN:
1-4020-7997-4 1-4020-7996-6
©2004 Springer Science + Business Media, Inc. Print ©2004 Kluwer Academic Publishers Dordrecht All rights reserved No part of this eBook may be reproduced or transmitted in any form or by any means, electronic, mechanical, recording, or otherwise, without written consent from the Publisher Created in the United States of America
Visit Springer's eBookstore at: and the Springer Global Website Online at:
http://www.ebooks.kluweronline.com http://www.springeronline.com
Contents
Preface
ix
Contributing Authors
xi
Introduction F. Kordon, M. Lemoine 1 The “Traditional” development approach 2 What is covered in this book 3 Organization of chapters
xvii xvii xviii xviii
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
3 3 3 4 5 8 10 11 16 17 18 19
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
v
25 25 28 38 42 56 57
vi
FORMAL METHODS FOR EMBEDDED DISTRIBUTED SYSTEMS 7
Appendixes
3 From UML to Z M. Lemoine, G. Gaudi`ere 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
60 65 65 67 72 80 81 86 87 89 89 92 102 116 127 127
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 BART case study 4 Applying the approach to the case study 5 Results raised by this technique 6 Conclusion
133 133 135 147 149 166 169
6 171 Modeling and verifying behavioral aspects F. Br´eant, J.-M. Couvreur, F. Gilliers, F. Kordon, I. Mounier, E. Paviot-Adet, D. Poitrenaud, D. Regep, G. Sutre 1 Introduction 171 2 Technical approach and method
Data Loading...
