Preface
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 ac-
tions they can perform, but also on the action execution time. Due to their
importance and design challenges, real-time systems have attracted the atten-
tion 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 Com-
puter, Communication and Software Systems (SFM). The school addressed the
use of formal methods in computer science as a prominent approach to the rig-
orous design of computer, communication and software systems. The main aim
of the SFM series is to offer 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 these time-
critical systems, the expressiveness of such models and languages, as well as
supporting tools and related applications in different domains.
The opening paper by Rajeev Alur and Parthasarathy Madhusudan pro-
vides a survey of the theoretical results concerning decision problems of reach-
ability, language inclusion, and language equivalence for timed automata. The
survey is concluded with a discussion of some open problems. Elmar Bihler and
Walter Vogler’s paper presents timed extensions of Petri nets with continuous
and discrete time and a natural testing-based faster-than relation for comparing
asynchronous systems. Several applications of the theory are also presented.
Jos C.M. Baeten and Michel A. Reniers present the theory and application
of classical process algebras extended with different notions of time and time
passing and compare their expressiveness via embeddings and conservative ex-
tensions. The PAR communication protocol is considered as a case study. The
expressiveness of existing timed process algebras that deal with temporal as-
pects by following very different interpretations is also the main theme of Diletta
R. Cacciagrano and Flavio Corradini’s paper. In addition, they compare the ex-
pressiveness of urgent, lazy and maximal progress tests. Mario Bravetti presents
a theory of probabilistic timed systems where durations are expressed by gen-
erally distributed random variables. The theory supports the specification of
both real-time and stochastic time during the design and analysis of concurrent
systems. Bran Selic, instead, provides an overview of the foundations of the run-
time semantics underlying the Unified Modeling Language (UML) as defined in
revision 2.0 of the official OMG standard.
我的内容管理
收起
我的收益 登录查看自己的收益
我的积分
登录查看自己的积分
我的C币
登录后查看C币余额
我的收藏 
我的下载 
下载帮助 
