Department of Information Technology

Abstract

Analysis of discrete embedded systems often assumes that the embedded systems,
like controllers, are finite-state and that there are finitely many in the
whole system, for instance in a car. This assumption can in general not be
kept up if multiple systems like cars are supposed to interact, for example in
order to autonomously form convoys to reduce energy and space consumption
(as studied in the California PATH Project). A rather natural model for such systems,
where participants as cars freely appear and disappear, may be interconnected via links,
and communicate via synchronous or asynchronous message exchange, are graph-labelled
transition systems complemented by a first-order variant of temporal logic.

The talk surveys and discusses three aspects of specification and analysis of so-called
Dynamic Communication Systems (DCS). Firstly, there is a new model description language
for DCS, which we will discuss in particular in comparison to calculii like the
pi-calculus. Secondly, we employ a particularfirst-order temporal logic. It solves a
couple of issues shared between most earlier proposals, which interestingly
converged syntax-wise but differ significantly in semantics. And thirdly,
we demonstrate the application of an abstraction technique by K. McMillan
in this setting, which is particularly suitable for a fragment of our logic
corresponding to so-called scenarios.

Updated  2008-04-02 09:15:30 by Lisa Kaati.