Preservation of timed properties during an incremental development by components
Abstract
We are interested in the preservation of local properties of timed components
during their integration in a timed system. Timed components are modeled
as timed automata or timed automata with deadlines. Properties considered
are all safety and liveness properties which can be expressed with the timed
linear logic MITL (Metric Interval Linear Logic), as well as non-zenoness and
deadlock-freedom. Integration of components is a kind of incremental development
which consists in checking locally the properties of the components, before
integrating them in the complete system, using some composition operator. Of
course, established properties have to be preserved by this integration. Checking
preservation can be achieved by means of the verification of timed -simulation
relations. Composability, compatibility and compositionality of these relations
w.r.t. composition operators are properties which allow to reduce the cost of
this verification. We examine these properties when integration is achieved with
two different timed composition operators: the classic operator usually taken
for timed systems and which uses a CSP-like composition paradigm, and a nonblocking
operator closer to the CCS paradigm.