Logical Time @ Work pour la modelisation et l'analyse des systemes embarques

Le temps logique est une forme de temps détendue, promue par les langages synchrones, qui est fonctionnelle, élastique (peut être abstraite ou raffinée) et multiforme. Toutes ces propriétés font que le temps logique est adéquat également au moment de la conception, alors que des annotations précises du temps physique ne devraient avoir de l'importance que dans les étapes ultérieures de la synthèse. Le Clock Constraint Specification Language (CCSL) est un langage concret dédié à la modélisation et à l'analyse des propriétés du temps logique. Le CCSL a été initialement défini comme un compagnon pour le modèle temporel du profil UML pour MARTE. Il est maintenant devenu un véritable langage de modélisation spécifique à un domaine pour la capture des relations causales, chronologiques et temporelles. Il devrait compléter d'autres modèles syntaxiques pour saisir leur modèle de calcul sous-jacent. Ce livre commence par décrire les modèles historiques de concurrence qui ont inspiré la construction du CCSL. Ensuite, le CCSL est présenté et utilisé pour construire des bibliothèques dédiées à deux modèles standards émergents dans les domaines de l'automobile (East-ADL) et de l'avionique (AADL). Enfin, une technique basée sur l'observation pour vérifier les implémentations Esterel et VHDL par rapport aux spécifications du CCSL est présentée.