This Festschrift volume is published to honour both Dines Bjørner and Zhou Chaochen on the occasion of their 70th birthdays. The volume includes 25 refereed papers by leading researchers, current and former colleagues, who congregated at a celebratory symposium held in Macao, China, in the course of the International Colloquium on Theoretical Aspects of Computing, ICTAC 2007. The papers cover a broad spectrum of subjects.

A large class of computing systems can be specified and verified by abstracting away from the temporal aspects of their behavior. In real-time systems,instead, time issues become essential. Their correctness depends not only on which functions they can perform, but also on the action execution time. Due to their importance and design challenges, real-time systems have attracted the attention of a considerable number of computer scientists and engineers from various research areas. This volume collects a set of papers accompanying the lectures of the fourth edition of the International School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM). The school addressed the use of formal methods in computer science as a prominent approach to the r- orous design of computer, communication and software systems. The main aim of the SFM series is to o?er a good spectrum of current research in foundations as well as applications of formal methods, which can be of help for graduate students and young researchers who intend to approach the field. SFM-04:RT was devoted to real-time systems. It covered formal models and languages for the specification,modeling,analysis,and verification of the seti- critical systems, the expressiveness of such models and languages, as well as supporting tools and related applications in different domains.

Real-time systems need to react to certain input stimuli within given time bounds. For example, an airbag in a car has to unfold within 300 milliseconds in a crash. There are many embedded safety-critical applications and each requires real-time specification techniques. This text introduces three of these techniques, based on logic and automata: duration calculus, timed automata, and PLC-automata. The techniques are brought together to form a seamless design flow, from real-time requirements specified in the duration calculus; via designs specified by PLC-automata; and into source code for hardware platforms of embedded systems. The syntax, semantics, and proof methods of the specification techniques are introduced; their most important properties are established; and real-life examples illustrate their use. Detailed case studies and exercises conclude each chapter. Ideal for students of real-time systems or embedded systems, this text will also be of great interest to researchers and professionals in transportation and automation.

This book constitutes the refereed proceedings of the Fifth International AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems, ARTS '99, held in Bamberg, Germany in May 1999. The 17 revised full papers presented together with three invited contributions were carefully reviewed and selected from 33 submissions. The papers are organized in topical sections on verification of probabilistic systems, model checking for probabilistic systems, semantics of probabilistic process calculi, semantics of real-time processes, real-time compilation, stochastic process algebra, and modeling and verification of real-time systems.

The first book to provide a comprehensive overview of the subject rather than a collection of papers. The author is a recognized authority in the field as well as an outstanding teacher lauded for his ability to convey these concepts clearly to many different audiences. A handy reference for practitioners in the field.

Formal engineering methods are changing the way that software systems are - veloped.Withlanguageandtoolsupport,theyarebeingusedforautomaticcode generation, and for the automatic abstraction and checking of implementations. In the future, they will be used at every stage of development: requirements, speci?cation, design, implementation, testing, and documentation. The ICFEM series of conferences aims to bring together those interested in the application of formal engineering methods to computer systems. Researchers and practitioners, from industry, academia, and government, are encouraged to attend,andtohelpadvancethestateoftheart.Authorsarestronglyencouraged to make their ideas as accessible as possible, and there is a clear emphasis upon work that promises to bring practical, tangible bene?t: reports of case studies should have a conceptual message, theory papers should have a clear link to application, and papers describing tools should have an account of results. ICFEM 2004 was the sixth conference in the series, and the ?rst to be held in North America. Previous conferences were held in Singapore, China, UK, A- tralia, and Japan. The Programme Committee received 110 papers and selected 30forpresentation.The?nalversionsofthosepapersareincludedhere,together with 2-page abstracts for the 5 accepted tutorials, and shorter abstracts for the 4 invited talks.