A practical theory of reactive systems. Incremental modeling of dynamic behaviors. (Q1770845)

This book deals with reactive systems by first explaining a simple condition action effect language, which is similar to the language Unity or the one used in I/O automata. Subsequently, the book introduces the Temporal Logic of Actions (TLA) with an associated logic to prove properties. In the second part of the book several example systems are designed (allocator, calculator, doctor's office) along with the development of some theory (refinement) and design methodologies (object orientation, interfaces). The third part of the book deals with distributed systems and real time. Basic protocols (dining philosophers, coordination) are addressed. Regarding real time, the book adresses the basic notions (zero behavior, hybrid systems delays). This is a hefty book containing more than 400 pages. It starts with a long introduction on the practical application of theory. In the book this is translated to addressing a very large number of notions in a long winding, mathematically not too deep style. The book is usable as an extensive introduction for those that acquire the skill to use and extend it elsewhere. Of course as such it is also usable for those that want to know what is going on in the field of concurrency from a TLA perspective.