Modern Formal Methods And Applications

MODERN FORMAL METHODS AND APPLICATIONS Modern Formal Methods and Applications Edited by HOSSAM A. GABBAR Okayama University, Okayama, Japan A C.I.P. Catalogue record for this book is available from the Library of Congress. ISBN-10 ISBN-13 ISBN-10 ISBN-13 1-4020-4222-1 (HB) 978-1-4020-4222-5 (HB) 1-4020-4223-X (e-book) 978-1-4020-4223-2 (e-book) Published by Springer, P.O. Box 17, 3300 AA Dordrecht, The Netherlands. www.springer.com Printed on acid-free paper All Rights Reserved © 2006 Springer No part of this work may be reproduced, stored in a retrieval system, or transmitted in any form or by any means, electronic, mechanical, photocopying, microfilming, recording or otherwise, without written permission from the Publisher, with the exception of any material supplied specifically for the purpose of being entered and executed on a computer system, for exclusive use by the purchaser of the work. Printed in the Netherlands. Table of Contents PREFACE xi ABOUT THE EDITOR xiii ABOUT THE AUTHORS xv LIST OF FIGURES xix LIST OF TABLES xxiii 1 FUNDAMENTALS OF FORMAL METHODS 1.1 Overview 1.2 Logic 1.2.1 Predicates 1.2.2 Function signs 1.2.3 Elementary logic 1.3 Argument & Proofs 1.4 Automata Theory 1.4.1 Deterministic finite state machine or deterministic finite automaton (DFA) 1.4.2. Nondeterministic finite state machine or nondeterministic finite automaton (NFA) 1.4.3. Quick Facts about: Nondeterministic Finite Automata, with transitions (FND- or -NFA) v 1 1 4 8 9 9 9 10 10 11 12 vi Table of Contents 1.5 Algorithms 1.5.1 Algorithm design 1.5.2 Problem solving 1.6 Logic Programming 1.6.1 Example 1.6.2 Dynamic typing 1.6.3 Unification 1.7 Formal Languages 1.7.1 Formal language anatomy 1.7.2 Object language versus meta-language 1.7.3 Formal language examples 1.8 Conclusion 1.9 References 12 12 14 14 16 16 16 17 17 17 18 20 20 2 FORMAL METHODS FOR PROCESS SYSTEMS ENGINEERING 21 2.1 2.2 2.3 2.4 2.5 2.6 2.7 2.8 2.9 Introduction Process Systems Engineering Why Formal Language? Operation Engineering SOP synthesis 2.5.1 SOP structure 2.5.2 Tokens 2.5.3 Domain knowledge 2.5.4 Formulas 2.5.5 Synthesis of meta-operation 2.5.6 Examples of meta-operation 2.5.7 Isolation 2.5.8 Cleaning 2.5.9 Heating 2.5.10 Recovery Meta-Operation for Master Recipe Control Recipe Generation Conclusion References 3 FORMAL METHODS FOR PRODUCTION CHAIN MANAGEMENT 3.1 Introduction 3.2 Production Chain Operation Framework 21 22 23 25 25 25 26 27 28 29 29 29 30 30 31 31 32 33 34 37 37 38 Table of Contents 3.3 3.4 3.5 3.6 3.2.1 Unit operation knowledge model Formal Representation of OM Case Study Production Chain Conclusions References 4 FORMALIZING WASTE MANAGEMENT 4.1 4.2 4.3 4.4 Introduction The Formal Method PSSP Ontology The Universal Properties 4.4.1 Purpose 4.4.2 Structure 4.4.3 State 4.4.4 Performance 4.5 Central Objects 4.5.1 Event 4.5.2 Medium 4.5.3 Event-medium composite 4.5.4 Process 4.5.5 Product 4.6 Application to Waste Management 4.6.1 What is waste? 4.6.2 Traditional view 4.6.3 Waste as PSSP object 4.7 What Is Waste Management? 4.7.1 Traditional view 4.7.2 Waste management in PSSP format 4.8 A Case 4.9 Discussion 4.10 Acknowledgement 4.11 References vii 39 43 44 45 45 47 47 48 49 50 50 51 52 53 54 54 56 57 61 63 63 63 63 65 72 72 72 76 80 81 81 5 FORMAL METHODS FOR MODELING BIOLOGICAL REGULATORY NETWORKS 83 5.1 Introduction 5.2 Qualitative Dynamics of Biological Regulatory Networks 5.2.1 Biological regulatory graphs 5.2.2 Models of biological regulatory graphs 5.2.3 Dynamics of models 83 86 87 89 91 v