Construction and analysis of transition systems with MEC [electronic resource] / Andre Arnold, Didier Begay, Paul Crubille.

Includes bibliographical references (p. 187-189) and index.

1. Introduction -- pt. I. Theoretical foundations. 2. The model. 2.1. Transition systems. 2.2. Synchronization systems -- 3. Properties. 3.1. Elementary computations. 3.2. The definition of new operators. 3.3. Loops and fairness -- 4. Algorithms. 4.1. Computation of least fixpoints. 4.2. Tarjan's algorithm for loops -- pt. II. Some examples. 5. First contact. 5.1. General outline. 5.2. Ergonomics. 5.3. MEC computations. 5.4. Annotated session -- 6. A solitaire game -- 7. A can filling system. 7.1. The example. 7.2. Verification -- 8. Verification of a control system. 8.1. The description of the control unit by a statechart. 8.2. From a statechart to a synchronization system. 8.3. Verification of the six properties -- 9. Atomic readings and writings. 9.1. Regular and atomic variables. 9.2. Modeling the algorithm. 9.3. Verification with observers. 9.4. Verification with fixpoint functions -- 10. A call processing system. 10.1. Modeling the system. 10.2. Discovering forgotten transitions -- 11. An electronic mail system. 11.1. From CCS to labeled transitions systems. 11.2. Verification with MEC -- 12. The 'transit node' case study. 12.1. The model. 12.2. Validation of the model. 12.3. Another version -- pt. III. Principles of implementation. 13. Architecture of MEC software. 13.1. The 'transition and synchronization systems' module. 13.2. The 'algorithms' module. 13.3. The 'interpreter' module -- 14. MEC reference manual. 14.1. Presentation. 14.2. Memory management. 14.3. Interface. 14.4. Commands. 14.5. Files.

The importance of formal methods in software engineering has been receiving greater acknowledgement. These methods can be used at several stages of the software development process. This book focuses on a method concerning the early stages of design, namely the modeling of a system at conceptual level, and the verification and validation of this model. The mathematical formalism used for modeling and verifying systems is the synchronized product of transition systems. The book introduces this notion and presents several examples of modeling and verification covering various domains: games, industrial processes, communication protocols, etc. These examples are worked out using the "MEC" software tool. This book is also intended to be an introduction to this tool which is described in full detail.

Electronic reproduction. Singapore : World Scientific Publishing Co., 1994. System requirements: Adobe Acrobat Reader. Mode of access: World Wide Web.