文档介绍：Modeling and Verification
Using UML Statecharts
Modeling and Verification
Using UML Statecharts
A Working Guide to Reactive System
Design, Runtime Monitoring and
Execution-Based Model Checking
Doron Drusinsky
AMSTERDAM • BOSTON • HEIDELBERG • LONDON
NEW YORK • OXFORD • PARIS • SAN DIEGO
SAN FRANCISCO • SINGAPORE • SYDNEY • TOKYO
Newnes is an imprint of Elsevier
Newnes is an imprint of Elsevier
30 Corporate Drive, Suite 400, Burlington, MA 01803, USA
Linacre House, Jordan Hill, Oxford OX2 8DP, UK
Copyright © 2006, Elsevier Inc. All rights reserved.
No part of this publication may be reproduced, stored in a retrieval system, or transmitted in
any form or by any means, electronic, mechanical, photocopying, recording, or otherwise,
without the prior written permission of the publisher.
Permissions may be sought directly from Elsevier’s Science & Technology Rights
Department in Oxford, UK: phone: (+44) 1865 843830, fax: (+44) 1865 853333, e-mail:
******@.uk. You may plete your request online via the Elsevier
homepage (), by selecting “Customer Support” and then “Obtain-
ing Permissions.”
Recognizing the importance of preserving what has been written,
Elsevier prints its books on acid-free paper whenever possible.
Library of Congress Cataloging-in-Publication Data
Drusinsky, Doron.
Modeling and verification using UML statecharts : a working guide to reactive system
design, runtime monitoring, and execution-based model checking / Doron Drusinsky.
p. cm.
ISBN 0-7506-7949-2 (pbk. : alk. paper) 1. UML (Computer science) 2. Formal methods
(Computer science) 3. Computer software--Development. I. Title.
2006
’17--dc22
2006005265
British Library Cataloguing-in-Publication Data
A catalogue record for this book is available from the British Library.
ISBN-13: 978-0-7506-7949-7
ISBN 0-7506-7949-2
For information on all Newnes publications,
visit our website at .
06 07 08 09 10 10 9 8