Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

Local Testing of Message Sequence Charts is Difficult

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

Date
Le mardi 22 mai 2007 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
Madhavan Mukund (Chennai Mathematical Institute, India)

We consider message sequence charts enriched with timing constraints between pairs of events. As in the untimed setting, an infinite family of time-constrained message sequence charts (TC-MSCs) is generated using an HMSC?a finite-state automaton whose nodes are labelled by TC-MSCs.

A timed MSC is an MSC in which each event is assigned an explicit time-stamp. A timed MSC covers a TC-MSC if it satisfies all the time constraints of the TC-MSC. A natural recognizer for timed MSCs is a message-passing automaton (MPA) augmented with clocks.

The question we address is the following: given a timed system specified as a time-constrained HMSC H and an implementation in the form of a timed MPA A, is every TC-MSC generated by H covered by some timed MSC recognized by A?

We give a complete solution for locally synchronized time-constrained HMSCs, whose underlying behaviour is always regular. We also describe a restricted solution for the general case.

This is joint work with S Akshay and K Narayan Kumar.


À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

No entries.

Les séminaires précédents