Operational Semantics for Timed Systems(定时系统的操作语义学：定时与混合系统的统一建模的非标准方法)

This monograph is dedicated to a novel approach for uniform modeling of timed and hybrid systems. The author introduces a time model that allows for both the description of discrete time steps and continuous processes with a discrete time model with infinitesimal step widths.
The underlying mathematical structure of this time model is based on the concepts of non-standard analysis. The discrete modeling, i.e., the description of sequential discrete algorithms at different abstraction levels, is done using the abstract state machines formalism.
The presentation is well balanced between theoretical elaboration and critical discussion of the applicability of the theoretical results by means of appropriate case studies. The new temporal semantics proposed helps theoreticians as well as practitioners in gaining a better understanding of time models and in building better notations, models, and tools for the formal treatment of systems where time matters.

The LNCS series reports state-of-the-art results in computer science research，development，and education，at a high level and in both printed and electronic form. Enjoying tight cooperation with the R&D community，with numerous individuals，as well as with prestigious organizations and societies，LNCS has grown into the most comprehensive computer science research forum available.
The scope of LNCS，including its subseries LNAI，spans the whole range of computer science and information technology including interdisciplinary topics in a variety of application fields. The type of material published traditionally includes.
—proceedings （published in time for the respective conference）
—post-proceedings （consisting of thoroughly revised final full papers）
—research monographs（which may be based on outstanding PhD work，research projects，technical reports，etc.）

1. Overview
2. Context: Formal Methods in Software Engineering
2.1 The Place of Formal Methods in Software Engineering . .
2.2 The Role of Mathematics
2.3 Conditions for Using Inconsistencies Productively
2.4 Two Sides of Machine Support for Proofs ..
2.5 The Essence of Formal Methods in Software Engineering .
2.6 Specific and General Formalisms
2.7 Goals and Consequences from the Analysis
Part Ⅰ. Basic Concepts
　3. Models of Time and of System Behaviors
3.1 Dense and Discrete Time Domains
3.2 Interval Sequences and Subclasses of Hybrid Systems
3.3 The Main Idea: Use of Infinitesimals
3.4 Summary
　4. Infinitesimals
4.1 The Axiom of Idealization
4.2 The Axiom of Standardization
4.3 The Axiom of Transfer
4.4 More Structure Discerned in Classical Objects
4.5 Real-Time Systems with Constant Infinitesimal Steps
4.6 Summary
　5. Operational Semantics of Discrete Systems
5.1 Action Systems
5.2 Abstract State Machines
　5.2.1 Some Introductory Examples of ASM Rules
5.2.2 Terms
5.2.3 Rules
5.3 Effectivity
5.4 Classes of Symbols
5.5 Interaction with the Environment
5.6 Gurevich's Thesis
5.6.1 Elements of Programming Languages
5.6.2 Operationality
5.6.3 No Complications Induced by Formalism
5.7 Comparison to Other Formalisms for Discrete Systems ...
5.7.1 Updates vs. Transitions
5.7.2 State Based vs. Event Based Systems
5.7.3 Structured vs. Unstructured States
5.7.4 Explicit vs. hnplieit Nondeterminism
5.7.5 Operationality vs. Declarativity
5.8 Summary
　6. Defining Hybrid Systems with ASMs
　6.1 ASMs for the Definition of Classical Hybrid Systems
　6.1.1 Standard Time ASM Rules and Hybrid Transition Systems
6.1.2 Infinite Activity
6.1.3 Hesitation and Urgency
6.2 ASMs with Infinitesimal Step Width
6.2.1 A Note on Zeno-ness in NTASMs
6.3 Simulation of an STASM by an NTASM
6.4 Well-Behaved Rules
6.5 Summary
　7. A Notation for a Temporal Logic
7.1 Semantic Domain
7.2 Interval Terms and Focused Predicates
7.3 Abbreviations
7.4 Examples of Valid Formulas
7.5 Fairness, Limited Activity and Other Example Specifications
7.6 On Accountability of a Step to Some Rule, and an Application to Synchronous Systems
7.7 Summary
Part Ⅱ. Modelling Strategies
　8. Concurrency and Reactivity: Interleaving
8.1 The Interleaving Approach to Concurrency
8.2 Some Remarks on Fairness
8.3 Properties
8.4 Interleaving NTASM Models
8.5 On the Appropriateness of the Interleaving Abstract, ion ..
8.6 Summary
　……
Part Ⅲ Applications
Part Ⅳ Summary
References
Index